kernelCokernelCompSequence_exact — Mathlib

English

Let f: X → Y and g: Y → Z be morphisms in an Abelian category. Then the four-term sequence ker(f) → X → Y → cokernel(g) is exact.

Русский

Пусть f: X → Y и g: Y → Z — морфизмы в абелевой категории. Тогда последовательность ker(f) → X → Y → cokernel(g) точна.

LaTeX

$$$\\ker f \\xrightarrow{\\iota_f} X \\xrightarrow{f} Y \\xrightarrow{\\pi_g} \\operatorname{coker}(g) \\text{ is exact }$$$

Lean4

theorem kernelCokernelCompSequence_exact : (kernelCokernelCompSequence f g).Exact :=
  (snakeInput f g).snake_lemma

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