The sl n ↔ gl n dictionary for irreducible modules

gl n K is reductive (TauCeti.hasCentralRadical_matrix), its centre is the scalar matrices and its derived ideal is sl n K (TauCeti.derivedSeries_one_eq_slIdeal). Specializing the reductive theory of TauCeti/Algebra/Lie/Reductive.lean to that data gives the two halves of the transfer between the representation theory of gl n K and that of sl n K:

• restriction to sl n K preserves irreducibility, over an algebraically closed field of characteristic zero;
• an sl n K-equivariant map between gl n K-modules on which the identity matrix acts by one and the same scalar is already gl n K-equivariant.

Both statements are the concrete face of "the centre acts by scalars, and the centre and the derived ideal span": nothing about a gl n K-module is invisible to sl n K except the single scalar by which the identity matrix acts, which is the central weight of TauCeti/Algebra/Lie/Weights/Central.lean.

Main results

• TauCeti.isIrreducible_slIdeal_of_isIrreducible_matrix: a finite-dimensional irreducible gl n K-module is irreducible over sl n K, for K algebraically closed of characteristic zero.
• TauCeti.map_lie_matrix_of_one_lie_eq_smul_of_forall_mem_slIdeal: an sl n K-equivariant linear map between gl n K-modules on which 1 acts by the same scalar is gl n K-equivariant, with TauCeti.lieModuleEquivOfOneLieEqSmulOfSlEquiv the packaged equivalence.

Roadmap

This is the "sl ↔ gl transfer, pinned" bullet of Layer 9 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, stated for an arbitrary irreducible gl n K-module rather than for the not-yet-constructed named carrier glIrreducible n μ, which it will specialize to.

theorem TauCeti.map_lie_matrix_of_one_lie_eq_smul_of_forall_mem_slIdeal {n : Type u_1} [DecidableEq n] [Fintype n] (K : Type u) [Field K] [CharZero K] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule (Matrix n n K) M] {N : Type w'} [AddCommGroup N] [Module K N] [LieRingModule (Matrix n n K) N] [LieModule K (Matrix n n K) M] [LieModule K (Matrix n n K) N] (f : M →ₗ[K] N) {c : K} (hM : ∀ (m : M), ⁅1, m⁆ = c • m) (hN : ∀ (m : N), ⁅1, m⁆ = c • m) (hsl : ∀ A ∈ slIdeal K n, ∀ (m : M), f ⁅A, m⁆ = ⁅A, f m⁆) (A : Matrix n n K) (m : M) : f ⁅A, m⁆ = ⁅A, f m⁆

An sl n K-equivariant map between gl n K-modules on which the identity matrix acts by the same scalar is gl n K-equivariant. gl n K is spanned by its centre, the scalar matrices, and its derived ideal sl n K (TauCeti.sup_center_derivedSeries_eq_top), so equivariance need only be checked on those two.

def TauCeti.lieModuleEquivOfOneLieEqSmulOfSlEquiv {n : Type u_1} [DecidableEq n] [Fintype n] (K : Type u) [Field K] [CharZero K] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule (Matrix n n K) M] {N : Type w'} [AddCommGroup N] [Module K N] [LieRingModule (Matrix n n K) N] [LieModule K (Matrix n n K) M] [LieModule K (Matrix n n K) N] (e : M ≃ₗ[K] N) {c : K} (hM : ∀ (m : M), ⁅1, m⁆ = c • m) (hN : ∀ (m : N), ⁅1, m⁆ = c • m) (hsl : ∀ A ∈ slIdeal K n, ∀ (m : M), e ⁅A, m⁆ = ⁅A, e m⁆) : M ≃ₗ⁅K,Matrix n n K⁆ N

The packaged form of TauCeti.map_lie_matrix_of_one_lie_eq_smul_of_forall_mem_slIdeal: an sl n K-equivariant linear equivalence between gl n K-modules on which the identity matrix acts by the same scalar is an equivalence of gl n K-modules.

Equations

• TauCeti.lieModuleEquivOfOneLieEqSmulOfSlEquiv K e hM hN hsl = { toLinearMap := ↑e, map_lie' := ⋯, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.lieModuleEquivOfOneLieEqSmulOfSlEquiv_apply {n : Type u_1} [DecidableEq n] [Fintype n] (K : Type u) [Field K] [CharZero K] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule (Matrix n n K) M] {N : Type w'} [AddCommGroup N] [Module K N] [LieRingModule (Matrix n n K) N] [LieModule K (Matrix n n K) M] [LieModule K (Matrix n n K) N] (e : M ≃ₗ[K] N) {c : K} (hM : ∀ (m : M), ⁅1, m⁆ = c • m) (hN : ∀ (m : N), ⁅1, m⁆ = c • m) (hsl : ∀ A ∈ slIdeal K n, ∀ (m : M), e ⁅A, m⁆ = ⁅A, e m⁆) (m : M) : (lieModuleEquivOfOneLieEqSmulOfSlEquiv K e hM hN hsl) m = e m

@[simp]

theorem TauCeti.lieModuleEquivOfOneLieEqSmulOfSlEquiv_symm_apply {n : Type u_1} [DecidableEq n] [Fintype n] (K : Type u) [Field K] [CharZero K] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule (Matrix n n K) M] {N : Type w'} [AddCommGroup N] [Module K N] [LieRingModule (Matrix n n K) N] [LieModule K (Matrix n n K) M] [LieModule K (Matrix n n K) N] (e : M ≃ₗ[K] N) {c : K} (hM : ∀ (m : M), ⁅1, m⁆ = c • m) (hN : ∀ (m : N), ⁅1, m⁆ = c • m) (hsl : ∀ A ∈ slIdeal K n, ∀ (m : M), e ⁅A, m⁆ = ⁅A, e m⁆) (n✝ : N) : (lieModuleEquivOfOneLieEqSmulOfSlEquiv K e hM hN hsl).symm n✝ = e.symm n✝

theorem TauCeti.isIrreducible_slIdeal_of_isIrreducible_matrix {n : Type u_1} [DecidableEq n] [Fintype n] (K : Type u) [Field K] [CharZero K] (M : Type w) [AddCommGroup M] [Module K M] [LieRingModule (Matrix n n K) M] [IsAlgClosed K] [LieModule K (Matrix n n K) M] [FiniteDimensional K M] [LieModule.IsIrreducible K (Matrix n n K) M] : LieModule.IsIrreducible K (↥(slIdeal K n)) M

A finite-dimensional irreducible gl n K-module is irreducible over sl n K, for K algebraically closed of characteristic zero. This is TauCeti.isIrreducible_restrict_derivedSeries for the reductive Lie algebra gl n K, whose derived ideal is sl n K; the scalar matrices act by the central weight and so stabilize every subspace.