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

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

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

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

      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) :
      @[instance 100]
      Equations
      • =
      @[instance 100]
      Equations
      • =

      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.

      @[instance 100]

      An isomorphism is in particular a strong epimorphism.

      Equations
      • =
      @[instance 100]

      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 epi category is a category in which every epimorphism is strong.

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

        Instances

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