The Lie algebra sl₂ and its representations

The Lie algebra sl₂ is the unique simple Lie algebra of minimal rank, 1, and as such occupies a distinguished position in the general theory. This file provides some basic definitions and results about sl₂.

Main definitions:

• IsSl2Triple: a structure representing a triple of elements in a Lie algebra which satisfy the standard relations for sl₂.
• IsSl2Triple.HasPrimitiveVectorWith: a structure representing a primitive vector in a representation of a Lie algebra relative to a distinguished sl₂ triple.
• IsSl2Triple.HasPrimitiveVectorWith.exists_nat: the eigenvalue of a primitive vector must be a natural number if the representation is finite-dimensional.

structure IsSl2Triple {L : Type u_2} [LieRing L] (h e f : L) : Prop

An sl₂ triple within a Lie ring L is a triple of elements h, e, f obeying relations which ensure that the Lie subalgebra they generate is equivalent to sl₂.

• h_ne_zero : h ≠ 0
• lie_e_f : ⁅e, f⁆ = h
• lie_h_e_nsmul : ⁅h, e⁆ = 2 • e
• lie_h_f_nsmul : ⁅h, f⁆ = -(2 • f)

theorem IsSl2Triple.symm {L : Type u_2} [LieRing L] {h e f : L} (ht : IsSl2Triple h e f) : IsSl2Triple (-h) f e

@[simp]

theorem IsSl2Triple.symm_iff {L : Type u_2} [LieRing L] {h e f : L} : IsSl2Triple (-h) f e ↔ IsSl2Triple h e f

theorem IsSl2Triple.lie_h_e_smul (R : Type u_1) {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {h e f : L} (t : IsSl2Triple h e f) : ⁅h, e⁆ = 2 • e

theorem IsSl2Triple.lie_lie_smul_f (R : Type u_1) {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {h e f : L} (t : IsSl2Triple h e f) : ⁅h, f⁆ = -(2 • f)

theorem IsSl2Triple.e_ne_zero {L : Type u_2} [LieRing L] {h e f : L} (t : IsSl2Triple h e f) : e ≠ 0

theorem IsSl2Triple.f_ne_zero {L : Type u_2} [LieRing L] {h e f : L} (t : IsSl2Triple h e f) : f ≠ 0

structure IsSl2Triple.HasPrimitiveVectorWith {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {h e f : L} (t : IsSl2Triple h e f) (m : M) (μ : R) : Prop

Given a representation of a Lie algebra with distinguished sl₂ triple, a vector is said to be primitive if it is a simultaneous eigenvector for the action of both h and e, and the eigenvalue for e is zero.

• ne_zero : m ≠ 0
• lie_h : ⁅h, m⁆ = μ • m
• lie_e : ⁅e, m⁆ = 0

theorem IsSl2Triple.HasPrimitiveVectorWith.mk' {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {h e f : L} [IsAddTorsionFree M] (t : IsSl2Triple h e f) (m : M) (μ ρ : R) (hm : m ≠ 0) (hm' : ⁅h, m⁆ = μ • m) (he : ⁅e, m⁆ = ρ • m) : t.HasPrimitiveVectorWith m μ

Given a representation of a Lie algebra with distinguished sl₂ triple, a simultaneous eigenvector for the action of both h and e necessarily has eigenvalue zero for e.

def IsSl2Triple.toLieSubalgebra (R : Type u_1) {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {h e f : L} (t : IsSl2Triple h e f) : LieSubalgebra R L

The subalgebra associated to an sl₂ triple.

Equations

• IsSl2Triple.toLieSubalgebra R t = { toSubmodule := Submodule.span R {e, f, h}, lie_mem' := ⋯ }

theorem IsSl2Triple.mem_toLieSubalgebra_iff {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {h e f x : L} {t : IsSl2Triple h e f} : x ∈ toLieSubalgebra R t ↔ ∃ (c₁ : R) (c₂ : R) (c₃ : R), x = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆

theorem IsSl2Triple.HasPrimitiveVectorWith.lie_f_pow_toEnd_f {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {h e f : L} {m : M} {μ : R} {t : IsSl2Triple h e f} (P : t.HasPrimitiveVectorWith m μ) (n : ℕ) : ⁅f, ((LieModule.toEnd R L M) f ^ n) m⁆ = ((LieModule.toEnd R L M) f ^ (n + 1)) m

theorem IsSl2Triple.HasPrimitiveVectorWith.lie_h_pow_toEnd_f {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {h e f : L} {m : M} {μ : R} {t : IsSl2Triple h e f} (P : t.HasPrimitiveVectorWith m μ) (n : ℕ) : ⁅h, ((LieModule.toEnd R L M) f ^ n) m⁆ = (μ - 2 * ↑n) • ((LieModule.toEnd R L M) f ^ n) m

theorem IsSl2Triple.HasPrimitiveVectorWith.lie_e_pow_succ_toEnd_f {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {h e f : L} {m : M} {μ : R} {t : IsSl2Triple h e f} (P : t.HasPrimitiveVectorWith m μ) (n : ℕ) : ⁅e, ((LieModule.toEnd R L M) f ^ (n + 1)) m⁆ = ((↑n + 1) * (μ - ↑n)) • ((LieModule.toEnd R L M) f ^ n) m

theorem IsSl2Triple.HasPrimitiveVectorWith.exists_nat {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {h e f : L} {m : M} {μ : R} {t : IsSl2Triple h e f} (P : t.HasPrimitiveVectorWith m μ) [IsNoetherian R M] [Module.IsTorsionFree R M] [IsDomain R] [CharZero R] : ∃ (n : ℕ), μ = ↑n

The eigenvalue of a primitive vector must be a natural number if the representation is finite-dimensional.

theorem IsSl2Triple.HasPrimitiveVectorWith.pow_toEnd_f_ne_zero_of_eq_nat {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {h e f : L} {m : M} {μ : R} {t : IsSl2Triple h e f} (P : t.HasPrimitiveVectorWith m μ) [CharZero R] [IsDomain R] [Module.IsTorsionFree R M] {n : ℕ} (hn : μ = ↑n) {i : ℕ} (hi : i ≤ n) : ((LieModule.toEnd R L M) f ^ i) m ≠ 0

theorem IsSl2Triple.HasPrimitiveVectorWith.pow_toEnd_f_eq_zero_of_eq_nat {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {h e f : L} {m : M} {μ : R} {t : IsSl2Triple h e f} (P : t.HasPrimitiveVectorWith m μ) [IsDomain R] [CharZero R] [IsNoetherian R M] [Module.IsTorsionFree R M] {n : ℕ} (hn : μ = ↑n) : ((LieModule.toEnd R L M) f ^ (n + 1)) m = 0

theorem IsSl2Triple.lie_e_pow_toEnd_e {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {e : L} {m : M} (n : ℕ) : ⁅e, ((LieModule.toEnd R L M) e ^ n) m⁆ = ((LieModule.toEnd R L M) e ^ (n + 1)) m

theorem IsSl2Triple.lie_h_pow_toEnd_e {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {h e f : L} {m : M} {μ : R} (t : IsSl2Triple h e f) (hm : ⁅h, m⁆ = μ • m) (n : ℕ) : ⁅h, ((LieModule.toEnd R L M) e ^ n) m⁆ = (μ + 2 * ↑n) • ((LieModule.toEnd R L M) e ^ n) m

theorem IsSl2Triple.exists_hasPrimitiveVectorWith {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {h e f : L} [IsDomain R] [CharZero R] [Nontrivial M] [Module.IsTorsionFree R M] [Module.Finite R M] [LieModule.IsTriangularizable R L M] (t : IsSl2Triple h e f) : ∃ (μ : R) (m : M), m ≠ 0 ∧ t.HasPrimitiveVectorWith m μ