Documentation

Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Long exact sequence for the kernel and cokernel of a composition #

If f : X ⟶ Y and g : Y ⟶ Z are composable morphisms in an abelian category, we construct a long exact sequence : 0 ⟶ ker f ⟶ ker (f ≫ g) ⟶ ker g ⟶ coker f ⟶ coker (f ≫ g) ⟶ coker g ⟶ 0.

This is obtained by applying the snake lemma to the following morphism of exact sequences, where the rows are the obvious split exact sequences

0 ⟶ X ⟶ X ⊞ Y ⟶ Y ⟶ 0
    |f    |φ    |g
    v     v     v
0 ⟶ Y ⟶ Y ⊞ Z ⟶ Z ⟶ 0

and φ is given by the following matrix:

(f  -𝟙 Y)
(0     g)

Indeed the snake lemma gives an exact sequence involving the kernels and cokernels of the vertical maps: in order to get the expected long exact sequence, it suffices to obtain isomorphisms ker φ ≅ ker (f ≫ g) and coker φ ≅ coker (f ⋙ g).

source
noncomputable def CategoryTheory.kernelCokernelCompSequence.ι {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
Limits.kernel (CategoryStruct.comp f g) ⟶ X ⊞ Y

If f : X ⟶ Y and g : Y ⟶ Z are composable morphisms, this is the morphism kernel (f ≫ g) ⟶ X ⊞ Y which "sends x to (x, f(x))".

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.kernelCokernelCompSequence.ι_fst {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
    CategoryStruct.comp (ι f g) Limits.biprod.fst = Limits.kernel.ι (CategoryStruct.comp f g)
    source
    @[simp]
    theorem CategoryTheory.kernelCokernelCompSequence.ι_fst_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : C} (h : X ⟶ Z✝) :
    CategoryStruct.comp (ι f g) (CategoryStruct.comp Limits.biprod.fst h) = CategoryStruct.comp (Limits.kernel.ι (CategoryStruct.comp f g)) h
    source
    @[simp]
    theorem CategoryTheory.kernelCokernelCompSequence.ι_snd {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
    CategoryStruct.comp (ι f g) Limits.biprod.snd = CategoryStruct.comp (Limits.kernel.ι (CategoryStruct.comp f g)) f
    source
    @[simp]
    theorem CategoryTheory.kernelCokernelCompSequence.ι_snd_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : C} (h : Y ⟶ Z✝) :
    CategoryStruct.comp (ι f g) (CategoryStruct.comp Limits.biprod.snd h) = CategoryStruct.comp (Limits.kernel.ι (CategoryStruct.comp f g)) (CategoryStruct.comp f h)
    source
    noncomputable def CategoryTheory.kernelCokernelCompSequence.φ {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
    X ⊞ Y ⟶ Y ⊞ Z

    If f : X ⟶ Y and g : Y ⟶ Z are composable morphisms, this is the morphism X ⊞ Y ⟶ Y ⊞ Z given by the matrix

    (f  -𝟙 Y)
(0     g)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.kernelCokernelCompSequence.inl_φ {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
      CategoryStruct.comp Limits.biprod.inl (φ f g) = CategoryStruct.comp f Limits.biprod.inl
      source
      @[simp]
      theorem CategoryTheory.kernelCokernelCompSequence.inl_φ_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : C} (h : Y ⊞ Z ⟶ Z✝) :
      CategoryStruct.comp Limits.biprod.inl (CategoryStruct.comp (φ f g) h) = CategoryStruct.comp f (CategoryStruct.comp Limits.biprod.inl h)
      source
      @[simp]
      theorem CategoryTheory.kernelCokernelCompSequence.inr_φ_fst {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
      CategoryStruct.comp Limits.biprod.inr (CategoryStruct.comp (φ f g) Limits.biprod.fst) = -CategoryStruct.id Y
      source
      @[simp]
      theorem CategoryTheory.kernelCokernelCompSequence.inr_φ_fst_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : C} (h : Y ⟶ Z✝) :
      CategoryStruct.comp Limits.biprod.inr (CategoryStruct.comp (φ f g) (CategoryStruct.comp Limits.biprod.fst h)) = CategoryStruct.comp (-CategoryStruct.id Y) h
      source
      @[simp]
      theorem CategoryTheory.kernelCokernelCompSequence.φ_snd {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
      CategoryStruct.comp (φ f g) Limits.biprod.snd = CategoryStruct.comp Limits.biprod.snd g
      source
      @[simp]
      theorem CategoryTheory.kernelCokernelCompSequence.φ_snd_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : C} (h : Z ⟶ Z✝) :
      CategoryStruct.comp (φ f g) (CategoryStruct.comp Limits.biprod.snd h) = CategoryStruct.comp Limits.biprod.snd (CategoryStruct.comp g h)
      source
      noncomputable def CategoryTheory.kernelCokernelCompSequence.π {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
      Y ⊞ Z ⟶ Limits.cokernel (CategoryStruct.comp f g)

      If f : X ⟶ Y and g : Y ⟶ Z are composable morphisms, this is the morphism Y ⊞ Z ⟶ cokernel (f ≫ g) which "sends (y, z) to [g(y)] + [z]".

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.kernelCokernelCompSequence.inl_π {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
        CategoryStruct.comp Limits.biprod.inl (π f g) = CategoryStruct.comp g (Limits.cokernel.π (CategoryStruct.comp f g))
        source
        @[simp]
        theorem CategoryTheory.kernelCokernelCompSequence.inl_π_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : C} (h : Limits.cokernel (CategoryStruct.comp f g) ⟶ Z✝) :
        CategoryStruct.comp Limits.biprod.inl (CategoryStruct.comp (π f g) h) = CategoryStruct.comp g (CategoryStruct.comp (Limits.cokernel.π (CategoryStruct.comp f g)) h)
        source
        @[simp]
        theorem CategoryTheory.kernelCokernelCompSequence.inr_π {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
        CategoryStruct.comp Limits.biprod.inr (π f g) = Limits.cokernel.π (CategoryStruct.comp f g)
        source
        @[simp]
        theorem CategoryTheory.kernelCokernelCompSequence.inr_π_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : C} (h : Limits.cokernel (CategoryStruct.comp f g) ⟶ Z✝) :
        CategoryStruct.comp Limits.biprod.inr (CategoryStruct.comp (π f g) h) = CategoryStruct.comp (Limits.cokernel.π (CategoryStruct.comp f g)) h
        source
        @[simp]
        theorem CategoryTheory.kernelCokernelCompSequence.ι_φ {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
        CategoryStruct.comp (ι f g) (φ f g) = 0
        source
        @[simp]
        theorem CategoryTheory.kernelCokernelCompSequence.ι_φ_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : C} (h : Y ⊞ Z ⟶ Z✝) :
        CategoryStruct.comp (ι f g) (CategoryStruct.comp (φ f g) h) = CategoryStruct.comp 0 h
        source
        @[simp]
        theorem CategoryTheory.kernelCokernelCompSequence.φ_π {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
        CategoryStruct.comp (φ f g) (π f g) = 0
        source
        @[simp]
        theorem CategoryTheory.kernelCokernelCompSequence.φ_π_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : C} (h : Limits.cokernel (CategoryStruct.comp f g) ⟶ Z✝) :
        CategoryStruct.comp (φ f g) (CategoryStruct.comp (π f g) h) = CategoryStruct.comp 0 h
        source
        instance CategoryTheory.kernelCokernelCompSequence.instMonoι {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
        Mono (ι f g)
        source
        instance CategoryTheory.kernelCokernelCompSequence.instEpiπ {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
        Epi (π f g)
        source
        noncomputable def CategoryTheory.kernelCokernelCompSequence.isLimit {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
        Limits.IsLimit (Limits.KernelFork.ofι (ι f g) ⋯)

        If f : X ⟶ Y and g : Y ⟶ Z are composable morphisms, then the kernel of φ f g : X ⊞ Y ⟶ Y ⊞ Z identifies to kernel (f ≫ g).

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def CategoryTheory.kernelCokernelCompSequence.isColimit {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
          Limits.IsColimit (Limits.CokernelCofork.ofπ (π f g) ⋯)

          If f : X ⟶ Y and g : Y ⟶ Z are composable morphisms, then the cokernel of φ f g : X ⊞ Y ⟶ Y ⊞ Z identifies to cokernel (f ≫ g).

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def CategoryTheory.kernelCokernelCompSequence.snakeInput {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
            ShortComplex.SnakeInput C

            The "snake input" which gives the exact sequence 0 ⟶ ker f ⟶ ker (f ≫ g) ⟶ ker g ⟶ coker f ⟶ coker (f ≫ g) ⟶ coker g ⟶ 0, see kernelCokernelCompSequence_exact.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_v₁₂_τ₃ {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).v₁₂.τ₃ = g
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_g {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).L₃.g = Limits.cokernel.map (CategoryStruct.comp f g) g f (CategoryStruct.id Z) ⋯
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_X₁ {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).L₂.X₁ = Y
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₂ {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).v₂₃.τ₂ = π f g
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_v₁₂_τ₂ {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).v₁₂.τ₂ = φ f g
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₃ {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).v₀₁.τ₃ = Limits.kernel.ι g
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_X₁ {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).L₁.X₁ = X
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_X₂ {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).L₀.X₂ = Limits.kernel (CategoryStruct.comp f g)
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_X₃ {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).L₂.X₃ = Z
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_X₁ {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).L₃.X₁ = Limits.cokernel f
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_X₃ {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).L₀.X₃ = Limits.kernel g
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_X₂ {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).L₃.X₂ = Limits.cokernel (CategoryStruct.comp f g)
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_g {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).L₁.g = Limits.biprod.snd
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_g {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).L₀.g = Limits.kernel.map (CategoryStruct.comp f g) g f (CategoryStruct.id Z) ⋯
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_g {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).L₂.g = Limits.biprod.snd
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₃ {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).v₂₃.τ₃ = Limits.cokernel.π g
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_f {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).L₃.f = Limits.cokernel.map f (CategoryStruct.comp f g) (CategoryStruct.id X) g ⋯
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_X₂ {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).L₂.X₂ = (Y ⊞ Z)
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_v₁₂_τ₁ {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).v₁₂.τ₁ = f
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₁ {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).v₂₃.τ₁ = Limits.cokernel.π f
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₁ {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).v₀₁.τ₁ = Limits.kernel.ι f
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₂ {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).v₀₁.τ₂ = ι f g
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_f {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).L₂.f = Limits.biprod.inl
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_X₃ {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).L₁.X₃ = Y
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_X₁ {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).L₀.X₁ = Limits.kernel f
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_f {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).L₁.f = Limits.biprod.inl
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_X₃ {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).L₃.X₃ = Limits.cokernel g
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_f {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).L₀.f = Limits.kernel.map f (CategoryStruct.comp f g) (CategoryStruct.id X) g ⋯
              source
              @[simp]
              theorem CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_X₂ {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (snakeInput f g).L₁.X₂ = (X ⊞ Y)
              source
              noncomputable def CategoryTheory.kernelCokernelCompSequence.δ {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
              Limits.kernel g ⟶ Limits.cokernel f

              If f : X ⟶ Y and g : Y ⟶ Z are composable morphisms, this is the connecting homomorphism kernel g ⟶ cokernel f.

              Equations
              Instances For
                source
                theorem CategoryTheory.kernelCokernelCompSequence.δ_fac {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
                δ f g = -CategoryStruct.comp (Limits.kernel.ι g) (Limits.cokernel.π f)
                source
                @[reducible, inline]
                noncomputable abbrev CategoryTheory.kernelCokernelCompSequence {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
                ComposableArrows C 5

                If f : X ⟶ Y and g : Y ⟶ Z are composable morphisms in an abelian category, this is the long exact sequence 0 ⟶ ker f ⟶ ker (f ≫ g) ⟶ ker g ⟶ coker f ⟶ coker (f ≫ g) ⟶ coker g ⟶ 0.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  instance CategoryTheory.instMonoMap'KernelCokernelCompSequenceOfNatNat {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
                  Mono ((kernelCokernelCompSequence f g).map' 0 1 ⋯ ⋯)
                  source
                  instance CategoryTheory.instEpiMap'KernelCokernelCompSequenceOfNatNat {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
                  Epi ((kernelCokernelCompSequence f g).map' 4 5 ⋯ ⋯)
                  source
                  theorem CategoryTheory.kernelCokernelCompSequence_exact {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
                  (kernelCokernelCompSequence f g).Exact