Documentation

Mathlib.CategoryTheory.Limits.Shapes.Kernels

Kernels and cokernels #

In a category with zero morphisms, the kernel of a morphism f : X ⟶ Y is the equalizer of f and 0 : X ⟶ Y. (Similarly the cokernel is the coequalizer.)

The basic definitions are

Main statements #

Besides the definition and lifts, we prove

and the corresponding dual statements.

Future work #

Implementation notes #

As with the other special shapes in the limits library, all the definitions here are given as abbreviations of the general statements for limits, so all the simp lemmas and theorems about general limits can be used.

References #

@[inline, reducible]

A morphism f has a kernel if the functor ParallelPair f 0 has a limit.

Equations
Instances For
    @[inline, reducible]

    A morphism f has a cokernel if the functor ParallelPair f 0 has a colimit.

    Equations
    Instances For
      @[inline, reducible]

      A kernel fork is just a fork where the second morphism is a zero morphism.

      Equations
      Instances For
        @[inline, reducible]

        A morphism ι satisfying ι ≫ f = 0 determines a kernel fork over f.

        Equations
        Instances For

          If F is an equivalence, then applying F to a diagram indexing a (co)kernel of f yields the diagram indexing the (co)kernel of F.map f.

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

            If s is a limit kernel fork and k : W ⟶ X satisfies k ≫ f = 0, then there is some l : W ⟶ s.X such that l ≫ fork.ι s = k.

            Equations
            Instances For

              This is a slightly more convenient method to verify that a kernel fork is a limit cone. It only asks for a proof of facts that carry any mathematical content

              Equations
              Instances For
                def CategoryTheory.Limits.KernelFork.IsLimit.ofι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} {Y : C} {f : X Y} {W : C} (g : W X) (eq : CategoryTheory.CategoryStruct.comp g f = 0) (lift : {W' : C} → (g' : W' X) → CategoryTheory.CategoryStruct.comp g' f = 0(W' W)) (fac : ∀ {W' : C} (g' : W' X) (eq' : CategoryTheory.CategoryStruct.comp g' f = 0), CategoryTheory.CategoryStruct.comp (lift g' eq') g = g') (uniq : ∀ {W' : C} (g' : W' X) (eq' : CategoryTheory.CategoryStruct.comp g' f = 0) (m : W' W), CategoryTheory.CategoryStruct.comp m g = g'm = lift g' eq') :

                This is a more convenient formulation to show that a KernelFork constructed using KernelFork.ofι is a limit cone.

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

                  This is a more convenient formulation to show that a KernelFork of the form KernelFork.ofι i _ is a limit cone when we know that i is a monomorphism.

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

                    Every kernel of f induces a kernel of f ≫ g if g is mono.

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

                      Every kernel of f ≫ g is also a kernel of f, as long as c.ι ≫ f vanishes.

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

                        X identifies to the kernel of a zero map X ⟶ Y.

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

                          The morphism between points of kernel forks induced by a morphism in the category of arrows.

                          Equations
                          Instances For

                            The isomorphism between points of limit kernel forks induced by an isomorphism in the category of arrows.

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

                              The kernel of a morphism, expressed as the equalizer with the 0 morphism.

                              Equations
                              Instances For

                                The kernel built from kernel.ι f is limiting.

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

                                  Given any morphism k : W ⟶ X satisfying k ≫ f = 0, k factors through kernel.ι f via kernel.lift : W ⟶ kernel f.

                                  Equations
                                  Instances For

                                    Any morphism k : W ⟶ X satisfying k ≫ f = 0 induces a morphism l : W ⟶ kernel f such that l ≫ kernel.ι f = k.

                                    Equations
                                    Instances For

                                      Given a commutative diagram X --f--> Y --g--> Z | | | | | | v v v X' -f'-> Y' -g'-> Z' with horizontal arrows composing to zero, then we obtain a commutative square X ---> kernel g | | | | kernel.map | | v v X' --> kernel g'

                                      A commuting square of isomorphisms induces an isomorphism of kernels.

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

                                        Every kernel of the zero morphism is an isomorphism

                                        Equations
                                        • =

                                        The kernel of a zero morphism is isomorphic to the source.

                                        Equations
                                        Instances For

                                          When g is a monomorphism, the kernel of f ≫ g is isomorphic to the kernel of f.

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

                                            When f is an isomorphism, the kernel of f ≫ g is isomorphic to the kernel of g.

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

                                              The morphism from the zero object determines a cone on a kernel diagram

                                              Equations
                                              Instances For

                                                The kernel of a monomorphism is isomorphic to the zero object

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

                                                  If i is an isomorphism such that l ≫ i.hom = f, then any kernel of f is a kernel of l.

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

                                                    If s is any limit kernel cone over f and if i is an isomorphism such that i.hom ≫ s.ι = l, then l is a kernel of f.

                                                    Equations
                                                    Instances For
                                                      @[inline, reducible]

                                                      A cokernel cofork is just a cofork where the second morphism is a zero morphism.

                                                      Equations
                                                      Instances For
                                                        @[inline, reducible]

                                                        A morphism π satisfying f ≫ π = 0 determines a cokernel cofork on f.

                                                        Equations
                                                        Instances For

                                                          If π = π', then CokernelCofork.of_π π _ and CokernelCofork.of_π π' _ are isomorphic.

                                                          Equations
                                                          Instances For

                                                            If s is a colimit cokernel cofork, then every k : Y ⟶ W satisfying f ≫ k = 0 induces l : s.X ⟶ W such that cofork.π s ≫ l = k.

                                                            Equations
                                                            Instances For

                                                              This is a slightly more convenient method to verify that a cokernel cofork is a colimit cocone. It only asks for a proof of facts that carry any mathematical content

                                                              Equations
                                                              Instances For
                                                                def CategoryTheory.Limits.CokernelCofork.IsColimit.ofπ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} {Y : C} {f : X Y} {Z : C} (g : Y Z) (eq : CategoryTheory.CategoryStruct.comp f g = 0) (desc : {Z' : C} → (g' : Y Z') → CategoryTheory.CategoryStruct.comp f g' = 0(Z Z')) (fac : ∀ {Z' : C} (g' : Y Z') (eq' : CategoryTheory.CategoryStruct.comp f g' = 0), CategoryTheory.CategoryStruct.comp g (desc g' eq') = g') (uniq : ∀ {Z' : C} (g' : Y Z') (eq' : CategoryTheory.CategoryStruct.comp f g' = 0) (m : Z Z'), CategoryTheory.CategoryStruct.comp g m = g'm = desc g' eq') :

                                                                This is a more convenient formulation to show that a CokernelCofork constructed using CokernelCofork.ofπ is a limit cone.

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

                                                                  This is a more convenient formulation to show that a CokernelCofork of the form CokernelCofork.ofπ p _ is a colimit cocone when we know that p is an epimorphism.

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

                                                                    Every cokernel of f induces a cokernel of g ≫ f if g is epi.

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

                                                                      Every cokernel of g ≫ f is also a cokernel of f, as long as f ≫ c.π vanishes.

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

                                                                        Y identifies to the cokernel of a zero map X ⟶ Y.

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

                                                                          The morphism between points of cokernel coforks induced by a morphism in the category of arrows.

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

                                                                            The isomorphism between points of limit cokernel coforks induced by an isomorphism in the category of arrows.

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

                                                                              The cokernel of a morphism, expressed as the coequalizer with the 0 morphism.

                                                                              Equations
                                                                              Instances For

                                                                                The cokernel built from cokernel.π f is colimiting.

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

                                                                                  Given any morphism k : Y ⟶ W such that f ≫ k = 0, k factors through cokernel.π f via cokernel.desc : cokernel f ⟶ W.

                                                                                  Equations
                                                                                  Instances For

                                                                                    Any morphism k : Y ⟶ W satisfying f ≫ k = 0 induces l : cokernel f ⟶ W such that cokernel.π f ≫ l = k.

                                                                                    Equations
                                                                                    Instances For

                                                                                      Given a commutative diagram X --f--> Y --g--> Z | | | | | | v v v X' -f'-> Y' -g'-> Z' with horizontal arrows composing to zero, then we obtain a commutative square cokernel f ---> Z | | | cokernel.map | | | v v cokernel f' --> Z'

                                                                                      A commuting square of isomorphisms induces an isomorphism of cokernels.

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

                                                                                        The cokernel of the zero morphism is an isomorphism

                                                                                        Equations
                                                                                        • =

                                                                                        The cokernel of a zero morphism is isomorphic to the target.

                                                                                        Equations
                                                                                        Instances For

                                                                                          When g is an isomorphism, the cokernel of f ≫ g is isomorphic to the cokernel of f.

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

                                                                                            When f is an epimorphism, the cokernel of f ≫ g is isomorphic to the cokernel of g.

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

                                                                                              The morphism to the zero object determines a cocone on a cokernel diagram

                                                                                              Equations
                                                                                              Instances For

                                                                                                The morphism to the zero object is a cokernel of an epimorphism

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

                                                                                                  The cokernel of an epimorphism is isomorphic to the zero object

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

                                                                                                    The cokernel of the image inclusion of a morphism f is isomorphic to the cokernel of f.

                                                                                                    (This result requires that the factorisation through the image is an epimorphism. This holds in any category with equalizers.)

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

                                                                                                      If f ≫ g = 0 implies g = 0 for all g, then 0 : Y ⟶ 0 is a cokernel of f.

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

                                                                                                        If i is an isomorphism such that i.hom ≫ l = f, then any cokernel of f is a cokernel of l.

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

                                                                                                          HasKernels represents the existence of kernels for every morphism.

                                                                                                          Instances

                                                                                                            HasCokernels represents the existence of cokernels for every morphism.

                                                                                                            Instances