English
For a group homomorphism f: G → H and a representation A of H over k, there is a natural transformation between the functors A ↦ H_n(G, Res_f A) and A ↦ H_n(H, A) for all n ≥ 0. The component at A is given by the map on homology induced by f on chains.
Русский
Для гомоморфизма групп f: G → H и представления A над k для группы H существует естественная трансформация между функторами A ↦ H_n(G, Res_f A) и A ↦ H_n(H, A) для всех n ≥ 0. Компонента для A задаётся отображением на гомологии, индуцированным f на цепях.
LaTeX
$$$\mathrm{cores}_n^f: H_n(G, \mathrm{Res}_f(-)) \Rightarrow H_n(H, -)$$$
Lean4
/-- Given a group homomorphism `f : G →* H`, this is a natural transformation between the functors
sending `A : Rep k H` to `Hₙ(G, Res(f)(A))` and to `Hₙ(H, A)`. -/
@[simps]
noncomputable def coresNatTrans (n : ℕ) : Action.res (ModuleCat k) f ⋙ functor k G n ⟶ functor k H n
where
app X := map f (𝟙 _) n
naturality {X Y}
φ := by
simp [← cancel_epi (groupHomology.π _ n), ← HomologicalComplex.cyclesMap_comp_assoc, ← chainsMap_comp,
congr (MonoidHom.id_comp _) chainsMap, congr (MonoidHom.comp_id _) chainsMap,
Category.id_comp (X := (Action.res _ _).obj _)]
