H2Iso — Mathlib

English

The second homology H2(A) is canonically isomorphic to the left-hand homology data of the 2nd complex, i.e., H2(A) ≅ (shortComplexH2 A).moduleCatLeftHomologyData.H.

Русский

Вторая гомология H2(A) естественным образом изоморфна левому гомологическому данным 2-го комплекса: H2(A) ≅ (shortComplexH2 A).moduleCatLeftHomologyData.H.

LaTeX

$$$H_2(A) \\cong (shortComplexH2 A).moduleCatLeftHomologyData.H$$$

Lean4

/-- The 2nd group homology of `A`, defined as the 2nd homology of the complex of inhomogeneous
chains, is isomorphic to `cycles₂ A ⧸ boundaries₂ A`, which is a simpler type. -/
def H2Iso : H2 A ≅ (shortComplexH2 A).moduleCatLeftHomologyData.H :=
  (leftHomologyIso _).symm ≪≫ (leftHomologyMapIso' (isoShortComplexH2 A) _ _)

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