mapShortComplexH2_id_comp — Mathlib

English

The identity on the source G composes with φ and ψ as expected: mapShortComplexH2(id_G)(φ ≫ ψ) = mapShortComplexH2(id_G) φ ≫ mapShortComplexH2(id_G) ψ.

Русский

Единичное отображение на G компонуется с φ и ψ как положено: mapShortComplexH2(id_G)(φ ≫ ψ) = mapShortComplexH2(id_G) φ ∘ mapShortComplexH2(id_G) ψ.

LaTeX

$$$ mapShortComplexH2(\mathrm{id}_G)(\varphi \;\mathrm{≫}\; \psi) = mapShortComplexH2(\mathrm{id}_G)\varphi \;\mathrm{≫}\; mapShortComplexH2(\mathrm{id}_G)\psi $$$

Lean4

theorem mapShortComplexH2_id_comp {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) :
    mapShortComplexH2 (MonoidHom.id G) (φ ≫ ψ) =
      mapShortComplexH2 (MonoidHom.id G) φ ≫ mapShortComplexH2 (MonoidHom.id G) ψ :=
  mapShortComplexH2_comp (MonoidHom.id G) (MonoidHom.id G) _ _

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