π_comp_H1Iso_hom — Mathlib

English

For trivial A, π A 1 ≫ (H1Iso A).hom equals (isoCycles₁ A).hom ≫ (shortComplexH1 A).moduleCatLeftHomologyData.π.

Русский

Для тривиального A композиция π A 1 затем гомоморфизм H1Iso(A) равна композиции izoCycles₁(A).hom с π модуля leftHomologyData.

LaTeX

$$$\\pi A 1 \\;\\circ\\; (H1Iso A).hom = (\\mathrm{isoCycles}_1 A).hom \\;\\circ\\; (\\text{shortComplexH1 }A).moduleCatLeftHomologyData.\\pi$$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem π_comp_H1Iso_hom :
    π A 1 ≫ (H1Iso A).hom = (isoCycles₁ A).hom ≫ (shortComplexH1 A).moduleCatLeftHomologyData.π := by
  simp [H1Iso, isoCycles₁, π, HomologicalComplex.homologyπ, leftHomologyπ]

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