The central weight of an irreducible Lie module

A central element z of a Lie algebra L acts on any L-module M by a morphism of L-modules, because ⁅x, ⁅z, m⁆⁆ = ⁅⁅x, z⁆, m⁆ + ⁅z, ⁅x, m⁆⁆ and the first summand vanishes. When M is a finite-dimensional irreducible module over an algebraically closed field, Schur's lemma turns that morphism into a scalar, and the scalar depends linearly on z: the central weight of M, an element of Module.Dual K (LieAlgebra.center K L).

Unlike the weights of a Cartan subalgebra on a finite-dimensional module over a semisimple Lie algebra, the central weight carries no integrality constraint: it is recorded here as a plain element of Module.Dual K (LieAlgebra.center K L), with no lattice condition attached. For gl n K, whose centre is the scalar matrices (TauCeti.center_matrix_toSubmodule_eq_span_one), the central weight is the scalar by which the identity matrix acts, and for n > 0 in characteristic zero that scalar is an arbitrary element of K: twisting a module by the character (c / n) • Matrix.trace shifts it by c, so none of the integrality that the general linear group imposes on the central characters of its representations survives here. That twist needs n invertible; when the characteristic divides n the identity matrix lies in ⁅gl n K, gl n K⁆ = sl n K and the scalars that occur can be constrained, so what is claimed in general is only the absence of a lattice condition, not that every scalar occurs.

Algebraic closedness is essential and not a convenience: over ℝ the one-dimensional abelian Lie algebra acting on ℝ² by the rotation generator is irreducible, is its own centre, and no scalar describes its action.

Main definitions

• TauCeti.centralEnd: the action of a central element on an L-module, as a morphism of L-modules.
• TauCeti.centralWeight: the central weight of a finite-dimensional irreducible module over an algebraically closed field, a linear functional on LieAlgebra.center K L.

Main results

• TauCeti.exists_forall_apply_eq_smul is Schur's lemma for Lie modules: over an algebraically closed field, a morphism of a finite-dimensional irreducible L-module to itself is a scalar. Its companion TauCeti.eq_of_forall_lie_eq_smul says that the scalar describing the action of a single element of L on a faithful module is unique, which is what makes centralWeight well defined and linear.
• TauCeti.forall_apply_eq_smul_of_apply_eq_smul and its central-element form TauCeti.forall_lie_eq_smul_of_lie_eq_smul are the half of Schur's lemma that needs neither algebraic closedness nor finite-dimensionality: a scalar already known on one nonzero vector of an irreducible module describes the whole action.
• TauCeti.exists_centralWeight_of_isIrreducible is the existential form the roadmap pins.
• TauCeti.lie_eq_centralWeight_smul and TauCeti.toEnd_eq_centralWeight_smul are the defining property of the central weight, and TauCeti.centralWeight_eq_of_forall_lie_eq_smul its characterization.
• TauCeti.centralWeight_eq_of_lieModuleEquiv: the central weight is an isomorphism invariant.
• TauCeti.isIrreducible_of_sup_center_eq_top: a Lie subalgebra whose sum with the centre is all of L already acts irreducibly. This is the mechanism by which a reductive Lie algebra hands its irreducibles down to its derived ideal, the centre contributing only the scalars recorded by centralWeight. Its generalization TauCeti.isIrreducible_of_sup_center_eq_top_of_forall_exists_lie_eq_smul takes those scalars as a hypothesis instead, and so applies over any commutative ring.

Implementation notes

Schur's lemma is proved through LieModuleHom.ker: f - c • LieModuleHom.id is again a morphism of L-modules, so its kernel is a Lie submodule, and it is nonzero because c was chosen to be an eigenvalue of the underlying linear map. That is why the ambient hypotheses are FiniteDimensional K M and IsAlgClosed K, exactly the hypotheses of Module.End.exists_eigenvalue.

TauCeti.eq_of_forall_lie_eq_smul is stated for any bracket action and any faithful scalar action, rather than under an irreducibility hypothesis, since uniqueness of the scalar needs nothing else. A nontrivial module over a division ring is faithful, which is how the central weight uses it.

References

This is the "irreducibles of a reductive algebra" item of Layer 9 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md: "Over algebraically closed K the centre acts on a finite-dimensional irreducible by a central weight, a functional on the centre with no integrality constraint", the target named there exists_centralWeight_of_isIrreducible, together with the API that makes the functional a named object rather than an existential.

Uniqueness of the scalar by which an element acts

theorem TauCeti.eq_of_forall_lie_eq_smul {K : Type u} {L : Type v} {M : Type w} [SMul K M] [FaithfulSMul K M] [Bracket L M] {x : L} {c d : K} (hc : ∀ (m : M), ⁅x, m⁆ = c • m) (hd : ∀ (m : M), ⁅x, m⁆ = d • m) : c = d

The scalar by which an element of L acts is unique. When K acts faithfully on M, two scalars that both describe the action of x agree; no irreducibility is needed.

Schur's lemma for Lie modules

theorem TauCeti.forall_apply_eq_smul_of_apply_eq_smul (K : Type u) [CommRing K] (L : Type v) [LieRing L] [LieAlgebra K L] (M : Type w) [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [LieModule.IsIrreducible K L M] (f : M →ₗ⁅K,L⁆ M) {c : K} {m₀ : M} (hm₀ : m₀ ≠ 0) (h : f m₀ = c • m₀) (m : M) : f m = c • m

A morphism of an irreducible module that scales one nonzero vector scales every vector. The vectors f scales by c are the kernel of f - c • id, a Lie submodule, nonzero by hypothesis and therefore everything. Neither finite-dimensionality nor algebraic closedness enters: those are what TauCeti.exists_forall_apply_eq_smul needs to produce the scalar in the first place.

theorem TauCeti.exists_forall_apply_eq_smul (K : Type u) [Field K] (L : Type v) [LieRing L] [LieAlgebra K L] (M : Type w) [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [LieModule.IsIrreducible K L M] [IsAlgClosed K] [FiniteDimensional K M] (f : M →ₗ⁅K,L⁆ M) : ∃ (c : K), ∀ (m : M), f m = c • m

Schur's lemma for Lie modules. Over an algebraically closed field, a morphism of a finite-dimensional irreducible L-module to itself is multiplication by a scalar: an eigenvalue exists, and the corresponding eigenspace is a nonzero Lie submodule, hence everything.

The action of a central element

def TauCeti.centralEnd (K : Type u) [CommRing K] (L : Type v) [LieRing L] [LieAlgebra K L] (M : Type w) [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] (z : ↥(LieAlgebra.center K L)) : M →ₗ⁅K,L⁆ M

The action of a central element, as a morphism of L-modules. The Leibniz rule ⁅x, ⁅z, m⁆⁆ = ⁅⁅x, z⁆, m⁆ + ⁅z, ⁅x, m⁆⁆ has vanishing first summand exactly because z is central, so ⁅z, -⁆ commutes with the action of every element of L.

Equations

• TauCeti.centralEnd K L M z = { toFun := fun (m : M) => ⁅↑z, m⁆, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

@[simp]

theorem TauCeti.centralEnd_apply (K : Type u) [CommRing K] (L : Type v) [LieRing L] [LieAlgebra K L] (M : Type w) [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] (z : ↥(LieAlgebra.center K L)) (m : M) : (centralEnd K L M z) m = ⁅↑z, m⁆

theorem TauCeti.forall_lie_eq_smul_of_lie_eq_smul (K : Type u) [CommRing K] (L : Type v) [LieRing L] [LieAlgebra K L] (M : Type w) [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [LieModule.IsIrreducible K L M] (z : ↥(LieAlgebra.center K L)) {c : K} {m₀ : M} (hm₀ : m₀ ≠ 0) (h : ⁅↑z, m₀⁆ = c • m₀) (m : M) : ⁅↑z, m⁆ = c • m

A central element scaling one nonzero vector of an irreducible module scales every vector: TauCeti.forall_apply_eq_smul_of_apply_eq_smul applied to TauCeti.centralEnd. Where the scalar is known in advance — read off a highest weight vector, say — this replaces the appeal to Schur's lemma, and with it the hypotheses of algebraic closedness and finite-dimensionality.

The central weight

theorem TauCeti.exists_forall_lie_eq_smul (K : Type u) [Field K] [IsAlgClosed K] (L : Type v) [LieRing L] [LieAlgebra K L] (M : Type w) [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [LieModule.IsIrreducible K L M] (z : ↥(LieAlgebra.center K L)) : ∃ (c : K), ∀ (m : M), ⁅↑z, m⁆ = c • m

A central element acts by a scalar on a finite-dimensional irreducible module over an algebraically closed field: TauCeti.exists_forall_apply_eq_smul applied to TauCeti.centralEnd.

noncomputable def TauCeti.centralWeight (K : Type u) [Field K] [IsAlgClosed K] (L : Type v) [LieRing L] [LieAlgebra K L] (M : Type w) [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [LieModule.IsIrreducible K L M] : Module.Dual K ↥(LieAlgebra.center K L)

The central weight of a finite-dimensional irreducible module over an algebraically closed field: the linear functional on LieAlgebra.center K L recording the scalar by which each central element acts.

Equations

• TauCeti.centralWeight K L M = { toFun := fun (z : ↥(LieAlgebra.center K L)) => ⋯.choose, map_add' := ⋯, map_smul' := ⋯ }

theorem TauCeti.lie_eq_centralWeight_smul (K : Type u) [Field K] [IsAlgClosed K] (L : Type v) [LieRing L] [LieAlgebra K L] (M : Type w) [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [LieModule.IsIrreducible K L M] (z : ↥(LieAlgebra.center K L)) (m : M) : ⁅↑z, m⁆ = (centralWeight K L M) z • m

The defining property of the central weight: a central element acts by the scalar the weight assigns to it.

theorem TauCeti.centralWeight_eq_of_forall_lie_eq_smul (K : Type u) [Field K] [IsAlgClosed K] (L : Type v) [LieRing L] [LieAlgebra K L] (M : Type w) [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [LieModule.IsIrreducible K L M] {z : ↥(LieAlgebra.center K L)} {c : K} (h : ∀ (m : M), ⁅↑z, m⁆ = c • m) : (centralWeight K L M) z = c

The central weight is characterized by its defining property: any scalar describing the action of a central element is its value.

theorem TauCeti.toEnd_eq_centralWeight_smul (K : Type u) [Field K] [IsAlgClosed K] (L : Type v) [LieRing L] [LieAlgebra K L] (M : Type w) [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [LieModule.IsIrreducible K L M] (z : ↥(LieAlgebra.center K L)) : (LieModule.toEnd K L M) ↑z = (centralWeight K L M) z • LinearMap.id

The central weight, read as a statement about the representation LieModule.toEnd: a central element acts by a scalar multiple of the identity.

theorem TauCeti.centralWeight_eq_zero_iff (K : Type u) [Field K] [IsAlgClosed K] (L : Type v) [LieRing L] [LieAlgebra K L] (M : Type w) [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [LieModule.IsIrreducible K L M] (z : ↥(LieAlgebra.center K L)) : (centralWeight K L M) z = 0 ↔ ↑z ∈ LieModule.ker K L M

A central element is in the kernel of the representation exactly when the central weight vanishes on it.

theorem TauCeti.exists_centralWeight_of_isIrreducible (K : Type u) [Field K] [IsAlgClosed K] (L : Type v) [LieRing L] [LieAlgebra K L] (M : Type w) [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [LieModule.IsIrreducible K L M] : ∃ (xi : Module.Dual K ↥(LieAlgebra.center K L)), ∀ (z : ↥(LieAlgebra.center K L)) (m : M), ⁅↑z, m⁆ = xi z • m

The centre acts by a central weight, in existential form: there is a linear functional on LieAlgebra.center K L by which every central element acts. This is the form the roadmap pins; the named witness is TauCeti.centralWeight. The roadmap signature also carries [CharZero K] and [FiniteDimensional K L], neither of which the statement needs.

theorem TauCeti.lie_mem_of_mem_center (K : Type u) [Field K] [IsAlgClosed K] (L : Type v) [LieRing L] [LieAlgebra K L] (M : Type w) [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [LieModule.IsIrreducible K L M] (z : ↥(LieAlgebra.center K L)) {N : Submodule K M} {m : M} (hm : m ∈ N) : ⁅↑z, m⁆ ∈ N

Every K-submodule of M is stable under the centre. The centre acts by scalars, and a submodule is stable under scalars; irreducibility of M puts no constraint on the submodules of the underlying vector space.

Invariance and descent to a subalgebra

theorem TauCeti.centralWeight_eq_of_lieModuleEquiv (K : Type u) [Field K] [IsAlgClosed K] (L : Type v) [LieRing L] [LieAlgebra K L] (M : Type w) [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] (N : Type x) [AddCommGroup N] [Module K N] [LieRingModule L N] [LieModule K L N] [FiniteDimensional K M] [LieModule.IsIrreducible K L M] [FiniteDimensional K N] [LieModule.IsIrreducible K L N] (e : M ≃ₗ⁅K,L⁆ N) : centralWeight K L N = centralWeight K L M

The central weight is an isomorphism invariant. Equivalent irreducible modules have the same central weight, so the weight is an invariant of the isomorphism class and can be used to separate irreducibles.

theorem TauCeti.isIrreducible_of_sup_center_eq_top_of_forall_exists_lie_eq_smul (K : Type u) [CommRing K] (L : Type v) [LieRing L] [LieAlgebra K L] (M : Type w) [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule.IsIrreducible K L M] (L' : LieSubalgebra K L) (h : L'.toSubmodule ⊔ ↑(LieAlgebra.center K L) = ⊤) (hc : ∀ (z : ↥(LieAlgebra.center K L)), ∃ (c : K), ∀ (m : M), ⁅↑z, m⁆ = c • m) : LieModule.IsIrreducible K (↥L') M

Irreducibility descends to a subalgebra complementing a centre that acts by scalars. If L' ⊔ center K L is all of L as a subspace and every central element acts by a scalar, then a submodule for L' is already a submodule for L, since the missing central directions only rescale. The scalars are a hypothesis rather than a conclusion here, so neither algebraic closedness nor finite-dimensionality is needed; TauCeti.isIrreducible_of_sup_center_eq_top is the case where Schur's lemma supplies them.

theorem TauCeti.isIrreducible_of_sup_center_eq_top (K : Type u) [Field K] (L : Type v) [LieRing L] [LieAlgebra K L] (M : Type w) [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [LieModule.IsIrreducible K L M] [IsAlgClosed K] [FiniteDimensional K M] (L' : LieSubalgebra K L) (h : L'.toSubmodule ⊔ ↑(LieAlgebra.center K L) = ⊤) : LieModule.IsIrreducible K (↥L') M

Irreducibility descends to a subalgebra complementing the centre. If L' ⊔ center K L is all of L as a subspace, then a submodule for L' is already a submodule for L, because the missing central directions act by scalars (TauCeti.exists_forall_lie_eq_smul). Applied to the derived ideal of a reductive Lie algebra, this is the statement that an irreducible module over a reductive algebra stays irreducible over its semisimple part, the centre contributing only the scalars recorded by TauCeti.centralWeight.