toCycles_comp_isoCycles₂_hom — Mathlib

English

The map toCycles in degree 3→2 composed with isoCycles₂.hom equals chainsIso₃.hom composed with the f' map from shortComplexH2.

Русский

К отношению toCycles в степенях 3→2 композиция с isoCycles₂.hom равна chainsIso₃.hom, затем с f' из shortComplexH2.

LaTeX

$$$ toCycles A\ 3 2 \circ isoCycles_2 A.hom = (chainsIso_3 A).hom \circ (shortComplexH2 A).moduleCatLeftHomologyData.f'$$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem toCycles_comp_isoCycles₂_hom :
    toCycles A 3 2 ≫ (isoCycles₂ A).hom = (chainsIso₃ A).hom ≫ (shortComplexH2 A).moduleCatLeftHomologyData.f' := by
  simp [← cancel_mono (shortComplexH2 A).moduleCatLeftHomologyData.i, comp_d₃₂_eq, shortComplexH2_f]

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