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

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

• 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

theorem CategoryTheory.StrongEpi.epi {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} {f : P ⟶ Q} [self : CategoryTheory.StrongEpi f] : CategoryTheory.Epi f

The epimorphism condition on f

theorem CategoryTheory.StrongEpi.llp {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} {f : P ⟶ Q} [self : CategoryTheory.StrongEpi f] ⦃X : C⦄ ⦃Y : C⦄ (z : X ⟶ Y) [CategoryTheory.Mono z] : CategoryTheory.HasLiftingProperty f z

The left lifting property with respect to all monomorphism

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), sq.HasLift) : CategoryTheory.StrongEpi f

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

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

• 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

theorem CategoryTheory.StrongMono.mono {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} {f : P ⟶ Q} [self : CategoryTheory.StrongMono f] : CategoryTheory.Mono f

The monomorphism condition on f

theorem CategoryTheory.StrongMono.rlp {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} {f : P ⟶ Q} [self : CategoryTheory.StrongMono f] ⦃X : C⦄ ⦃Y : C⦄ (z : X ⟶ Y) [CategoryTheory.Epi z] : CategoryTheory.HasLiftingProperty z f

The right lifting property with respect to all 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), sq.HasLift) : CategoryTheory.StrongMono f

@[instance 100]

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

• ⋯ = ⋯

@[instance 100]

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

• ⋯ = ⋯

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 100]

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

• ⋯ = ⋯

@[instance 100]

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

• ⋯ = ⋯

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

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

• 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.

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

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

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

• 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.

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

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 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯