Documentation

Mathlib.CategoryTheory.EpiMono

Facts about epimorphisms and monomorphisms. #

The definitions of Epi and Mono are in CategoryTheory.Category, since they are used by some lemmas for Iso, which is used everywhere.

Equations
  • =
Equations
  • =
structure CategoryTheory.SplitMono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X Y) :
Type v₁

A split monomorphism is a morphism f : X ⟶ Y with a given retraction retraction f : Y ⟶ X such that f ≫ retraction f = 𝟙 X.

Every split monomorphism is a monomorphism.

Instances For
    theorem CategoryTheory.SplitMono.ext {C : Type u₁} :
    ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C} {f : X Y} {x y : CategoryTheory.SplitMono f}, x.retraction = y.retractionx = y
    @[simp]

    f composed with retraction is the identity

    @[simp]
    class CategoryTheory.IsSplitMono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X Y) :

    IsSplitMono f is the assertion that f admits a retraction

    Instances

      A composition of SplitMono is a SplitMono. -

      Equations
      Instances For
        @[simp]
        theorem CategoryTheory.SplitMono.comp_retraction {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} {f : X Y} {g : Y Z} (smf : CategoryTheory.SplitMono f) (smg : CategoryTheory.SplitMono g) :
        (smf.comp smg).retraction = CategoryTheory.CategoryStruct.comp smg.retraction smf.retraction

        A constructor for IsSplitMono f taking a SplitMono f as an argument

        structure CategoryTheory.SplitEpi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X Y) :
        Type v₁

        A split epimorphism is a morphism f : X ⟶ Y with a given section section_ f : Y ⟶ X such that section_ f ≫ f = 𝟙 Y. (Note that section is a reserved keyword, so we append an underscore.)

        Every split epimorphism is an epimorphism.

        Instances For
          theorem CategoryTheory.SplitEpi.ext {C : Type u₁} :
          ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C} {f : X Y} {x y : CategoryTheory.SplitEpi f}, x.section_ = y.section_x = y
          @[simp]

          section_ composed with f is the identity

          class CategoryTheory.IsSplitEpi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X Y) :

          IsSplitEpi f is the assertion that f admits a section

          Instances

            A composition of SplitEpi is a split SplitEpi. -

            Equations
            Instances For
              @[simp]
              theorem CategoryTheory.SplitEpi.comp_section_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} {f : X Y} {g : Y Z} (sef : CategoryTheory.SplitEpi f) (seg : CategoryTheory.SplitEpi g) :
              (sef.comp seg).section_ = CategoryTheory.CategoryStruct.comp seg.section_ sef.section_

              A constructor for IsSplitEpi f taking a SplitEpi f as an argument

              noncomputable def CategoryTheory.retraction {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X Y) [hf : CategoryTheory.IsSplitMono f] :
              Y X

              The chosen retraction of a split monomorphism.

              Equations
              Instances For

                The retraction of a split monomorphism has an obvious section.

                Equations
                • sm.splitEpi = { section_ := f, id := }
                Instances For

                  The retraction of a split monomorphism is itself a split epimorphism.

                  Equations
                  • =
                  noncomputable def CategoryTheory.section_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X Y) [hf : CategoryTheory.IsSplitEpi f] :
                  Y X

                  The chosen section of a split epimorphism. (Note that section is a reserved keyword, so we append an underscore.)

                  Equations
                  Instances For

                    The section of a split epimorphism has an obvious retraction.

                    Equations
                    • se.splitMono = { retraction := f, id := }
                    Instances For

                      The section of a split epimorphism is itself a split monomorphism.

                      Equations
                      • =
                      @[instance 100]

                      Every iso is a split mono.

                      Equations
                      • =
                      @[instance 100]

                      Every iso is a split epi.

                      Equations
                      • =
                      @[instance 100]

                      Every split mono is a mono.

                      Equations
                      • =
                      @[instance 100]

                      Every split epi is an epi.

                      Equations
                      • =

                      Every split mono whose retraction is mono is an iso.

                      Every split mono whose retraction is mono is an iso.

                      Every split epi whose section is epi is an iso.

                      Every split epi whose section is epi is an iso.

                      A category where every morphism has a Trunc retraction is computably a groupoid.

                      Equations
                      Instances For

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

                        Instances

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

                          Instances

                            In a category in which every monomorphism is split, every monomorphism splits. This is not an instance because it would create an instance loop.

                            In a category in which every epimorphism is split, every epimorphism splits. This is not an instance because it would create an instance loop.

                            Split monomorphisms are also absolute monomorphisms.

                            Equations
                            • sm.map F = { retraction := F.map sm.retraction, id := }
                            Instances For
                              @[simp]
                              theorem CategoryTheory.SplitMono.map_retraction {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} {Y : C} {f : X Y} (sm : CategoryTheory.SplitMono f) (F : CategoryTheory.Functor C D) :
                              (sm.map F).retraction = F.map sm.retraction

                              Split epimorphisms are also absolute epimorphisms.

                              Equations
                              • se.map F = { section_ := F.map se.section_, id := }
                              Instances For
                                @[simp]
                                theorem CategoryTheory.SplitEpi.map_section_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} {Y : C} {f : X Y} (se : CategoryTheory.SplitEpi f) (F : CategoryTheory.Functor C D) :
                                (se.map F).section_ = F.map se.section_