chainsMap_comp — Mathlib

English

The composition of identity maps under chainsMap equals the chainsMap of the composition: chainsMap(id, φ ≫ ψ) = chainsMap(id, φ) ≫ chainsMap(id, ψ).

Русский

Сочетание идентичности по цепной карте даёт цепную карту композиции: chainsMap(id, φ ≫ ψ) = chainsMap(id, φ) ≫ chainsMap(id, ψ).

LaTeX

$$chainsMap (MonoidHom.id G) (φ ≫ ψ) = chainsMap (MonoidHom.id G) φ ≫ chainsMap (MonoidHom.id G) ψ$$

Lean4

theorem chainsMap_comp {G H K : Type u} [Group G] [Group H] [Group K] {A : Rep k G} {B : Rep k H} {C : Rep k K}
    (f : G →* H) (g : H →* K) (φ : A ⟶ (Action.res _ f).obj B) (ψ : B ⟶ (Action.res _ g).obj C) :
    chainsMap (g.comp f) (φ ≫ (Action.res _ f).map ψ) = chainsMap f φ ≫ chainsMap g ψ :=
  by
  ext
  simp [chainsMap_f, Function.comp_assoc]

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