shortComplexH0_exact — Mathlib

English

The short complex H0(A) is exact, i.e., the image of the first map equals the kernel of the second map.

Русский

Короткий комплекс H0(A) точен: образ первого отображения равен ядеру второго отображения.

LaTeX

$$$\operatorname{im}f = \ker g\quad\text{for } f,g\text{ the two maps in }(shortComplexH0\ A)$$$

Lean4

theorem shortComplexH0_exact : (shortComplexH0 A).Exact :=
  by
  rw [ShortComplex.moduleCat_exact_iff]
  intro x (hx : Coinvariants.mk _ _ = 0)
  rw [Coinvariants.mk_eq_zero, ← range_d₁₀_eq_coinvariantsKer] at hx
  rcases hx with ⟨x, hx, rfl⟩
  use x
  rfl

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