English
The map sumOfConjugatesEquivariant is defined so that, for each v ∈ W, its value equals the sum over g ∈ G of the conjugate π^g applied to v, viewed as a linear map over MonoidAlgebra k G.
Русский
Отображение sumOfConjugatesEquivariant задаётся так, что для каждого v ∈ W его значение равно сумме по g ∈ G от π^g(v), рассматриваемой как линейное отображение над MonoidAlgebra k G.
LaTeX
$$$\text{sumOfConjugatesEquivariant } G π = π.sumOfConjugates G \text{ как } W \to_{\ MonoidAlgebra k G} V$$$
Lean4
theorem equivariantProjection_condition (hcard : IsUnit (Fintype.card G : k)) (h : ∀ v : V, π (i v) = v) (v : V) :
(π.equivariantProjection G) (i v) = v :=
by
rw [equivariantProjection_apply]
simp only [conjugate_i π i h]
rw [Finset.sum_const, Finset.card_univ, ← Nat.cast_smul_eq_nsmul k, smul_smul, Ring.inverse_mul_cancel _ hcard,
one_smul]
