English
Define a k[G]-linear projection of W onto V by averaging the g-conjugates of π and multiplying by the inverse of |G| in k; this projection is a left inverse of i when π i = id_V and |G| is invertible in k.
Русский
Определяем k[G]-линейную проекцию из W в V как усреднение конъюгатов π и умножение на 1/|G|; эта проекция является обратной слева к i, если π i = id_V и |G| обращаемо в k.
LaTeX
$$$\text{equivariantProjection} : W \to_{\ MonoidAlgebra k G} V :=\ \mathrm{Ring.inverse} (|G| : k) \cdot π.sumOfConjugatesEquivariant G$$$
Lean4
/-- We construct our `k[G]`-linear retraction of `i` as
$$ \frac{1}{|G|} \sum_{g \in G} g⁻¹ • π(g • -). $$
-/
def equivariantProjection : W →ₗ[MonoidAlgebra k G] V :=
Ring.inverse (Fintype.card G : k) • π.sumOfConjugatesEquivariant G
