English
For a normal subgroup S ≤ G, there is a functor sending a G-representation to a G/S-representation on its S-coinvariants, with action induced by restriction and quotient.
Русский
Пусть S ≤ G нормальная. Существует функтор, отправляющий G-представление в представление над G/S, действующее через коинварианты по S; отображение гомоморфизмов строится через ограничение и косвенную факторизацию к G/S.
LaTeX
$$$\\mathrm{Rep\\;k\\;G} \\;\\xrightarrow{\\text{quotientToCoinvariantsFunctor}(S)}\\; \\mathrm{Rep\\;k\\; (G/S)} \\\\ Obj(X) = X.quotientToCoinvariants S, \\ map(f) = (coinvariantsFunctor\\;k\\;S).map((Action.res\\ _ S.subtype).map f)$$$
Lean4
/-- Given a normal subgroup `S ≤ G`, this is the functor sending a `G`-representation `A` to the
`G ⧸ S`-representation it induces on `A_S`. -/
@[simps obj_V map_hom]
noncomputable def quotientToCoinvariantsFunctor (S : Subgroup G) [S.Normal] : Rep k G ⥤ Rep k (G ⧸ S)
where
obj X := X.quotientToCoinvariants S
map {X Y}
f :=
{ hom := (coinvariantsFunctor k S).map ((Action.res _ S.subtype).map f)
comm g := QuotientGroup.induction_on g fun g => by ext; simp [ModuleCat.endRingEquiv, hom_comm_apply] }
