isoHomologyπ_hom_inv_id — Mathlib

English

The composition homologyπ with the inverse of isoHomologyπ yields the identity on the homology group.

Русский

Композиция homologyπ с обратной стороны isoHomologyπ дает тождество на гомологии.

LaTeX

$$$$ homology_j \\circ (isoHomologyπ_i_j)^{-1} = \\mathrm{Id} $$$$

Lean4

@[reassoc (attr := simp)]
theorem isoHomologyπ_hom_inv_id : K.homologyπ j ≫ (K.isoHomologyπ i j hi h).inv = 𝟙 _ :=
  (K.isoHomologyπ i j hi h).hom_inv_id

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