cocyclesMap_comp_isoCocycles₂_hom

English

The two routes via cocyclesMap and isoCocycles₂_hom agree.

Русский

Два маршрута через cocyclesMap и isoCocycles₂_hom сходятся.

LaTeX

$$$ cocyclesMap(f,\phi,2) \circ (isoCocycles_2 B) .hom = (isoCocycles_2 A) .hom \circ mapCocycles_2(f,\phi) $$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem cocyclesMap_comp_isoCocycles₂_hom :
    cocyclesMap f φ 2 ≫ (isoCocycles₂ B).hom = (isoCocycles₂ A).hom ≫ mapCocycles₂ f φ := by
  simp [← cancel_mono (moduleCatLeftHomologyData (shortComplexH2 B)).i, mapShortComplexH2,
    cochainsMap_f_2_comp_cochainsIso₂ f]

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