Commit 2025-06-05 17:13 d5f3cef4
View on Github →feat(RepresentationTheory/Coinvariants): the G ⧸ S-representation on A_S for A : Rep k G (#22652)
Given a G-representation A and a normal subgroup S ≤ G, this PR defines the G / S-representation induced on A_S, the coinvariants of ρ restricted to S. It also defines the short exact sequence of G-representations
0 ⟶ I(S)A ⟶ A ⟶ A_S ⟶ 0
where I(S)A is the submodule of A generated by elements of the form ρ(s)(a) - a for s : S, a : A.