The projections attached to the weight-space decomposition

A finite-dimensional triangularizable module M over a nilpotent Lie algebra L is the internal direct sum of its generalized weight spaces (Ado.isInternal_genWeightSpace). This file names the associated family of projections Ado.genWeightSpaceProjection, one for each weight, and records the three facts that characterise it: each projection lands in its weight space, it is the identity there and kills the other weight spaces, and the whole family sums to the identity.

The last section specialises to the root-space decomposition of a Lie algebra L with non-degenerate Killing form over its Cartan subalgebra H, where the projections acquire two further properties that the decomposition alone does not give. Root spaces are Killing-orthogonal unless the two weights are opposite, so the Killing-adjoint of the projection onto the χ-root space is the projection onto the -χ one; and each projection has trace the dimension of its root space, which for a root is 1.

Main definitions

• Ado.genWeightSpaceProjection: the projection of M onto the generalized weight space of a weight, along the sum of the other weight spaces.

Main results

• Ado.sum_genWeightSpaceProjection_apply: the projections sum to the identity.
• Ado.killingForm_genWeightSpaceProjection: κ (π_χ x) y = κ x (π_{-χ} y), so π_χ and π_{-χ} are Killing-adjoint; Ado.isAdjointPair_genWeightSpaceProjection says the same in the LinearMap.IsAdjointPair form.
• Ado.trace_genWeightSpaceProjection: the trace of a projection is the dimension of the weight space it projects onto.

Implementation notes

The projection specializes Ado.internalProjection to the internal decomposition by generalized weight spaces. Its characteristic equations and sum formula therefore share the generic internal-summand projection API, while the trace computation uses LinearMap.trace_eq_sum_trace_restrict.

DirectSum needs a DecidableEq (Weight K L M). The projection is noncomputable in any case, so that choice is made classically inside the definition instead of being carried as a hypothesis: the API is stated without any decidability assumption.

References

The projections are the working form of the "generalized weight-space decomposition" item of Layer 2 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md; the Killing-adjointness and the trace are what the Casimir eigenvalue computation of Layer 5 consumes.

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §8.1 (the root-space decomposition) and §8.2 (the Killing form pairs Lα with L_{-α} alone).

The projections of the weight-space decomposition

noncomputable def Ado.genWeightSpaceProjection (K : Type u) (L : Type v) (M : Type w) [Field K] [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [LieModule.IsTriangularizable K L M] (χ : LieModule.Weight K L M) : M →ₗ[K] M

The projection onto a generalized weight space along the sum of the other weight spaces, for a finite-dimensional triangularizable module.

Equations

• Ado.genWeightSpaceProjection K L M χ = (↑(LieModule.genWeightSpace M ⇑χ)).subtype ∘ₗ Ado.internalProjection ⋯ ⋯ χ

theorem Ado.genWeightSpaceProjection_apply_mem {K : Type u} {L : Type v} {M : Type w} [Field K] [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [LieModule.IsTriangularizable K L M] (χ : LieModule.Weight K L M) (m : M) : (genWeightSpaceProjection K L M χ) m ∈ LieModule.genWeightSpace M ⇑χ

A projection lands in the weight space it is attached to.

@[simp]

theorem Ado.genWeightSpaceProjection_apply_of_mem {K : Type u} {L : Type v} {M : Type w} [Field K] [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [LieModule.IsTriangularizable K L M] {χ : LieModule.Weight K L M} {m : M} (hm : m ∈ LieModule.genWeightSpace M ⇑χ) : (genWeightSpaceProjection K L M χ) m = m

A projection is the identity on its own weight space.

theorem Ado.genWeightSpaceProjection_apply_of_mem_of_ne {K : Type u} {L : Type v} {M : Type w} [Field K] [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [LieModule.IsTriangularizable K L M] {χ ψ : LieModule.Weight K L M} (h : ψ ≠ χ) {m : M} (hm : m ∈ LieModule.genWeightSpace M ⇑ψ) : (genWeightSpaceProjection K L M χ) m = 0

A projection kills every other weight space.

Not @[simp]: the weight ψ occurs only in the hypotheses, so simp could not instantiate it. The simp-usable consequence is Ado.genWeightSpaceProjection_apply_apply_of_ne.

@[simp]

theorem Ado.genWeightSpaceProjection_apply_apply {K : Type u} {L : Type v} {M : Type w} [Field K] [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [LieModule.IsTriangularizable K L M] (χ : LieModule.Weight K L M) (m : M) : (genWeightSpaceProjection K L M χ) ((genWeightSpaceProjection K L M χ) m) = (genWeightSpaceProjection K L M χ) m

The projections are idempotent.

@[simp]

theorem Ado.genWeightSpaceProjection_apply_apply_of_ne {K : Type u} {L : Type v} {M : Type w} [Field K] [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [LieModule.IsTriangularizable K L M] {χ ψ : LieModule.Weight K L M} (h : ψ ≠ χ) (m : M) : (genWeightSpaceProjection K L M χ) ((genWeightSpaceProjection K L M ψ) m) = 0

Projections attached to distinct weights annihilate one another.

theorem Ado.sum_genWeightSpaceProjection_apply {K : Type u} {L : Type v} {M : Type w} [Field K] [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [LieModule.IsTriangularizable K L M] (m : M) : ∑ χ : LieModule.Weight K L M, (genWeightSpaceProjection K L M χ) m = m

The projections sum to the identity: this is the weight-space decomposition, read on a single vector.

theorem Ado.mapsTo_genWeightSpaceProjection {K : Type u} {L : Type v} {M : Type w} [Field K] [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [LieModule.IsTriangularizable K L M] (χ ψ : LieModule.Weight K L M) : Set.MapsTo ⇑(genWeightSpaceProjection K L M χ) ↑(LieModule.genWeightSpace M ⇑ψ) ↑(LieModule.genWeightSpace M ⇑ψ)

A projection maps each weight space into itself: its own weight space identically, the others to zero.

theorem Ado.trace_genWeightSpaceProjection {K : Type u} {L : Type v} {M : Type w} [Field K] [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [LieModule.IsTriangularizable K L M] (χ : LieModule.Weight K L M) : (LinearMap.trace K M) (genWeightSpaceProjection K L M χ) = ↑(Module.finrank K ↥(LieModule.genWeightSpace M ⇑χ))

The trace of a projection is the dimension of the weight space it projects onto.

The root-space projections of a Killing Lie algebra

theorem Ado.killingForm_genWeightSpaceProjection {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (χ : LieModule.Weight K (↥H) L) (x y : L) : ((killingForm K L) ((genWeightSpaceProjection K (↥H) L χ) x)) y = ((killingForm K L) x) ((genWeightSpaceProjection K (↥H) L (-χ)) y)

The root-space projections are Killing-adjoint in opposite pairs. Root spaces pair to zero under the Killing form unless their weights are opposite, so pushing the projection onto the χ-root space across the form turns it into the projection onto the -χ-root space.

theorem Ado.isAdjointPair_genWeightSpaceProjection {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (χ : LieModule.Weight K (↥H) L) : LinearMap.IsAdjointPair (killingForm K L) (killingForm K L) ⇑(genWeightSpaceProjection K (↥H) L (-χ)) ⇑(genWeightSpaceProjection K (↥H) L χ)

Opposite root-space projections are a Killing-adjoint pair. This is the LinearMap.IsAdjointPair form of Ado.killingForm_genWeightSpaceProjection, which is what the Killing-dual-basis lemmas consume.

theorem Ado.trace_genWeightSpaceProjection_eq_one {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] [CharZero K] {χ : LieModule.Weight K (↥H) L} (hχ : χ.IsNonZero) : (LinearMap.trace K L) (genWeightSpaceProjection K (↥H) L χ) = 1

A root-space projection has trace one. The root spaces at nonzero weights are lines (LieAlgebra.IsKilling.finrank_rootSpace_eq_one).