map_id_comp — Mathlib

English

The identity on the domain G respects composition: map (Id_G) (φ ≫ ψ) n = map Id_G φ n ≫ map Id_G ψ n.

Русский

Тождество на области G сохраняет композицию: map(Id_G) (φ ≫ ψ) n = map(Id_G) φ n ≫ map(Id_G) ψ n.

LaTeX

$$$\mathrm{map}(\mathrm{Id}_G, \phi \circ \psi, n) = \mathrm{map}(\mathrm{Id}_G, \phi, n) \circ \mathrm{map}(\mathrm{Id}_G, \psi, n)$$$

Lean4

theorem map_id_comp {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) (n : ℕ) :
    map (MonoidHom.id G) (φ ≫ ψ) n = map (MonoidHom.id G) φ n ≫ map (MonoidHom.id G) ψ n := by
  rw [map, chainsMap_id_comp, HomologicalComplex.homologyMap_comp]

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