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

as well as the dual constructions for regular epimorphisms. Additionally, we give the construction

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

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

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

Instances
    source
    theorem CategoryTheory.RegularMono.w_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {X Y : C} {f : X ⟶ Y} [self : RegularMono f] {Z : C} (h : RegularMono.Z f ⟶ Z) :
    CategoryStruct.comp f (CategoryStruct.comp left h) = CategoryStruct.comp f (CategoryStruct.comp right h)
    source
    @[instance 100]
    instance CategoryTheory.RegularMono.mono {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [RegularMono f] :
    Mono f

    Every regular monomorphism is a monomorphism.

    source
    instance CategoryTheory.equalizerRegular {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (g h : X ⟶ Y) [Limits.HasLimit (Limits.parallelPair g h)] :
    RegularMono (Limits.equalizer.ι g h)
    Equations
      source
      @[instance 100]
      instance CategoryTheory.RegularMono.ofIsSplitMono {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [IsSplitMono f] :
      RegularMono f

      Every split monomorphism is a regular monomorphism.

      Equations
        source
        def CategoryTheory.RegularMono.lift' {C : Type u₁} [Category.{v₁, u₁} C] {X Y W : C} (f : X ⟶ Y) [RegularMono f] (k : W ⟶ Y) (h : CategoryStruct.comp k left = CategoryStruct.comp k right) :
        { l : W ⟶ X // CategoryStruct.comp l f = k }

        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
            source
            def CategoryTheory.regularOfIsPullbackSndOfRegular {C : Type u₁} [Category.{v₁, u₁} C] {P Q R S : C} {f : P ⟶ Q} {g : P ⟶ R} {h : Q ⟶ S} {k : R ⟶ S} [hr : RegularMono h] (comm : CategoryStruct.comp f h = CategoryStruct.comp g k) (t : Limits.IsLimit (Limits.PullbackCone.mk f g comm)) :
            RegularMono g

            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
              Instances For
                source
                def CategoryTheory.regularOfIsPullbackFstOfRegular {C : Type u₁} [Category.{v₁, u₁} C] {P Q R S : C} {f : P ⟶ Q} {g : P ⟶ R} {h : Q ⟶ S} {k : R ⟶ S} [RegularMono k] (comm : CategoryStruct.comp f h = CategoryStruct.comp g k) (t : Limits.IsLimit (Limits.PullbackCone.mk f g comm)) :
                RegularMono f

                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
                    source
                    @[instance 100]
                    instance CategoryTheory.strongMono_of_regularMono {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [RegularMono f] :
                    StrongMono f
                    source
                    theorem CategoryTheory.isIso_of_regularMono_of_epi {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [RegularMono f] [Epi f] :
                    IsIso f

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

                    source
                    class CategoryTheory.IsRegularMonoCategory (C : Type u₁) [Category.{v₁, u₁} C] :
                    Prop

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

                    Instances
                      source
                      def CategoryTheory.regularMonoOfMono {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [IsRegularMonoCategory C] (f : X ⟶ Y) [Mono f] :
                      RegularMono f

                      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
                          source
                          @[instance 100]
                          instance CategoryTheory.regularMonoCategoryOfSplitMonoCategory {C : Type u₁} [Category.{v₁, u₁} C] [SplitMonoCategory C] :
                          IsRegularMonoCategory C
                          source
                          @[instance 100]
                          instance CategoryTheory.strongMonoCategory_of_regularMonoCategory {C : Type u₁} [Category.{v₁, u₁} C] [IsRegularMonoCategory C] :
                          StrongMonoCategory C
                          source
                          class CategoryTheory.RegularEpi {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) :
                          Type (max u₁ v₁)

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

                          Instances
                            source
                            theorem CategoryTheory.RegularEpi.w_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {X Y : C} {f : X ⟶ Y} [self : RegularEpi f] {Z : C} (h : Y ⟶ Z) :
                            CategoryStruct.comp left (CategoryStruct.comp f h) = CategoryStruct.comp right (CategoryStruct.comp f h)
                            source
                            @[instance 100]
                            instance CategoryTheory.RegularEpi.epi {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [RegularEpi f] :
                            Epi f

                            Every regular epimorphism is an epimorphism.

                            source
                            instance CategoryTheory.coequalizerRegular {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (g h : X ⟶ Y) [Limits.HasColimit (Limits.parallelPair g h)] :
                            RegularEpi (Limits.coequalizer.π g h)
                            Equations
                              source
                              noncomputable def CategoryTheory.regularEpiOfKernelPair {C : Type u₁} [Category.{v₁, u₁} C] {B X : C} (f : X ⟶ B) [Limits.HasPullback f f] (hc : Limits.IsColimit (Limits.Cofork.ofπ f ⋯)) :
                              RegularEpi f

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

                              Equations
                                Instances For
                                  source
                                  @[instance 100]
                                  instance CategoryTheory.RegularEpi.ofSplitEpi {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [IsSplitEpi f] :
                                  RegularEpi f

                                  Every split epimorphism is a regular epimorphism.

                                  Equations
                                    source
                                    def CategoryTheory.RegularEpi.desc' {C : Type u₁} [Category.{v₁, u₁} C] {X Y W : C} (f : X ⟶ Y) [RegularEpi f] (k : X ⟶ W) (h : CategoryStruct.comp left k = CategoryStruct.comp right k) :
                                    { l : Y ⟶ W // CategoryStruct.comp f l = 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
                                        source
                                        def CategoryTheory.regularOfIsPushoutSndOfRegular {C : Type u₁} [Category.{v₁, u₁} C] {P Q R S : C} {f : P ⟶ Q} {g : P ⟶ R} {h : Q ⟶ S} {k : R ⟶ S} [gr : RegularEpi g] (comm : CategoryStruct.comp f h = CategoryStruct.comp g k) (t : Limits.IsColimit (Limits.PushoutCocone.mk h k comm)) :
                                        RegularEpi h

                                        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
                                          Instances For
                                            source
                                            def CategoryTheory.regularOfIsPushoutFstOfRegular {C : Type u₁} [Category.{v₁, u₁} C] {P Q R S : C} {f : P ⟶ Q} {g : P ⟶ R} {h : Q ⟶ S} {k : R ⟶ S} [RegularEpi f] (comm : CategoryStruct.comp f h = CategoryStruct.comp g k) (t : Limits.IsColimit (Limits.PushoutCocone.mk h k comm)) :
                                            RegularEpi k

                                            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
                                                source
                                                @[instance 100]
                                                instance CategoryTheory.strongEpi_of_regularEpi {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [RegularEpi f] :
                                                StrongEpi f
                                                source
                                                theorem CategoryTheory.isIso_of_regularEpi_of_mono {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [RegularEpi f] [Mono f] :
                                                IsIso f

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

                                                source
                                                class CategoryTheory.IsRegularEpiCategory (C : Type u₁) [Category.{v₁, u₁} C] :
                                                Prop

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

                                                Instances
                                                  source
                                                  def CategoryTheory.regularEpiOfEpi {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [IsRegularEpiCategory C] (f : X ⟶ Y) [Epi f] :
                                                  RegularEpi f

                                                  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
                                                      source
                                                      @[instance 100]
                                                      instance CategoryTheory.regularEpiCategoryOfSplitEpiCategory {C : Type u₁} [Category.{v₁, u₁} C] [SplitEpiCategory C] :
                                                      IsRegularEpiCategory C
                                                      source
                                                      @[instance 100]
                                                      instance CategoryTheory.strongEpiCategory_of_regularEpiCategory {C : Type u₁} [Category.{v₁, u₁} C] [IsRegularEpiCategory C] :
                                                      StrongEpiCategory C