Commit 2025-06-16 14:23 7e92ad1b

feat(RepresentationTheory): Ind and Coind isomorphism for a finite index subgroup (#25869) Given a commutative ring k, a finite index subgroup S ≤ G, and a k-linear S-representation A, this PR defines an isomorphism $Ind_S^G(A) ≅ Coind_S^G(A).$ Given g : G and a : A, the forward map sends ⟦g ⊗ₜ[k] a⟧ to the function G → A supported at sg by ρ(s)(a) for s : S and which is 0 elsewhere. Meanwhile, the inverse sends f : G → A to ∑ᵢ ⟦gᵢ ⊗ₜ[k] f(gᵢ)⟧ for 1 ≤ i ≤ n, where g₁, ..., gₙ is a set of right coset representatives of S.