mapShortComplexH1_id_comp — Mathlib

English

Let φ and ψ be as above; the H¹-map with the identity on G preserves composition in the obvious way.

Русский

Пусть φ и ψ заданы; отображение H¹, соответствующее тождественному гомоморфизму на G, сохраняет композицию φ и ψ в ожидаемом виде.

LaTeX

$$$\operatorname{mapShortComplexH1}(\mathrm{id}_G)(\varphi \circ \psi) = \operatorname{mapShortComplexH1}(\mathrm{id}_G)\varphi \circ \operatorname{mapShortComplexH1}(\mathrm{id}_G)\psi$$$

Lean4

@[reassoc]
theorem mapShortComplexH1_id_comp {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) :
    mapShortComplexH1 (MonoidHom.id G) (φ ≫ ψ) =
      mapShortComplexH1 (MonoidHom.id G) φ ≫ mapShortComplexH1 (MonoidHom.id G) ψ :=
  rfl

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