toCocycles_comp_isoCocycles₂_hom

English

The first cocycles isomorphism composed with the i-map from the H2 short complex equals the iCocycles₂ A composed with the second cochains isomorphism. This confirms the commutativity of the relevant square involving i-maps.

Русский

Изоморфизм кокози₁ компонуется с i и-маршрутом из H2-быстрого комплекса до iCocycles₂ A через cocycles₂; выражает коммутативность квадрата.

LaTeX

$$$(\text{isoCocycles}_{2}(A))^{\mathrm{hom}} \circ (shortComplexH2(A)).moduleCatLeftHomologyData.i = iCocycles(A,2) \circ (cochainsIso_{2}(A)).hom$$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem toCocycles_comp_isoCocycles₂_hom :
    toCocycles A 1 2 ≫ (isoCocycles₂ A).hom = (cochainsIso₁ A).hom ≫ (shortComplexH2 A).moduleCatLeftHomologyData.f' :=
  by simp [← cancel_mono (shortComplexH2 A).moduleCatLeftHomologyData.i, comp_d₁₂_eq, shortComplexH2_f]

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