English
The sum of conjugates yields a k[G]-linear map from W to V; more precisely, π.sumOfConjugatesEquivariant is defined as MonoidAlgebra.equivariantOfLinearOfComm (π.sumOfConjugates G) with the indicated equivariance data.
Русский
Сумма конъюгатов даёт k[G]-линейное отображение W → V; конкретно, sumOfConjugatesEquivariant определяется как MonoidAlgebra.equivariantOfLinearOfComm (π.sumOfConjugates G) с заданной эквиарияцией.
LaTeX
$$$\text{sumOfConjugatesEquivariant} : W \to_{\ MonoidAlgebra k G} V := \ text{MonoidAlgebra.equivariantOfLinearOfComm } (π.sumOfConjugates G) \!$$$
Lean4
/-- In fact, the sum over `g : G` of the conjugate of `π` by `g` is a `k[G]`-linear map.
-/
def sumOfConjugatesEquivariant : W →ₗ[MonoidAlgebra k G] V :=
MonoidAlgebra.equivariantOfLinearOfComm (π.sumOfConjugates G) fun g v =>
by
simp only [sumOfConjugates_apply, Finset.smul_sum, conjugate_apply]
refine Fintype.sum_bijective (· * g) (Group.mulRight_bijective g) _ _ fun i ↦ ?_
simp only [smul_smul, single_mul_single, mul_inv_rev, mul_inv_cancel_left, one_mul]
