Documentation

Mathlib.CategoryTheory.Limits.Shapes.StrongEpi

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

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 #

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

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

Instances
    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) :
    class CategoryTheory.StrongMono {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} (f : P Q) :

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

    Instances
      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) :

      The composition of two strong epimorphisms is a strong epimorphism.

      The composition of two strong monomorphisms is a strong monomorphism.

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

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

      An isomorphism is in particular a strong epimorphism.

      Equations
      • =

      An isomorphism is in particular a strong monomorphism.

      Equations
      • =

      A strong epimorphism that is a monomorphism is an isomorphism.

      A strong monomorphism that is an epimorphism is an isomorphism.

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

      Instances

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

        Instances