mapCycles₁_comp_i — Mathlib

English

The induced map on cycles commutes with the connecting morphism i in the left-hand homology data, i.e., mapCycles₁ f φ followed by i_B equals i_A followed by chainsMap₁ f φ.

Русский

У индуцированного отображения циклов на левой части отображения связности выполняется коммутация с i: mapCycles₁ f φ ∘ i_B = i_A ∘ chainsMap₁ f φ.

LaTeX

$$$ mapCycles_1(f, \varphi) \circ i_B = i_A \circ (chainsMap_1(f, \varphi)) $$$

Lean4

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

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