Commit 2025-05-12 19:39 3bb84d74

feat(RepresentationTheory): Add coinduced representations (#24732) Given a commutative ring k, a monoid homomorphism φ : G →* H, and a k-linear G-representation A, this file introduces the coinduced representation $Coind^H_G(A)$ of A as an H-representation. By coind φ A we mean the submodule of functions H → A such that for all g : G, h : H, f (φ g * h) = ρ g (f h). We define a representation of H on this submodule by sending h : H and f : coind φ A to the function H → A sending h₁ to f (h₁ * h). Alternatively, we could define $Coind_G^H(A)$ as the morphisms $Hom(k[H], A)$ in the category Rep k G, which we equip with the H-representation sending h : H and f : k[H] ⟶ A to the representation morphism sending r · h₁ to r • f (h₁ * h). We include this definition as coindHom φ A and prove the two representations are isomorphic. We also prove that the restriction functor Rep k H ⥤ Rep k G along φ is left adjoint to the coinduction functor and hence that the coinduction functor preserves limits.