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.

Instances For
    @[inline, reducible]

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

    Instances For
      @[inline, reducible]

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

      Instances For
        @[inline, reducible]

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

        Instances For

          If ι = ι', then fork.ofι ι _ and fork.ofι ι' _ are isomorphic.

          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.

            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.

              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

                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 W' 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 W' g' eq') :

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

                  Instances For

                    Any zero object identifies to the kernel of a given monomorphisms.

                    Instances For
                      @[inline, reducible]

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

                      Instances For
                        @[inline, reducible]

                        The map from kernel f into the source of f.

                        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.

                          Instances For

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

                            Instances For
                              @[inline, reducible]

                              A commuting square induces a morphism of kernels.

                              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.

                                Instances For

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

                                  Instances For

                                    If two morphisms are known to be equal, then their kernels are isomorphic.

                                    Instances For

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

                                      Instances For

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

                                        Instances For

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

                                          Instances For

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

                                            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.

                                              Instances For
                                                @[inline, reducible]

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

                                                Instances For
                                                  @[inline, reducible]

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

                                                  Instances For

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

                                                    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.

                                                      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

                                                        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 Z' 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 Z' g' eq') :

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

                                                          Instances For
                                                            @[inline, reducible]

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

                                                            Instances For
                                                              @[inline, reducible]

                                                              The map from the target of f to cokernel f.

                                                              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.

                                                                Instances For

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

                                                                  Instances For
                                                                    @[inline, reducible]

                                                                    A commuting square induces a morphism of cokernels.

                                                                    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.

                                                                      Instances For

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

                                                                        Instances For

                                                                          If two morphisms are known to be equal, then their cokernels are isomorphic.

                                                                          Instances For

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

                                                                            Instances For

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

                                                                              Instances For

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

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

                                                                                  Instances For

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

                                                                                    Instances For

                                                                                      If s is any colimit cokernel cocone over f and i is an isomorphism such that s.π ≫ i.hom = l, then l is a cokernel of f.

                                                                                      Instances For

                                                                                        HasKernels represents the existence of kernels for every morphism.

                                                                                        Instances

                                                                                          HasCokernels represents the existence of cokernels for every morphism.

                                                                                          Instances