mapCocycles₁_comp_i — Mathlib

English

A compatibility relation between the cocycle map and the standard inclusion is satisfied.

Русский

Существует совместимость отображения кокайкл с обычным включением.

LaTeX

$$$ mapCocycles_1(f,\varphi) \circ i_B = i_A \circ cochainsMap_1(f,\varphi) $$$

Lean4

@[reassoc, elementwise]
theorem mapCocycles₁_comp_i :
    mapCocycles₁ f φ ≫ (shortComplexH1 B).moduleCatLeftHomologyData.i =
      (shortComplexH1 A).moduleCatLeftHomologyData.i ≫ cochainsMap₁ f φ :=
  by simp

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