English
As above, for π: W → V and finite G, the equivariant version satisfies (SumOfConjugatesEquivariant G π) v = ∑_{g∈G} (π.conjugate g) v.
Русский
Как выше: для π: W → V и конечной группы G, эквиаривантная версия удовлетворяет (SumOfConjugatesEquivariant G π) v = ∑_{g∈G} (π^g) v.
LaTeX
$$$\\text{SumOfConjugatesEquivariant } G π \; v = \\sum_{g : G} π.conjugate g v$$$
Lean4
theorem exists_leftInverse_of_injective (f : V →ₗ[MonoidAlgebra k G] W) (hf : LinearMap.ker f = ⊥) :
∃ g : W →ₗ[MonoidAlgebra k G] V, g.comp f = LinearMap.id :=
by
let A := MonoidAlgebra k G
letI : Module k W := .compHom W (algebraMap k A)
letI : Module k V := .compHom V (algebraMap k A)
have := IsScalarTower.of_compHom k A W
have := IsScalarTower.of_compHom k A V
obtain ⟨φ, hφ⟩ :=
(f.restrictScalars k).exists_leftInverse_of_injective <| by
simp only [hf, Submodule.restrictScalars_bot, LinearMap.ker_restrictScalars]
refine ⟨φ.equivariantProjection G, DFunLike.ext _ _ ?_⟩
exact φ.equivariantProjection_condition G _ (.mk0 _ <| NeZero.ne _) <| DFunLike.congr_fun hφ
