English
Noether's inflation construction provides, for a group homomorphism f: G → H, a natural transformation from the functor A ↦ H^n(H, A) to the functor A ↦ H^n(G, Res_f A). In other words, there is a canonical, natural way to compare cohomology when restricting along f.
Русский
Для гомоморфа группы f: G → H существует естественное преобразование между функторами A ↦ H^n(H, A) и A ↦ H^n(G, Res_f A), то есть косвенно по ограничению действия по f.
LaTeX
$$$\mathrm{Inf}_f^n:\; H^n(H, A)\to H^n(G,\mathrm{Res}_f A).$$$
Lean4
/-- Given a group homomorphism `f : G →* H`, this is a natural transformation between the functors
sending `A : Rep k H` to `Hⁿ(H, A)` and to `Hⁿ(G, Res(f)(A))`. -/
@[simps]
noncomputable def resNatTrans (n : ℕ) : functor k H n ⟶ Action.res (ModuleCat k) f ⋙ functor k G n
where
app X := map f (𝟙 _) n
naturality {X Y}
φ := by
simp [← cancel_epi (groupCohomology.π _ n), ← HomologicalComplex.cyclesMap_comp_assoc, ← cochainsMap_comp,
congr (MonoidHom.id_comp _) cochainsMap, congr (MonoidHom.comp_id _) cochainsMap,
Category.id_comp (X := (Action.res _ _).obj _)]
