H1Iso — Mathlib

English

The first group cohomology H1 A is isomorphic to the left homology H of the short complex associated to the inhomogeneous cochains.

Русский

Первая когомология группы H1 A изоморфна левой одногомологий короткого комплекса связанных с негомогенными цепочками.

LaTeX

$$def H1Iso : H1 A ≅ (shortComplexH1 A).moduleCatLeftHomologyData.H$$

Lean4

/-- The 1st group cohomology of `A`, defined as the 1st cohomology of the complex of inhomogeneous
cochains, is isomorphic to `cocycles₁ A ⧸ coboundaries₁ A`, which is a simpler type. -/
def H1Iso : H1 A ≅ (shortComplexH1 A).moduleCatLeftHomologyData.H :=
  (leftHomologyIso _).symm ≪≫ (leftHomologyMapIso' (isoShortComplexH1 A) _ _)

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