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

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

Instances For

@[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)

@[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

@[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

@[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)

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

Instances For

@[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

@[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)

@[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

@[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

@[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

@[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)

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

Instances For

@[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))

@[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)

@[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)

@[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

@[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

@[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

@[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

@[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

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)

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)

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

Instances For

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

Instances For

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

Instances For

@[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

@[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

@[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)

@[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)

@[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

@[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 ⋯

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[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) ⋯

@[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

@[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)

@[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

@[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) ⋯

@[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

@[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)

@[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

@[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 ⋯

@[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

@[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

@[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

@[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

@[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

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

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)

@[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

Instances For

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

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

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