English
For a finite group G and a G-representation X in FDRep k G, the G-equivariant linear map from the right regular representation to X sending the identity vector to v ∈ X is given by f ↦ ∑_{s∈G} f(s) · (ρ(s^{-1})v).
Русский
Для конечной группы G и представления X в FDRep k G существует G-эквивariant-линейный отображение от правого регулярного представления к X, который отправляет базисный вектор единицы в v ∈ X и задан формулой f ↦ ∑_{s∈G} f(s) · (ρ(s^{-1})v).
LaTeX
$$$[\text{Fintype } G] \ {X : FDRep k G} \ {v \in X.V.carrier} \\sumSMulInv : (G \to k) \to_ℓ[k] X,\quad (toFun f) = \sum_{s \in G} f(s) \cdot (X.\rho(s^{-1}) v).$$
Lean4
/-- For `v : X` and `G` a finite group, the `G`-equivariant linear map from the right
regular representation `rightFDRep` to `X` sending `single 1 1` to `v`. -/
@[simps]
def sumSMulInv [Fintype G] {X : FDRep k G} (v : X) : (G → k) →ₗ[k] X
where
toFun f := ∑ s : G, (f s) • (X.ρ s⁻¹ v)
map_add' _ _ := by simp [add_smul, sum_add_distrib]
map_smul' _ _ := by simp [smul_sum, smul_smul]
