English
For a normal subgroup S ≤ G, there is a natural transformation between the functors A ↦ H_n(G, A) and the composite functor (G ↠ G/S) with coinvariants, yielding H_n(G/S, A_S). The construction uses the quotient map and the coinvariants ker data in a functorial way, natural in A.
Русский
Для нормальной подгруппы S ≤ G существует естественная трансформация между функторaми A ↦ H_n(G, A) и композиционным функтором (G ↠ G/S) через коинварианты, давая H_n(G/S, A_S). Конструкция использует естественный отображение фактор-группы и ядро коинвариантов, естественно по A.
LaTeX
$$$\mathrm{coinfNatTrans}(S, n): H_n(G, -) \Rightarrow H_n(G/S, -_S)$$$
Lean4
/-- Given a normal subgroup `S ≤ G`, this is a natural transformation between the functors
sending `A : Rep k G` to `Hₙ(G, A)` and to `Hₙ(G ⧸ S, A_S)`. -/
@[simps]
noncomputable def coinfNatTrans (S : Subgroup G) [S.Normal] (n : ℕ) :
functor k G n ⟶ quotientToCoinvariantsFunctor k S ⋙ functor k (G ⧸ S) n
where
app A := map (QuotientGroup.mk' S) (mkQ _ _ <| Coinvariants.le_comap_ker A.ρ S) n
naturality {X Y}
φ :=
by
simp only [Functor.comp_map, functor_map, ← cancel_epi (groupHomology.π _ n),
HomologicalComplex.homologyπ_naturality_assoc, HomologicalComplex.homologyπ_naturality,
← HomologicalComplex.cyclesMap_comp_assoc, ← chainsMap_comp]
congr 1
