π_descHomology — Mathlib

English

For any k: S.cycles → A with S.toCycles ≫ k = 0, the composition S.homologyπ ≫ S.descHomology(k,hk) equals k.

Русский

Для любого k: S.cycles → A с условием S.toCycles ≫ k = 0 композиция S.homologyπ ≫ S.descHomology(k,hk) равна k.

LaTeX

$$$S.homologyπ \circ S.descHomology(k,hk) = k \quad\text{for } k: S.cycles \to A,\; (S.toCycles \circ k = 0)$$$

Lean4

@[reassoc (attr := simp)]
theorem π_descHomology (k : S.cycles ⟶ A) (hk : S.toCycles ≫ k = 0) : S.homologyπ ≫ S.descHomology k hk = k :=
  Cofork.IsColimit.π_desc S.homologyIsCokernel

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