Restricting representations between gl n and sl n

As soon as the rank is invertible in the field of scalars, gl n is the sum of sl n and the scalar matrices. This file uses that decomposition in both directions needed by highest-weight theory: an irreducible gl n module stays irreducible on restriction to sl n, and an equivalence of sl n-modules upgrades to an equivalence of gl n-modules when the identity matrix acts by the same scalar on both modules.

The invertibility is asked for as n ≠ 0 → (n : K) ≠ 0, which is what the decomposition needs and no more: for positive rank it is supplied by TauCeti.isCompl_center_derivedSeries_one_matrix, while in rank zero every matrix is zero and nothing is needed. Characteristic zero is one way to have it, and the results stated over such a field discharge it themselves.

Main results

• TauCeti.isIrreducible_restrict_sl_of_forall_one_lie_eq_smul: restriction of an irreducible gl n module to sl n is irreducible as soon as the identity matrix acts by a scalar, and TauCeti.isIrreducible_restrict_sl_of_isGlHighestWeightVector reads that scalar off a highest weight vector.
• TauCeti.isIrreducible_restrict_sl: over an algebraically closed field Schur's lemma supplies that scalar, so a finite-dimensional irreducible gl n module restricts irreducibly.
• TauCeti.gl_equiv_of_sl_equiv_of_central_scalar: an sl n-module equivalence between two modules with the same scalar action of the identity matrix is a gl n-module equivalence.

References

These are the two pinned sl ↔ gl transfer statements in Layer 9 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md. The exact suggested signature for the upgrade theorem is in TauCetiRoadmap/RepresentationTheory/LieHighestWeight/Suggested.lean.

theorem TauCeti.isIrreducible_restrict_sl_of_forall_one_lie_eq_smul {K : Type u_1} [Field K] {n : ℕ} {M : Type u} [AddCommGroup M] [Module K M] [LieRingModule (Matrix (Fin n) (Fin n) K) M] [LieModule K (Matrix (Fin n) (Fin n) K) M] [LieModule.IsIrreducible K (Matrix (Fin n) (Fin n) K) M] {c : K} (hn : n ≠ 0 → ↑n ≠ 0) (hc : ∀ (m : M), ⁅1, m⁆ = c • m) : LieModule.IsIrreducible K (↥(LieAlgebra.SpecialLinear.sl (Fin n) K)) M

An irreducible representation of gl n on which the identity matrix acts by a given scalar stays irreducible after restriction to sl n: the scalars are exactly what the centre contributes, and, the rank being invertible, gl n is the sum of sl n and the scalar matrices. Neither algebraic closedness nor finite-dimensionality nor characteristic zero is needed, the first two being what TauCeti.isIrreducible_restrict_sl uses to produce the scalar.

theorem TauCeti.isIrreducible_restrict_sl_of_isGlHighestWeightVector {K : Type u_1} [Field K] {n : ℕ} {M : Type u} [AddCommGroup M] [Module K M] [LieRingModule (Matrix (Fin n) (Fin n) K) M] [LieModule K (Matrix (Fin n) (Fin n) K) M] [LieModule.IsIrreducible K (Matrix (Fin n) (Fin n) K) M] {mu : Fin n → K} {v : M} (hn : n ≠ 0 → ↑n ≠ 0) (hv : IsGlHighestWeightVector mu v) : LieModule.IsIrreducible K (↥(LieAlgebra.SpecialLinear.sl (Fin n) K)) M

An irreducible gl n module carrying a highest weight vector stays irreducible on restriction to sl n: by TauCeti.forall_one_lie_eq_sum_smul_of_isGlHighestWeightVector the identity matrix acts by the sum of the entries of that weight, which is the scalar TauCeti.isIrreducible_restrict_sl_of_forall_one_lie_eq_smul asks for. Reading the scalar off the vector is what lets this hold over any field in which the rank is invertible.

theorem TauCeti.isIrreducible_restrict_sl {K : Type u_1} [Field K] {n : ℕ} {M : Type u} [AddCommGroup M] [Module K M] [LieRingModule (Matrix (Fin n) (Fin n) K) M] [LieModule K (Matrix (Fin n) (Fin n) K) M] [LieModule.IsIrreducible K (Matrix (Fin n) (Fin n) K) M] [CharZero K] [IsAlgClosed K] [FiniteDimensional K M] : LieModule.IsIrreducible K (↥(LieAlgebra.SpecialLinear.sl (Fin n) K)) M

A finite-dimensional irreducible representation of gl n over an algebraically closed characteristic-zero field stays irreducible after restriction to sl n: Schur's lemma makes the identity matrix act by a scalar, and TauCeti.isIrreducible_restrict_sl_of_forall_one_lie_eq_smul does the rest.

theorem TauCeti.gl_equiv_of_sl_equiv_of_central_scalar {K : Type u_1} [Field K] [CharZero K] {n : ℕ} {M M' : Type u} [AddCommGroup M] [Module K M] [LieRingModule (Matrix (Fin n) (Fin n) K) M] [LieModule K (Matrix (Fin n) (Fin n) K) M] [AddCommGroup M'] [Module K M'] [LieRingModule (Matrix (Fin n) (Fin n) K) M'] [LieModule K (Matrix (Fin n) (Fin n) K) M'] (c : K) (hM : ∀ (m : M), ⁅1, m⁆ = c • m) (hM' : ∀ (m : M'), ⁅1, m⁆ = c • m) (e : Nonempty (M ≃ₗ⁅K,↥(LieAlgebra.SpecialLinear.sl (Fin n) K)⁆ M')) : Nonempty (M ≃ₗ⁅K,Matrix (Fin n) (Fin n) K⁆ M')

An equivalence of sl n-modules upgrades to an equivalence of gl n-modules when the identity matrix acts by the same scalar on both modules. No irreducibility or finite-dimensionality is needed.