English
Given f: H →* K and g: G →* H with φ and ψ, the cocyclesMap for f.comp g equals the composition cocyclesMap f φ and cocyclesMap g ψ at degree n. This is the naturality under composition of the group homomorphisms.
Русский
Пусть f: H →* K и g: G →* H; приведённые φ и ψ. Отображение cocyclesMap для f∘g равно композиции cocyclesMap f φ и cocyclesMap g ψ в степени n.
LaTeX
$$$\\\\cocyclesMap(f\\\\cdot g) (((Action.res\\\\_ g).map φ) \\\\gg ψ) n \\\\;=\n \\\\cocyclesMap f φ n \\\\circ \\\\cocyclesMap g ψ n$$$
Lean4
@[reassoc]
theorem cocyclesMap_comp {G H K : Type u} [Group G] [Group H] [Group K] {A : Rep k K} {B : Rep k H} {C : Rep k G}
(f : H →* K) (g : G →* H) (φ : (Action.res _ f).obj A ⟶ B) (ψ : (Action.res _ g).obj B ⟶ C) (n : ℕ) :
cocyclesMap (f.comp g) ((Action.res _ g).map φ ≫ ψ) n = cocyclesMap f φ n ≫ cocyclesMap g ψ n := by
simp [cocyclesMap, ← HomologicalComplex.cyclesMap_comp, ← cochainsMap_comp]
