exact_shortComplex — Mathlib

English

If h is a pushout in an Abelian category, then the associated short complex is exact.

Русский

Если h — пушоут в абеловой категории, связанная короткая последовательность точна.

LaTeX

$$$\\\\text{IsPushout}(t,l,r,b) \\\\Rightarrow \\\\text{ShortComplex}(t,l,r,b) \\\\text{ is exact }.$$$

Lean4

theorem exact_shortComplex (h : IsPushout t l r b) : h.shortComplex.Exact :=
  h.shortComplex.exact_of_g_is_cokernel h.isColimitCokernelCofork

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