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 #

@[reducible, inline]

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

Equations
Instances For
    @[reducible, inline]

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

    Equations
    Instances For
      @[reducible, inline]

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

      Equations
      Instances For
        @[reducible, inline]

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

        Equations
        Instances For

          Every kernel fork s is isomorphic (actually, equal) to fork.ofι (fork.ι s) _.

          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
                              Instances For
                                @[reducible, inline]

                                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
                                    @[reducible, inline]

                                    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, 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
                                                        @[reducible, inline]

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

                                                        Equations
                                                        Instances For
                                                          @[reducible, inline]

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

                                                          Equations
                                                          Instances For

                                                            Every cokernel cofork s is isomorphic (actually, equal) to cofork.ofπ (cofork.π s) _.

                                                            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
                                                                                  @[reducible, inline]

                                                                                  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
                                                                                      @[reducible, inline]

                                                                                      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

                                                                                                              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.

                                                                                                              Equations
                                                                                                              Instances For

                                                                                                                HasKernels represents the existence of kernels for every morphism.

                                                                                                                Instances

                                                                                                                  HasCokernels represents the existence of cokernels for every morphism.

                                                                                                                  Instances