English
Let k be a commutative ring, G and H groups, and A, B representations of G and H over k. For a group homomorphism f: G →* H and a representation morphism φ: A → Res(f)(B), there is a canonical map on the nth cycles Z_n(G,A) → Z_n(H,B) for every n ≥ 0, written cyclesMap(f, φ, n). This construction is functorial in (f, φ) and compatible with composition and identities.
Русский
Пусть k — коммутативное кольцо, G и H — группы, A и B — представления над k. Для гомоморфизма групп f: G →* H и морфизма представлений φ: A → Res(f)(B) существует каноническая карта на n-ых циклах Z_n(G,A) → Z_n(H,B) для каждого n ≥ 0, обозначаемая cyclesMap(f, φ, n). Эта конструкция естественна по отношению к (f, φ) и совместима с композициями и единицами.
LaTeX
$$$\mathrm{cyclesMap}(f, \phi, n) : \mathrm{Z}_n(G,A) \longrightarrow \mathrm{Z}_n(H,B).$$$
Lean4
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : A ⟶ Res(f)(B)`,
this is the induced map `Zₙ(G, A) ⟶ Zₙ(H, B)` sending `∑ aᵢ·gᵢ : Gⁿ →₀ A` to
`∑ φ(aᵢ)·(f ∘ gᵢ) : Hⁿ →₀ B`. -/
noncomputable abbrev cyclesMap (n : ℕ) : groupHomology.cycles A n ⟶ groupHomology.cycles B n :=
HomologicalComplex.cyclesMap (chainsMap f φ) n
