Strong epimorphisms

In this file, we define strong epimorphisms. A strong epimorphism is an epimorphism f which has the (unique) left lifting property with respect to monomorphisms. Similarly, a strong monomorphisms in a monomorphism which has the (unique) right lifting property with respect to epimorphisms.

Main results

Besides the definition, we show that

• the composition of two strong epimorphisms is a strong epimorphism,
• if f ≫ g is a strong epimorphism, then so is g,
• if f is both a strong epimorphism and a monomorphism, then it is an isomorphism

We also define classes StrongMonoCategory and StrongEpiCategory for categories in which every monomorphism or epimorphism is strong, and deduce that these categories are balanced.

TODO

Show that the dual of a strong epimorphism is a strong monomorphism, and vice versa.

References

• [F. Borceux, Handbook of Categorical Algebra 1][borceux-vol1]

class CategoryTheory.StrongEpi {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} (f : P ⟶ Q) : Prop

• epi : CategoryTheory.Epi f

  The epimorphism condition on f

• llp : ∀ ⦃X Y : C⦄ (z : X ⟶ Y) [inst : CategoryTheory.Mono z], CategoryTheory.HasLiftingProperty f z

  The left lifting property with respect to all monomorphism

A strong epimorphism f is an epimorphism which has the left lifting property with respect to monomorphisms.

theorem CategoryTheory.StrongEpi.mk' {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} {f : P ⟶ Q} [CategoryTheory.Epi f] (hf : ∀ (X Y : C) (z : X ⟶ Y), CategoryTheory.Mono z → ∀ (u : P ⟶ X) (v : Q ⟶ Y) (sq : CategoryTheory.CommSq u f z v), CategoryTheory.CommSq.HasLift sq) : CategoryTheory.StrongEpi f

class CategoryTheory.StrongMono {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} (f : P ⟶ Q) : Prop

• mono : CategoryTheory.Mono f

  The monomorphism condition on f

• rlp : ∀ ⦃X Y : C⦄ (z : X ⟶ Y) [inst : CategoryTheory.Epi z], CategoryTheory.HasLiftingProperty z f

  The right lifting property with respect to all epimorphisms

A strong monomorphism f is a monomorphism which has the right lifting property with respect to epimorphisms.

theorem CategoryTheory.StrongMono.mk' {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} {f : P ⟶ Q} [CategoryTheory.Mono f] (hf : ∀ (X Y : C) (z : X ⟶ Y), CategoryTheory.Epi z → ∀ (u : X ⟶ P) (v : Y ⟶ Q) (sq : CategoryTheory.CommSq u z f v), CategoryTheory.CommSq.HasLift sq) : CategoryTheory.StrongMono f

instance CategoryTheory.epi_of_strongEpi {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} (f : P ⟶ Q) [CategoryTheory.StrongEpi f] : CategoryTheory.Epi f

Equations

• (_ : CategoryTheory.Epi f) = (_ : CategoryTheory.Epi f)

instance CategoryTheory.mono_of_strongMono {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} (f : P ⟶ Q) [CategoryTheory.StrongMono f] : CategoryTheory.Mono f

Equations

• (_ : CategoryTheory.Mono f) = (_ : CategoryTheory.Mono f)

theorem CategoryTheory.strongEpi_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} {R : C} (f : P ⟶ Q) (g : Q ⟶ R) [CategoryTheory.StrongEpi f] [CategoryTheory.StrongEpi g] : CategoryTheory.StrongEpi (CategoryTheory.CategoryStruct.comp f g)

The composition of two strong epimorphisms is a strong epimorphism.

theorem CategoryTheory.strongMono_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} {R : C} (f : P ⟶ Q) (g : Q ⟶ R) [CategoryTheory.StrongMono f] [CategoryTheory.StrongMono g] : CategoryTheory.StrongMono (CategoryTheory.CategoryStruct.comp f g)

The composition of two strong monomorphisms is a strong monomorphism.

theorem CategoryTheory.strongEpi_of_strongEpi {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} {R : C} (f : P ⟶ Q) (g : Q ⟶ R) [CategoryTheory.StrongEpi (CategoryTheory.CategoryStruct.comp f g)] : CategoryTheory.StrongEpi g

If f ≫ g is a strong epimorphism, then so is g.

theorem CategoryTheory.strongMono_of_strongMono {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} {R : C} (f : P ⟶ Q) (g : Q ⟶ R) [CategoryTheory.StrongMono (CategoryTheory.CategoryStruct.comp f g)] : CategoryTheory.StrongMono f

If f ≫ g is a strong monomorphism, then so is f.

instance CategoryTheory.strongEpi_of_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} (f : P ⟶ Q) [CategoryTheory.IsIso f] : CategoryTheory.StrongEpi f

An isomorphism is in particular a strong epimorphism.

Equations

• @CategoryTheory.strongEpi_of_isIso = @CategoryTheory.strongEpi_of_isIso.proof_1

instance CategoryTheory.strongMono_of_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} (f : P ⟶ Q) [CategoryTheory.IsIso f] : CategoryTheory.StrongMono f

An isomorphism is in particular a strong monomorphism.

Equations

• @CategoryTheory.strongMono_of_isIso = @CategoryTheory.strongMono_of_isIso.proof_1

theorem CategoryTheory.StrongEpi.of_arrow_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} {B : C} {A' : C} {B' : C} {f : A ⟶ B} {g : A' ⟶ B'} (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g) [h : CategoryTheory.StrongEpi f] : CategoryTheory.StrongEpi g

theorem CategoryTheory.StrongMono.of_arrow_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} {B : C} {A' : C} {B' : C} {f : A ⟶ B} {g : A' ⟶ B'} (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g) [h : CategoryTheory.StrongMono f] : CategoryTheory.StrongMono g

theorem CategoryTheory.StrongEpi.iff_of_arrow_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} {B : C} {A' : C} {B' : C} {f : A ⟶ B} {g : A' ⟶ B'} (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g) : CategoryTheory.StrongEpi f ↔ CategoryTheory.StrongEpi g

theorem CategoryTheory.StrongMono.iff_of_arrow_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} {B : C} {A' : C} {B' : C} {f : A ⟶ B} {g : A' ⟶ B'} (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g) : CategoryTheory.StrongMono f ↔ CategoryTheory.StrongMono g

theorem CategoryTheory.isIso_of_mono_of_strongEpi {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} (f : P ⟶ Q) [CategoryTheory.Mono f] [CategoryTheory.StrongEpi f] : CategoryTheory.IsIso f

A strong epimorphism that is a monomorphism is an isomorphism.

theorem CategoryTheory.isIso_of_epi_of_strongMono {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} (f : P ⟶ Q) [CategoryTheory.Epi f] [CategoryTheory.StrongMono f] : CategoryTheory.IsIso f

A strong monomorphism that is an epimorphism is an isomorphism.

class CategoryTheory.StrongEpiCategory (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop

• strongEpi_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [inst : CategoryTheory.Epi f], CategoryTheory.StrongEpi f

  A strong epi category is a category in which every epimorphism is strong.

A strong epi category is a category in which every epimorphism is strong.

class CategoryTheory.StrongMonoCategory (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop

• strongMono_of_mono : ∀ {X Y : C} (f : X ⟶ Y) [inst : CategoryTheory.Mono f], CategoryTheory.StrongMono f

  A strong mono category is a category in which every monomorphism is strong.

A strong mono category is a category in which every monomorphism is strong.

theorem CategoryTheory.strongEpi_of_epi {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} [CategoryTheory.StrongEpiCategory C] (f : P ⟶ Q) [CategoryTheory.Epi f] : CategoryTheory.StrongEpi f

theorem CategoryTheory.strongMono_of_mono {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} [CategoryTheory.StrongMonoCategory C] (f : P ⟶ Q) [CategoryTheory.Mono f] : CategoryTheory.StrongMono f

instance CategoryTheory.balanced_of_strongEpiCategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.StrongEpiCategory C] : CategoryTheory.Balanced C

Equations

• @CategoryTheory.balanced_of_strongEpiCategory = @CategoryTheory.balanced_of_strongEpiCategory.proof_1

instance CategoryTheory.balanced_of_strongMonoCategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.StrongMonoCategory C] : CategoryTheory.Balanced C

Equations

• @CategoryTheory.balanced_of_strongMonoCategory = @CategoryTheory.balanced_of_strongMonoCategory.proof_1