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 : L) (e : L) (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.h_ne_zero {L : Type u_2} [LieRing L] {h : L} {e : L} {f : L} (self : IsSl2Triple h e f) : h ≠ 0

theorem IsSl2Triple.lie_e_f {L : Type u_2} [LieRing L] {h : L} {e : L} {f : L} (self : IsSl2Triple h e f) : ⁅e, f⁆ = h

theorem IsSl2Triple.lie_h_e_nsmul {L : Type u_2} [LieRing L] {h : L} {e : L} {f : L} (self : IsSl2Triple h e f) : ⁅h, e⁆ = 2 • e

theorem IsSl2Triple.lie_h_f_nsmul {L : Type u_2} [LieRing L] {h : L} {e : L} {f : L} (self : IsSl2Triple h e f) : ⁅h, f⁆ = -(2 • f)

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

@[simp]

theorem IsSl2Triple.symm_iff {L : Type u_2} [LieRing L] {h : L} {e : L} {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 : L} {e : L} {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 : L} {e : L} {f : L} (t : IsSl2Triple h e f) : ⁅h, f⁆ = -(2 • f)

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

theorem IsSl2Triple.f_ne_zero {L : Type u_2} [LieRing L] {h : L} {e : L} {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 : L} {e : L} {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, 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.ne_zero {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 : L} {e : L} {f : L} {t : IsSl2Triple h e f} {m : M} {μ : R} (self : t.HasPrimitiveVectorWith m μ) : m ≠ 0

theorem IsSl2Triple.HasPrimitiveVectorWith.lie_h {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 : L} {e : L} {f : L} {t : IsSl2Triple h e f} {m : M} {μ : R} (self : t.HasPrimitiveVectorWith m μ) : ⁅h, m⁆ = μ • m

theorem IsSl2Triple.HasPrimitiveVectorWith.lie_e {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 : L} {e : L} {f : L} {t : IsSl2Triple h e f} {m : M} {μ : R} (self : t.HasPrimitiveVectorWith m μ) : ⁅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 : L} {e : L} {f : L} [NoZeroSMulDivisors ℤ M] (t : IsSl2Triple h e f) (m : M) (μ : R) (ρ : 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.

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 : L} {e : L} {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 : L} {e : L} {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 : L} {e : L} {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 : L} {e : L} {f : L} {m : M} {μ : R} {t : IsSl2Triple h e f} (P : t.HasPrimitiveVectorWith m μ) [IsNoetherian R M] [NoZeroSMulDivisors 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 : L} {e : L} {f : L} {m : M} {μ : R} {t : IsSl2Triple h e f} (P : t.HasPrimitiveVectorWith m μ) [CharZero R] [NoZeroSMulDivisors 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 : L} {e : L} {f : L} {m : M} {μ : R} {t : IsSl2Triple h e f} (P : t.HasPrimitiveVectorWith m μ) [IsNoetherian R M] [NoZeroSMulDivisors R M] [IsDomain R] [CharZero R] {n : ℕ} (hn : μ = ↑n) : ((LieModule.toEnd R L M) f ^ (n + 1)) m = 0