Commit 2025-05-30 11:19 5db41a82

feat(RepresentationTheory/*): representations on Finsupp (#21732) Given a type α and a representation A, this PR defines Rep.finsupp, the representation defined pointwise on α →₀ A, and specializes this to Rep.free, when A = leftRegular k G. We define Rep.freeLiftLEquiv α A, the k-linear equivalence between functions α → A and representation morphisms Rep.free k G α ⟶ A. We also define representation isomorphisms (α →₀ A) ⊗ B ≅ (A ⊗ B) →₀ α ≅ A ⊗ (α →₀ B) given representations A and B, and finally k[G] ⊗ (α →₀ k) ≅ free k G α where α →₀ k is equipped with the trivial representation.