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

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

    If F is an equivalence and F.map f is a normal mono, then f is a normal mono.

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

      Every normal monomorphism is a regular monomorphism.

      Equations
      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.

      Equations
      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.

        Equations
        • One or more equations did not get rendered due to their size.
        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.

          Equations
          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.

              Equations
              Instances For
                @[instance 100]
                Equations
                • CategoryTheory.regularMonoCategoryOfNormalMonoCategory = { regularMonoOfMono := fun {X Y : C} (f : X Y) (x : CategoryTheory.Mono f) => inferInstance }
                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

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

                  If F is an equivalence and F.map f is a normal epi, then f is a normal epi.

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

                    Every normal epimorphism is a regular epimorphism.

                    Equations
                    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 NormalEpi.g ≫ k = 0 induces l : Y ⟶ W such that f ≫ l = k.

                    Equations
                    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.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      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.

                        Equations
                        Instances For

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

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

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

                            Equations
                            • One or more equations did not get rendered due to their size.
                            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.

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