English
For a normal subgroup S ≤ G, there is a natural transformation between the functors A ↦ H^n(G/S, A^S) and A ↦ H^n(G, A), i.e., a canonical map that is natural in A.
Русский
Для нормальной подгруппы S ≤ G существует естественное преобразование между функторaми A ↦ H^n(G/S, A^S) и A ↦ H^n(G, A), то есть канонический переход в когомологии, зависит естественным образом от A.
LaTeX
$$$\mathrm{Inf}_S^G:n\mapsto H^n(G/S, A^S) \Rightarrow H^n(G, A).$$$
Lean4
/-- Given a normal subgroup `S ≤ G`, this is a natural transformation between the functors
sending `A : Rep k G` to `Hⁿ(G ⧸ S, A^S)` and to `Hⁿ(G, A)`. -/
@[simps]
noncomputable def infNatTrans (S : Subgroup G) [S.Normal] (n : ℕ) :
quotientToInvariantsFunctor k S ⋙ functor k (G ⧸ S) n ⟶ functor k G n
where
app A := map (QuotientGroup.mk' S) (subtype _ _ <| le_comap_invariants A.ρ S) n
naturality {X Y}
φ :=
by
simp only [Functor.comp_map, functor_map, ← cancel_epi (groupCohomology.π _ n),
HomologicalComplex.homologyπ_naturality_assoc, HomologicalComplex.homologyπ_naturality,
← HomologicalComplex.cyclesMap_comp_assoc, ← cochainsMap_comp]
congr 1
