English
The (normalized) scalar product of characters equals the dimension of the space of G-equivariant maps: (1/|G|) Σ_g χ_W(g) χ_V(g^{-1}) = finrank_G(V→W).
Русский
Пусть скалярное произведение характеров равно размерности пространства G-экваритантных отображений: (1/|G|) Σ_g χ_W(g) χ_V(g^{-1}) = finrank_G(V→W).
LaTeX
$$$\frac{1}{|G|} \sum_{g \in G} W.\chi(g) \cdot V.\chi(g^{-1}) = \operatorname{finrank}_k(\mathrm{Hom}_G(V,W)).$$$
Lean4
/-- If `V` are `W` are finite-dimensional representations of a finite group, then the
scalar product of their characters is equal to the dimension of the space of
equivariant maps from `V` to `W`.
-/
theorem scalar_product_char_eq_finrank_equivariant (V W : FDRep k G) :
⅟(Fintype.card G : k) • ∑ g : G, W.character g * V.character g⁻¹ = Module.finrank k (V ⟶ W) :=
by
conv_lhs => congr; rfl; congr; rfl; intro _;
rw [mul_comm, ← FDRep.char_linHom]
-- The scalar product is the character of `Hom(V, W).`
rw [FDRep.average_char_eq_finrank_invariants, ←
LinearEquiv.finrank_eq (Representation.linHom.invariantsEquivFDRepHom V W), of_ρ']
simp only [FGModuleCat.of_carrier]
-- The average over the group of the character of a representation equals the dimension of the
-- space of invariants, and the space of invariants of `Hom(W, V)` is the subspace of
--`G`-equivariant linear maps, `Hom_G(W, V)`.
