Commit 2025-05-31 08:21 d36f2cbe

feat(RepresentationTheory/Coinvariants): coinvariants of a representation (#21733) Given a commutative ring k and a monoid G, this PR introduces the coinvariants of a k-linear G-representation (V, ρ). We first define Representation.Coinvariants.ker, the submodule of V generated by elements of the form ρ g x - x for x : V, g : G. Then the coinvariants of (V, ρ) are the quotient of V by this submodule. We show that the functor sending a representation to its coinvariants is left adjoint to the functor equipping a module with the trivial representation.