English
Let A be a G-module representation over k. The two canonical ways of obtaining a map from the H1 component to the left H1 data agree; equivalently, the projection π at degree 1 followed by the H1-isomorphism equals the cocycle map followed by the left-Homology projection.
Русский
Пусть A --- представление G над кольцом k. Два канонических способа получения отображения из H1 в левую гомологическую часть совпадают; эквивалентно тому, что проекция π в степени 1, затем гомоморфизм H1Isomorphism, равны отображению кокасков, затем проекции левой гомологии.
LaTeX
$$$\\pi_A(1) \\circ (H1A)^{\\mathrm{hom}} = (\\mathrm{isoCocycles}_1 A)^{\\mathrm{hom}} \\circ (shortComplexH1 A)^{\\mathrm{moduleLeftHomologyData}}_{\\pi}$$$
Lean4
@[reassoc (attr := simp), elementwise (attr := simp)]
theorem π_comp_H1Iso_hom :
π A 1 ≫ (H1Iso A).hom = (isoCocycles₁ A).hom ≫ (shortComplexH1 A).moduleCatLeftHomologyData.π := by
simp [H1Iso, isoCocycles₁, π, HomologicalComplex.homologyπ, leftHomologyπ]
