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
  • =
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
theorem CategoryTheory.SplitMono.ext_iff {C : Type u₁} :
∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C} {f : X Y} {x y : CategoryTheory.SplitMono f}, x = y x.retraction = y.retraction
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
    @[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 constructor for IsSplitMono f taking a SplitMono f as an argument

      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
      theorem CategoryTheory.SplitEpi.ext_iff {C : Type u₁} :
      ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C} {f : X Y} {x y : CategoryTheory.SplitEpi f}, x = y x.section_ = y.section_
      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
        @[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 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.

                        @[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 monomorphisms are also absolute monomorphisms.

                        Equations
                        • sm.map F = { retraction := F.map sm.retraction, 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_

                          Split epimorphisms are also absolute epimorphisms.

                          Equations
                          • se.map F = { section_ := F.map se.section_, id := }
                          Instances For