H2Iso — Mathlib

English

There is a canonical isomorphism between H2(A) and the left homology of the short complex H2(A).

Русский

Существует канонический изоморфизм между H2(A) и левой гомологией краткого комплекса H2(A).

LaTeX

$$H2Iso : H2 A ≅ (shortComplexH2 A).moduleCatLeftHomologyData.H$$

Lean4

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

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