Lie actions on exterior powers

An endomorphism of a module acts infinitesimally on an exterior power by applying the endomorphism to one factor at a time. This construction is linear in the endomorphism and carries commutators to commutators, hence defines a Lie algebra representation.

Main definitions

• exteriorPower.lieMap: the natural Lie action of Module.End K V on ⋀[K]^d V.

Main results

• exteriorPower.lieMap_apply_ιMulti: the action on a decomposable wedge is the sum of the terms obtained by applying the endomorphism to one factor.

References

• Highest-weight roadmap, Layer 8, where the Vinberg model of E₈ uses the sl₉ action on ⋀³(K⁹).

noncomputable def exteriorPower.lieMap {K : Type u} {V : Type v} [CommRing K] [AddCommGroup V] [Module K V] (d : ℕ) : Module.End K V →ₗ⁅K⁆ Module.End K ↥(⋀[K]^d V)

The infinitesimal action of endomorphisms on an exterior power.

Equations

• exteriorPower.lieMap d = { toLinearMap := exteriorPower.actionLinear✝ d, map_lie' := ⋯ }

@[simp]

theorem exteriorPower.lieMap_apply_ιMulti {K : Type u} {V : Type v} [CommRing K] [AddCommGroup V] [Module K V] (d : ℕ) (f : Module.End K V) (v : Fin d → V) : ((lieMap d) f) ((ιMulti K d) v) = ∑ i : Fin d, (ιMulti K d) (Function.update v i (f (v i)))

An endomorphism acts on a decomposable wedge by acting on one factor at a time.