Documentation

Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic

Definitions and basic properties of normal monomorphisms and epimorphisms. #

A normal monomorphism is a morphism that is the kernel of some other morphism.

We give the construction NormalMono → RegularMono (CategoryTheory.NormalMono.regularMono) as well as the dual construction for normal epimorphisms. We show equivalences reflect normal monomorphisms (CategoryTheory.equivalenceReflectsNormalMono), and that the pullback of a normal monomorphism is normal (CategoryTheory.normalOfIsPullbackSndOfNormal).

We also define classes NormalMonoCategory and NormalEpiCategory for classes in which every monomorphism or epimorphism is normal, and deduce that these categories are RegularMonoCategorys resp. RegularEpiCategorys.

A normal monomorphism is a morphism which is the kernel of some morphism.

Instances

    Every normal monomorphism is a regular monomorphism.

    def CategoryTheory.NormalMono.lift' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] {W : C} (f : X Y) [hf : CategoryTheory.NormalMono f] (k : W Y) (h : CategoryTheory.CategoryStruct.comp k CategoryTheory.NormalMono.g = 0) :

    If f is a normal mono, then any map k : W ⟶ Y such that k ≫ normal_mono.g = 0 induces a morphism l : W ⟶ X such that l ≫ f = k.

    Instances For

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

      See also pullback.sndOfMono for the basic monomorphism version, and normalOfIsPullbackFstOfNormal for the flipped version.

      Instances For

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

        See also pullback.fstOfMono for the basic monomorphism version, and normalOfIsPullbackSndOfNormal for the flipped version.

        Instances For

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

          Instances

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

            Instances For
              class CategoryTheory.NormalEpi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] (f : X Y) :
              Type (max u₁ v₁)

              A normal epimorphism is a morphism which is the cokernel of some morphism.

              Instances

                Every normal epimorphism is a regular epimorphism.

                def CategoryTheory.NormalEpi.desc' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] {W : C} (f : X Y) [nef : CategoryTheory.NormalEpi f] (k : X W) (h : CategoryTheory.CategoryStruct.comp CategoryTheory.NormalEpi.g k = 0) :

                If f is a normal epi, then every morphism k : X ⟶ W satisfying normal_epi.g ≫ k = 0 induces l : Y ⟶ W such that f ≫ l = k.

                Instances For

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

                  See also pushout.sndOfEpi for the basic epimorphism version, and normalOfIsPushoutFstOfNormal for the flipped version.

                  Instances For

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

                    See also pushout.fstOfEpi for the basic epimorphism version, and normalOfIsPushoutSndOfNormal for the flipped version.

                    Instances For

                      A normal mono becomes a normal epi in the opposite category.

                      Instances For

                        A normal epi becomes a normal mono in the opposite category.

                        Instances For

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

                          Instances

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

                            Instances For