cochainsMap_f_3_comp_cochainsIso₃

English

In degree 3, the compatibility between cocyclesMap and cochainsMap extends with cochainsIso₃, again expressing naturality of the construction across degrees.

Русский

В градусе 3 совместимость cocyclesMap и cochainsMap распространяется на cochainsIso₃, подчеркивая естественность конструкций во всех степенях.

LaTeX

$$$$(\\\\mathrm{cochainsMap} f φ).f 3 \\\\circ (\\\\mathrm{cochainsIso}₃ B).hom = (\\\\mathrm{cochainsIso}₃ A).hom \\\\circ (\\\\mathrm{cochainsMap} f φ)$$$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem cochainsMap_f_3_comp_cochainsIso₃ :
    (cochainsMap f φ).f 3 ≫ (cochainsIso₃ B).hom = (cochainsIso₃ A).hom ≫ cochainsMap₃ f φ :=
  by
  ext x g
  change φ.hom (x _) = φ.hom (x _)
  rcongr x
  fin_cases x <;> rfl

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