English
For group homomorphisms f: G →* H and g: H →* K with morphisms φ and ψ, the cycles maps satisfy cyclesMap(g ∘ f, φ ≫ Res_f(ψ), n) = cyclesMap(f, φ, n) ∘ cyclesMap(g, ψ, n) for all n.
Русский
Для гомоморфизмов f: G →* H и g: H →* K с морфизмами φ и ψ тензорные карты удовлетворяют: cyclesMap(g ∘ f, φ ≫ Res_f(ψ), n) = cyclesMap(f, φ, n) ∘ cyclesMap(g, ψ, n) для всех n.
LaTeX
$$$\mathrm{cyclesMap}(g \circ f, \phi \gg \mathrm{Res}(f)(\psi), n) = \mathrm{cyclesMap}(f, \phi, n) \circ \mathrm{cyclesMap}(g, \psi, n)$$$
Lean4
@[reassoc]
theorem cyclesMap_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) (n : ℕ) :
cyclesMap (g.comp f) (φ ≫ (Action.res _ f).map ψ) n = cyclesMap f φ n ≫ cyclesMap g ψ n := by
simp [cyclesMap, ← HomologicalComplex.cyclesMap_comp, ← chainsMap_comp]
