English
For a group homomorphism f: G →* H and a representation morphism φ: Res_f(A) ⟶ B, there is a canonical induced map on n-cocycles Z^n(H,A) → Z^n(G,B) given by x ↦ φ ∘ x ∘ f. This is denoted cocyclesMap(n).
Русский
Для группоподобного гомоморфизма f: G →* H и отображения φ: Res_f(A) ⟶ B существует канонически индуцированное отображение на n-ку cocycles: Z^n(H,A) → Z^n(G,B) по формуле x ↦ φ ∘ x ∘ f.
LaTeX
$$$\\\\cocyclesMap(n): \\; Z^n(H,A) \\\\longrightarrow Z^n(G,B):\\; x \\mapsto (g_1,\\\\dots,g_n) \\\\mapsto φ(x(f(g_1),\\\\dots,f(g_n)))$$$
Lean4
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : Res(f)(A) ⟶ B`,
this is the induced map `Zⁿ(H, A) ⟶ Zⁿ(G, B)` sending `x : Hⁿ → A` to
`(g : Gⁿ) ↦ φ (x (f ∘ g))`. -/
noncomputable abbrev cocyclesMap (n : ℕ) : groupCohomology.cocycles A n ⟶ groupCohomology.cocycles B n :=
HomologicalComplex.cyclesMap (cochainsMap f φ) n
