English
There is a standard equivalence expressing that the induced map on homology equals the homology map obtained via the cochains map, i.e., map f φ n = HomologicalComplex.homologyMap(cochainsMap f φ) n.
Русский
Существует эквивалентность: отображение на гомологии, получаемое через map f φ n, равно отображению гомологии, получаемому через cochainsMap f φ.
LaTeX
$$$\\\\map f\\\\phi n \\\\;=\\\\; \\\\mathrm{HomologicalComplex.homologyMap}\\\\left(\\\\mathrm{cochainsMap} f\\\\phi\\\\right) n$$$
Lean4
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : Res(f)(A) ⟶ B`,
this is the induced map `Hⁿ(H, A) ⟶ Hⁿ(G, B)` sending `x : Hⁿ → A` to
`(g : Gⁿ) ↦ φ (x (f ∘ g))`. -/
noncomputable abbrev map (n : ℕ) : groupCohomology A n ⟶ groupCohomology B n :=
HomologicalComplex.homologyMap (cochainsMap f φ) n
