π_comp_H2Iso_hom — Mathlib

English

Compatibility statement expressing the equality of two constructions of the H2 isomorphism under different identifications.

Русский

Соответствующее утверждение о совместимости двух конструирований изоморфизма H2 при разных обозначениях.

LaTeX

$$Eq (H2Iso A) = (composition of canonical left-homology identifications).$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem π_comp_H2Iso_hom :
    π A 2 ≫ (H2Iso A).hom = (isoCycles₂ A).hom ≫ (shortComplexH2 A).moduleCatLeftHomologyData.π := by
  simp [H2Iso, isoCycles₂, π, HomologicalComplex.homologyπ, leftHomologyπ]

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