Complete reducibility from a single irreducible input

Weyl's complete reducibility theorem and its sl₂ rank-one case share one and the same argument. Only a single step of that argument is representation-theoretic; everything else is formal, and this file isolates the formal part so that it is proved once.

The input is Ado.HasInvariantOutsideIrreducible K L: whenever L carries a finite-dimensional module M into a proper irreducible Lie submodule N and acts nontrivially somewhere on M, the module M has a nonzero L-invariant vector outside N. In practice this is supplied by a Casimir operator, which is injective on a nontrivial irreducible while its range lies in N, so it cannot be injective on M; its kernel is then the invariant vector. That is the only place where the base field, the Lie algebra, and the choice of Casimir enter.

From that input alone this file derives, over an arbitrary field:

• the same conclusion with no irreducibility hypothesis on N (Ado.HasInvariantOutsideIrreducible.exists_invariant_notMem), by an induction on finrank K M that peels a nonzero proper W ≤ N off, first in the quotient M ⧸ W and then in the span W + K v₀;
• an L-equivariant projection of M onto an arbitrary Lie submodule (Ado.HasInvariantOutsideIrreducible.exists_equivariant_projection), by running the previous step inside the endomorphism module M →ₗ[K] M;
• complete reducibility (Ado.HasInvariantOutsideIrreducible.exists_isCompl): every Lie submodule of a finite-dimensional module has a complement.

The two endomorphism submodules

The reduction to the irreducible input runs inside M →ₗ[K] M and turns on the pair of Lie submodules Ado.homVanishingOn N ≤ Ado.homScalarOn N: endomorphisms carrying M into N and acting on N by a scalar, respectively by the scalar 0. Bracketing an element of L with an element of homScalarOn N lands in homVanishingOn N (Ado.lie_mem_comap_homVanishingOn), so L carries homScalarOn N into homVanishingOn N, which is proper as soon as N ≠ ⊥ because a linear projection onto N acts there by the scalar 1. An invariant vector outside it is, after rescaling, an equivariant projection, and its kernel is the complement.

Main definitions

• Ado.homScalarOn and Ado.homVanishingOn: the two Lie submodules of M →ₗ[K] M above.
• Ado.HasInvariantOutsideIrreducible: the irreducible input described above.

Main results

• Ado.exists_isCompl_of_equivariant_projection: a Lie submodule admitting an L-equivariant projection is a direct summand. This needs no finiteness and no field, only a commutative ring.
• Ado.HasInvariantOutsideIrreducible.exists_invariant_notMem: the irreducibility hypothesis may be dropped.
• Ado.HasInvariantOutsideIrreducible.exists_equivariant_projection: every Lie submodule of a finite-dimensional module admits an L-equivariant projection.
• Ado.HasInvariantOutsideIrreducible.exists_isCompl: complete reducibility.

References

• [J. E. Humphreys, Introduction to Lie Algebras and Representation Theory][humphreys1972], §6.2 and §6.3.

Endomorphisms acting on a submodule by a scalar

def Ado.homScalarOn {K : Type u_1} [CommRing K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {M : Type u_3} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] (N : LieSubmodule K L M) : LieSubmodule K L (M →ₗ[K] M)

The endomorphisms of M carrying M into N and acting on N by a scalar. It is a Lie submodule of M →ₗ[K] M because bracketing with an element of L kills N.

Equations

• Ado.homScalarOn N = { carrier := {φ : M →ₗ[K] M | (∀ (m : M), φ m ∈ N) ∧ ∃ (c : K), ∀ n ∈ N, φ n = c • n}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯, lie_mem := ⋯ }

def Ado.homVanishingOn {K : Type u_1} [CommRing K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {M : Type u_3} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] (N : LieSubmodule K L M) : LieSubmodule K L (M →ₗ[K] M)

The endomorphisms of M carrying M into N and killing N, a Lie submodule of Ado.homScalarOn that misses every projection onto a nonzero N.

Equations

• Ado.homVanishingOn N = { carrier := {φ : M →ₗ[K] M | (∀ (m : M), φ m ∈ N) ∧ ∀ n ∈ N, φ n = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯, lie_mem := ⋯ }

@[simp]

theorem Ado.mem_homScalarOn {K : Type u_1} [CommRing K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {M : Type u_3} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {N : LieSubmodule K L M} {φ : M →ₗ[K] M} : φ ∈ homScalarOn N ↔ (∀ (m : M), φ m ∈ N) ∧ ∃ (c : K), ∀ n ∈ N, φ n = c • n

Membership in Ado.homScalarOn: land in N, and act on N by one scalar.

@[simp]

theorem Ado.mem_homVanishingOn {K : Type u_1} [CommRing K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {M : Type u_3} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {N : LieSubmodule K L M} {φ : M →ₗ[K] M} : φ ∈ homVanishingOn N ↔ (∀ (m : M), φ m ∈ N) ∧ ∀ n ∈ N, φ n = 0

Membership in Ado.homVanishingOn: land in N, and vanish on N.

theorem Ado.homVanishingOn_le_homScalarOn {K : Type u_1} [CommRing K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {M : Type u_3} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] (N : LieSubmodule K L M) : homVanishingOn N ≤ homScalarOn N

Vanishing on N is acting on N by the scalar 0.

theorem Ado.lie_mem_comap_homVanishingOn {K : Type u_1} [CommRing K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {M : Type u_3} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] (N : LieSubmodule K L M) (x : L) (ψ : ↥(homScalarOn N)) : ⁅x, ψ⁆ ∈ LieSubmodule.comap (homScalarOn N).incl (homVanishingOn N)

Bracketing an endomorphism acting scalarly on N with an element of L produces one vanishing on N. The bracket again lands in N and vanishes there.

An equivariant projection splits off its image

theorem Ado.exists_isCompl_of_equivariant_projection {K : Type u_1} [CommRing K] {L : Type u_2} [LieRing L] {M : Type u_3} [AddCommGroup M] [Module K M] [LieRingModule L M] {N : LieSubmodule K L M} {ψ : M →ₗ[K] M} (hψmem : ∀ (m : M), ψ m ∈ N) (hψid : ∀ n ∈ N, ψ n = n) (hψlie : ∀ (x : L) (m : M), ψ ⁅x, m⁆ = ⁅x, ψ m⁆) : ∃ (N' : LieSubmodule K L M), IsCompl N N'

A Lie submodule admitting an equivariant projection is a direct summand. If an L-equivariant linear endomorphism of M takes values in N and restricts to the identity on N, then N has a complement, namely the kernel of that endomorphism.

The irreducible input, and the induction that removes irreducibility

def Ado.HasInvariantOutsideIrreducible (K : Type u_1) [Field K] (L : Type u_2) [LieRing L] [LieAlgebra K L] : Prop

The one representation-theoretic input of complete reducibility. Whenever L carries a finite-dimensional module M into a proper irreducible Lie submodule N, and acts nontrivially somewhere on M, the module M has a nonzero L-invariant vector outside N.

A Casimir operator supplies this: it commutes with the action, its range lies in N because L carries M into N, and it is injective on a nontrivial irreducible N, so it fails to be surjective and hence, in finite dimension, fails to be injective; any nonzero kernel vector is invariant and outside N.

Ado.HasInvariantOutsideIrreducible.exists_isCompl turns this into complete reducibility.

Equations

• One or more equations did not get rendered due to their size.

theorem Ado.HasInvariantOutsideIrreducible.exists_invariant_notMem {K : Type u_1} [Field K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {M : Type v} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] (h : HasInvariantOutsideIrreducible K L) [FiniteDimensional K M] (N : LieSubmodule K L M) (hN : N ≠ ⊤) (htriv : ∀ (x : L) (m : M), ⁅x, m⁆ ∈ N) : ∃ w ∉ N, ∀ (x : L), ⁅x, w⁆ = 0

An invariant vector outside a proper submodule, with no irreducibility hypothesis. If L carries a finite-dimensional module M into a proper Lie submodule N, then M has an invariant vector outside N.

This is the load-bearing half of complete reducibility: applied inside the endomorphism module M →ₗ[K] M it produces the equivariant projection onto an arbitrary submodule.

theorem Ado.HasInvariantOutsideIrreducible.exists_equivariant_projection {K : Type u_1} [Field K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {M : Type v} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] (h : HasInvariantOutsideIrreducible K L) [FiniteDimensional K M] (N : LieSubmodule K L M) : ∃ (ψ : M →ₗ[K] M), (∀ (m : M), ψ m ∈ N) ∧ (∀ n ∈ N, ψ n = n) ∧ ∀ (x : L) (m : M), ψ ⁅x, m⁆ = ⁅x, ψ m⁆

Every Lie submodule admits an L-equivariant projection onto it. There is a linear endomorphism of M taking values in N, restricting to the identity on N, and commuting with the action of L.

theorem Ado.HasInvariantOutsideIrreducible.exists_isCompl {K : Type u_1} [Field K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {M : Type v} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] (h : HasInvariantOutsideIrreducible K L) [FiniteDimensional K M] (N : LieSubmodule K L M) : ∃ (N' : LieSubmodule K L M), IsCompl N N'

Complete reducibility. Every Lie submodule of a finite-dimensional module has a complement, so the module is a direct sum of irreducibles.