cocyclesMap_comp_isoCocycles₁_hom

English

The cocycle map and the isomorphism on cocycles commute up to equality.

Русский

Кокайклово отображение и изоморфизм кокайклов коммутируют до тождества.

LaTeX

$$$ (\mathrm{mapCocycles}_1 f\phi) \circ (\mathrm{isoCocycles}_1 B)^\mathrm{hom} = (\mathrm{isoCocycles}_1 A)^\mathrm{hom} \circ \mathrm{mapCocycles}_1 f\phi $$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem cocyclesMap_comp_isoCocycles₁_hom :
    cocyclesMap f φ 1 ≫ (isoCocycles₁ B).hom = (isoCocycles₁ A).hom ≫ mapCocycles₁ f φ := by
  simp [← cancel_mono (moduleCatLeftHomologyData (shortComplexH1 B)).i, mapShortComplexH1,
    cochainsMap_f_1_comp_cochainsIso₁ f]

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