kernelCokernelCompSequence — Mathlib

English

In an abelian category with suitable kernels and cokernels, the canonical comparison map from coimage to image is an isomorphism.

Русский

В абелевой категории при наличии подходящих ядер и кокернелей каноническое отображение между кообразом и образом является изоморфизмом.

LaTeX

$$$\text{coimageImageComparison } f \;:\; \text{coimage } f \;\to\; \text{image } f\; \text{ is an isomorphism}.$$$

Lean4

/-- 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`. -/
noncomputable abbrev kernelCokernelCompSequence : ComposableArrows C 5 :=
  .mk₅ (kernel.map f (f ≫ g) (𝟙 _) g (by simp)) (kernel.map (f ≫ g) g f (𝟙 _) (by simp)) (δ f g)
    (cokernel.map f (f ≫ g) (𝟙 _) g (by simp)) (cokernel.map (f ≫ g) g f (𝟙 _) (by simp))

Похожие утверждения