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.

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

      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
        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
            Instances For
              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
                Instances For

                  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]

                        Split monomorphisms are also absolute monomorphisms.

                        Equations
                        Instances For
                          @[simp]

                          Split epimorphisms are also absolute epimorphisms.

                          Equations
                          Instances For
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Equations
                            • One or more equations did not get rendered due to their size.