Documentation

Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Definitions and basic properties of regular monomorphisms and epimorphisms. #

A regular monomorphism is a morphism that is the equalizer of some parallel pair.

We give the constructions

We also define classes RegularMonoCategory and RegularEpiCategory for categories in which every monomorphism or epimorphism is regular, and deduce that these categories are StrongMonoCategorys resp. StrongEpiCategorys.

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

A regular monomorphism is a morphism which is the equalizer of some parallel pair.

Instances
    theorem CategoryTheory.RegularMono.w {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {f : X Y} [self : CategoryTheory.RegularMono f] :
    CategoryTheory.CategoryStruct.comp f CategoryTheory.RegularMono.left = CategoryTheory.CategoryStruct.comp f CategoryTheory.RegularMono.right

    f equalizes the two maps

    @[instance 100]

    Every regular monomorphism is a monomorphism.

    Equations
    • =
    Equations
    • One or more equations did not get rendered due to their size.
    @[instance 100]

    Every split monomorphism is a regular monomorphism.

    Equations
    • One or more equations did not get rendered due to their size.
    def CategoryTheory.RegularMono.lift' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {W : C} (f : X Y) [CategoryTheory.RegularMono f] (k : W Y) (h : CategoryTheory.CategoryStruct.comp k CategoryTheory.RegularMono.left = CategoryTheory.CategoryStruct.comp k CategoryTheory.RegularMono.right) :

    If f is a regular mono, then any map k : W ⟶ Y equalizing RegularMono.left and RegularMono.right induces a morphism l : W ⟶ X such that l ≫ f = k.

    Equations
    Instances For

      The second leg of a pullback cone is a regular monomorphism if the right component is too.

      See also Pullback.sndOfMono for the basic monomorphism version, and regularOfIsPullbackFstOfRegular for the flipped version.

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

        The first leg of a pullback cone is a regular monomorphism if the left component is too.

        See also Pullback.fstOfMono for the basic monomorphism version, and regularOfIsPullbackSndOfRegular for the flipped version.

        Equations
        Instances For
          @[instance 100]
          Equations
          • =

          A regular monomorphism is an isomorphism if it is an epimorphism.

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

          Instances

            In a category in which every monomorphism is regular, we can express every monomorphism as an equalizer. This is not an instance because it would create an instance loop.

            Equations
            Instances For
              @[instance 100]
              Equations
              • CategoryTheory.regularMonoCategoryOfSplitMonoCategory = { regularMonoOfMono := fun {X Y : C} (f : X Y) (x : CategoryTheory.Mono f) => inferInstance }
              class CategoryTheory.RegularEpi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X Y) :
              Type (max u₁ v₁)

              A regular epimorphism is a morphism which is the coequalizer of some parallel pair.

              Instances
                theorem CategoryTheory.RegularEpi.w {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {f : X Y} [self : CategoryTheory.RegularEpi f] :
                CategoryTheory.CategoryStruct.comp CategoryTheory.RegularEpi.left f = CategoryTheory.CategoryStruct.comp CategoryTheory.RegularEpi.right f

                f coequalizes the two maps

                @[instance 100]

                Every regular epimorphism is an epimorphism.

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

                A morphism which is a coequalizer for its kernel pair is a regular epi.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[instance 100]

                  Every split epimorphism is a regular epimorphism.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  def CategoryTheory.RegularEpi.desc' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {W : C} (f : X Y) [CategoryTheory.RegularEpi f] (k : X W) (h : CategoryTheory.CategoryStruct.comp CategoryTheory.RegularEpi.left k = CategoryTheory.CategoryStruct.comp CategoryTheory.RegularEpi.right k) :

                  If f is a regular epi, then every morphism k : X ⟶ W coequalizing RegularEpi.left and RegularEpi.right induces l : Y ⟶ W such that f ≫ l = k.

                  Equations
                  Instances For

                    The second leg of a pushout cocone is a regular epimorphism if the right component is too.

                    See also Pushout.sndOfEpi for the basic epimorphism version, and regularOfIsPushoutFstOfRegular for the flipped version.

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

                      The first leg of a pushout cocone is a regular epimorphism if the left component is too.

                      See also Pushout.fstOfEpi for the basic epimorphism version, and regularOfIsPushoutSndOfRegular for the flipped version.

                      Equations
                      Instances For
                        @[instance 100]
                        Equations
                        • =

                        A regular epimorphism is an isomorphism if it is a monomorphism.

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

                        Instances

                          In a category in which every epimorphism is regular, we can express every epimorphism as a coequalizer. This is not an instance because it would create an instance loop.

                          Equations
                          Instances For
                            @[instance 100]
                            Equations
                            • CategoryTheory.regularEpiCategoryOfSplitEpiCategory = { regularEpiOfEpi := fun {X Y : C} (f : X Y) (x : CategoryTheory.Epi f) => inferInstance }