mapCocycles₂_comp_i — Mathlib

English

The mapCocycles₂ interacts with the i-inclusion: composition with i matches cochainsMap₂ via the appropriate inclusions.

Русский

Отображение mapCocycles₂ совместимо с включением i и cochainsMap₂.

LaTeX

$$$ mapCocycles_2(f,\varphi) \circ i_B = i_A \circ cochainsMap_2(f,\varphi) $$$

Lean4

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

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