Extremal epimorphisms

An extremal epimorphism p : X ⟶ Y is an epimorphism which does not factor through any proper subobject of Y. In case the category has equalizers, we show that a morphism p : X ⟶ Y which does not factor through any proper subobject of Y is automatically an epimorphism, and also an extremal epimorphism. We also show that a strong epimorphism is an extremal epimorphism, and that both notions coincide when the category has pullbacks.

References

• https://ncatlab.org/nlab/show/extremal+epimorphism

class CategoryTheory.ExtremalEpi {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) extends CategoryTheory.Epi f : Prop

An extremal epimorphism f : X ⟶ Y is an epimorphism which does not factor through any proper subobject of Y.

• left_cancellation {Z : C} (g h : Y ⟶ Z) : CategoryStruct.comp f g = CategoryStruct.comp f h → g = h
• isIso {Z : C} (p : X ⟶ Z) (i : Z ⟶ Y) (fac : CategoryStruct.comp p i = f) [Mono i] : IsIso i

theorem CategoryTheory.ExtremalEpi.subobject_eq_top {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [ExtremalEpi f] {A : Subobject Y} (hA : A.Factors f) : A = ⊤

theorem CategoryTheory.ExtremalEpi.mk_of_hasEqualizers {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Limits.HasEqualizers C] (hf : ∀ ⦃Z : C⦄ (p : X ⟶ Z) (i : Z ⟶ Y), CategoryStruct.comp p i = f → ∀ [Mono i], IsIso i) : ExtremalEpi f

instance CategoryTheory.instExtremalEpiOfStrongEpi {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [StrongEpi f] : ExtremalEpi f

theorem CategoryTheory.extremalEpi_iff_strongEpi_of_hasPullbacks {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Limits.HasPullbacks C] : ExtremalEpi f ↔ StrongEpi f