The standard irreducible representations of sl₂

TauCeti/Algebra/Lie/Sl2/WeightString.lean classifies the finite-dimensional modules irreducible over the subalgebra of an sl₂ triple and carrying a primitive vector of weight n: there is at most one, of rank n + 1. It does not exhibit one, so the classification is so far vacuous for all we know. This file exhibits one, for every n : ℕ at once.

The module is Ado.Sl2Std K n, a type synonym for the coordinate space Fin (n + 1) → K, with LieAlgebra.SpecialLinear.sl (Fin 2) K acting through the standard basis (e, f, h) of Ado.slFinTwoBasis by the explicit ladder

e · vᵢ = i · vᵢ₋₁, f · vᵢ = (n - i) · vᵢ₊₁, h · vᵢ = (n - 2i) · vᵢ

on the coordinate vectors v₀, …, vₙ. Both ladder coefficients vanish at the end of the string they would run off, which is what makes the finite string a module; the h-eigenvalues n, n - 2, …, -n are the weights. So v₀ is a primitive vector of weight n, and over a field of characteristic zero the module is irreducible: a nonzero submodule contains a nonzero vector killed by e (the raising operator is nilpotent), such a vector is a multiple of v₀, and f carries v₀ along the whole string because the coefficients n - i are invertible.

Nothing about that construction is special to sl (Fin 2) K: an arbitrary sl₂ triple t : IsSl2Triple h e f generating a Lie algebra L is a basis of L obeying the same relations (Ado.basisOfIsSl2Triple), so V(n) is a module over L too. That is what Ado.exists_isIrreducible_hasPrimitiveVectorWith records, the existence half of the classification for an arbitrary sl₂.

Main definitions

• Ado.Sl2Std: the module V(n), with the sl (Fin 2) K-action supplied by Ado.Sl2Std.instLieRingModule and Ado.Sl2Std.instLieModule.
• Ado.Sl2Std.raise, Ado.Sl2Std.lower, Ado.Sl2Std.diag: the three ladder operators, defined directly in coordinates.
• Ado.Sl2Std.rep: the representation itself, the Lie algebra homomorphism sl (Fin 2) K →ₗ⁅K⁆ Module.End K (Sl2Std K n) sending the standard basis to the three operators. That the ladder operators obey the relations is Ado.Sl2Std.lie_raise_lower, Ado.Sl2Std.lie_diag_raise and Ado.Sl2Std.lie_diag_lower.
• Ado.Sl2Std.repOfIsSl2Triple: the action on V(n) of a Lie algebra generated by an arbitrary sl₂ triple, sending the triple to the ladder operators. It is built from the basis Ado.basisOfIsSl2Triple of that algebra.
• Ado.Sl2Std.basis: the coordinate basis v₀, …, vₙ.
• Ado.Sl2Std.basisVector: the coordinate basis vectors indexed by ℕ and extended by zero past the end of the string, for uniformly stated ladder identities.
• Ado.Sl2Std.lieModuleEquiv: the classification, obtained by feeding this module to Ado.lieModuleEquivOfHasPrimitiveVectorWith.

Main results

• Ado.Sl2Std.hasPrimitiveVectorWith: v₀ is a primitive vector of weight n for the standard sl₂ triple of sl (Fin 2) K.
• Ado.Sl2Std.finrank_eq: V(n) has rank n + 1, matching the value forced by Ado.finrank_eq_of_hasPrimitiveVectorWith.
• Ado.Sl2Std.eigenspace_diag, Ado.Sl2Std.finrank_eigenspace_diag and Ado.Sl2Std.eigenspace_diag_eq_bot: the weights of V(n) are exactly n, n - 2, …, -n, each with multiplicity one, the eigenspace of n - 2i being the coordinate line of vᵢ.
• Ado.Sl2Std.lower_pow_basis_zero: the weight string of v₀ in coordinates, fⁱ · v₀ being vᵢ scaled by n(n - 1)⋯(n - i + 1). Ado.Sl2Std.lieModuleEquiv_apply_basis reads the classification through it.
• Ado.Sl2Std.isIrreducible and Ado.Sl2Std.isIrreducible_toLieSubalgebra: over a field of characteristic zero V(n) is irreducible, both over sl (Fin 2) K and over the subalgebra generated by the standard triple. The second is the hypothesis the classification asks for; the two agree here because the standard triple generates the whole of sl (Fin 2) K (Ado.toLieSubalgebra_isSl2Triple_single_eq_top).
• Ado.Sl2Std.raise_pow_apply, Ado.Sl2Std.lower_pow_apply and Ado.Sl2Std.diag_pow_apply: explicit coordinate action formulas for powers of the ladder and Cartan operators.
• Ado.Sl2Std.isNilpotent_raise and Ado.Sl2Std.isNilpotent_lower: nilpotence of the raising and lowering operators on V(n), with Ado.Sl2Std.raise_pow_eq_zero and Ado.Sl2Std.lower_pow_eq_zero giving the explicit exponent n + 1.
• Ado.exists_isIrreducible_hasPrimitiveVectorWith: existence for an arbitrary sl₂. A Lie algebra generated by an sl₂ triple has, for every n, a finite-dimensional irreducible module with a primitive vector of weight n.

Implementation notes

Sl2Std K n is a type synonym for Fin (n + 1) → K rather than that type itself: the sl (Fin 2) K-action is not canonical on a plain function space, and registering it there as an instance would give every Fin m → K a surprise Lie module structure. The synonym is @[expose]d so that its coordinates are still directly available, and Ado.Sl2Std.add_apply, Ado.Sl2Std.smul_apply, Ado.Sl2Std.sub_apply, Ado.Sl2Std.neg_apply, Ado.Sl2Std.zero_apply and Ado.Sl2Std.sum_apply restate the pointwise operations that Pi lemmas can no longer reach through it.

The three ladder operators are @[expose]d for the same reason. They are defined by a Module.End literal, and unfolding that literal is exactly what proves their coordinate equations Ado.Sl2Std.raise_apply, Ado.Sl2Std.lower_apply and Ado.Sl2Std.diag_apply. A public theorem may unfold only exposed definitions, in its own module as much as anywhere else, so without exposure those equations could not be stated as public theorems at all, and there would be no way to use the operators. Exposure is what makes those three equations provable, not an invitation to unfold the literal again: the operators are marked irreducible immediately after the equations, so the equations really are the only elimination API and no consumer, here or downstream, can depend on how the operators are built.

Ado.Sl2Std.lie_slFinTwoBasis_zero, Ado.Sl2Std.lie_slFinTwoBasis_one and Ado.Sl2Std.lie_slFinTwoBasis_two are deliberately not @[simp]: Ado.slFinTwoBasis_zero, Ado.slFinTwoBasis_one and Ado.slFinTwoBasis_two are themselves @[simp], so their left hand sides are not in simp normal form and simpNF rejects them. simp reaches the ladder operators through the coordinate equations instead, and these three are used in both directions.

The ladder coefficients are pinned as above rather than in the more common normalization e · vᵢ = i(n + 1 - i) · vᵢ₋₁, f · vᵢ = vᵢ₊₁: the two differ by rescaling the basis, and in the normalization used here both coefficients vanish at the relevant end of the string, so the bracket identities need no case split at the ends of the string and hold verbatim over any commutative ring.

The construction and the bracket identities are stated over an arbitrary commutative ring. The Cartan eigenspaces and the kernel of the raising operator need the coefficients i and n - i only to be distinct and nonzero, and so ask for a domain of characteristic zero; a field is used where those coefficients are actually inverted, which is the multiplicity count and irreducibility.

Ado.Sl2Std.rep is not the special case of Ado.Sl2Std.repOfIsSl2Triple for the standard triple of sl (Fin 2) K: the general form needs a torsion-free Lie algebra over a domain of characteristic zero, since a triple is a basis of the algebra it generates only there, while the action on sl (Fin 2) K is available over any commutative ring. The two are instead both built from Ado.lieHomOfSl2Basis, which carries the bilinearity argument they share.

The module produced by Ado.exists_isIrreducible_hasPrimitiveVectorWith lives in the universe of the coefficient field, that being where the coordinate space Kⁿ⁺¹ lives.

References

This is the "standard irreducible V(n)" milestone of Layer 0 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, whose sl2_exists_irreducible is Ado.exists_isIrreducible_hasPrimitiveVectorWith.

• [J. E. Humphreys, Introduction to Lie Algebras and Representation Theory][humphreys1972], §7.2.

The relations of the standard basis of sl₂

theorem Ado.lie_slFinTwoBasis_zero_one (K : Type u_1) [CommRing K] : ⁅(slFinTwoBasis K) 0, (slFinTwoBasis K) 1⁆ = (slFinTwoBasis K) 2

The standard basis of sl (Fin 2) K obeys the relation ⁅e, f⁆ = h, in the form Ado.lieHomOfSl2Basis asks for.

theorem Ado.lie_slFinTwoBasis_two_zero (K : Type u_1) [CommRing K] : ⁅(slFinTwoBasis K) 2, (slFinTwoBasis K) 0⁆ = 2 • (slFinTwoBasis K) 0

The standard basis of sl (Fin 2) K obeys the relation ⁅h, e⁆ = 2e.

theorem Ado.lie_slFinTwoBasis_two_one (K : Type u_1) [CommRing K] : ⁅(slFinTwoBasis K) 2, (slFinTwoBasis K) 1⁆ = -(2 • (slFinTwoBasis K) 1)

The standard basis of sl (Fin 2) K obeys the relation ⁅h, f⁆ = -2f.

def Ado.Sl2Std (K : Type u_1) (n : ℕ) : Type u_1

The standard sl₂-module V(n): the (n + 1)-dimensional module of LieAlgebra.SpecialLinear.sl (Fin 2) K with highest weight n. It is a type synonym for the coordinate space Fin (n + 1) → K, carrying the action of Ado.Sl2Std.rep.

Equations

• Ado.Sl2Std K n = (Fin (n + 1) → K)

@[instance_reducible]

instance Ado.Sl2Std.instAddCommGroup (K : Type u_1) [CommRing K] (n : ℕ) : AddCommGroup (Sl2Std K n)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Ado.Sl2Std.instModule (K : Type u_1) [CommRing K] (n : ℕ) : Module K (Sl2Std K n)

Equations

• Ado.Sl2Std.instModule K n = { smul := Ado.Sl2Std.instModule._aux_1 K n, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[instance_reducible, instance 100]

instance Ado.Sl2Std.instModuleRatOfAlgebra (K : Type u_1) [CommRing K] (n : ℕ) [Algebra ℚ K] : Module ℚ (Sl2Std K n)

Equations

• Ado.Sl2Std.instModuleRatOfAlgebra K n = { smul := Ado.Sl2Std.instModuleRatOfAlgebra._aux_1 K n, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[instance 100]

instance Ado.Sl2Std.instIsScalarTowerRat (K : Type u_1) [CommRing K] (n : ℕ) [Algebra ℚ K] : IsScalarTower ℚ K (Sl2Std K n)

@[instance 100]

instance Ado.Sl2Std.instSMulCommClassRat (K : Type u_1) [CommRing K] (n : ℕ) [Algebra ℚ K] : SMulCommClass K ℚ (Sl2Std K n)

The three ladder operators

@[irreducible]

def Ado.Sl2Std.raise (K : Type u_1) [CommRing K] (n : ℕ) : Module.End K (Sl2Std K n)

The raising operator e of V(n), sending the coordinate vector vᵢ to i · vᵢ₋₁; in coordinates, (e · v) i = (i + 1) * v (i + 1), and 0 at the last index. It raises the weight by 2.

Equations

• Ado.Sl2Std.raise K n = { toFun := fun (v : Fin (n + 1) → K) (i : Fin (n + 1)) => if h : ↑i < n then (↑↑i + 1) * v ⟨↑i + 1, ⋯⟩ else 0, map_add' := ⋯, map_smul' := ⋯ }

@[irreducible]

def Ado.Sl2Std.lower (K : Type u_1) [CommRing K] (n : ℕ) : Module.End K (Sl2Std K n)

The lowering operator f of V(n), sending the coordinate vector vᵢ to (n - i) · vᵢ₊₁; in coordinates, (f · v) i = (n - i + 1) * v (i - 1), and 0 at index 0. It lowers the weight by 2.

Equations

• Ado.Sl2Std.lower K n = { toFun := fun (v : Fin (n + 1) → K) (i : Fin (n + 1)) => if h : 0 < ↑i then (↑n - ↑↑i + 1) * v ⟨↑i - 1, ⋯⟩ else 0, map_add' := ⋯, map_smul' := ⋯ }

@[irreducible]

def Ado.Sl2Std.diag (K : Type u_1) [CommRing K] (n : ℕ) : Module.End K (Sl2Std K n)

The Cartan operator h of V(n), diagonal in the coordinate basis with eigenvalue n - 2i at index i. Its eigenvalues are the weights n, n - 2, …, -n.

Equations

• Ado.Sl2Std.diag K n = { toFun := fun (v : Fin (n + 1) → K) (i : Fin (n + 1)) => (↑n - 2 * ↑↑i) * v i, map_add' := ⋯, map_smul' := ⋯ }

The vector space operations in coordinates

The type synonym hides Fin (n + 1) → K from the Pi lemmas, so the pointwise operations are restated here.

@[simp]

theorem Ado.Sl2Std.add_apply {K : Type u_1} [CommRing K] {n : ℕ} (v w : Sl2Std K n) (i : Fin (n + 1)) : (v + w) i = v i + w i

Addition on V(n) is coordinatewise.

@[simp]

theorem Ado.Sl2Std.smul_apply {K : Type u_1} [CommRing K] {n : ℕ} (c : K) (v : Sl2Std K n) (i : Fin (n + 1)) : (c • v) i = c * v i

Scalar multiplication on V(n) is coordinatewise.

@[simp]

theorem Ado.Sl2Std.sub_apply {K : Type u_1} [CommRing K] {n : ℕ} (v w : Sl2Std K n) (i : Fin (n + 1)) : (v - w) i = v i - w i

Subtraction on V(n) is coordinatewise.

@[simp]

theorem Ado.Sl2Std.neg_apply {K : Type u_1} [CommRing K] {n : ℕ} (v : Sl2Std K n) (i : Fin (n + 1)) : (-v) i = -v i

Negation on V(n) is coordinatewise.

@[simp]

theorem Ado.Sl2Std.zero_apply {K : Type u_1} [CommRing K] {n : ℕ} (i : Fin (n + 1)) : 0 i = 0

The zero vector of V(n) has zero coordinates.

@[simp]

theorem Ado.Sl2Std.sum_apply {K : Type u_1} [CommRing K] {n : ℕ} {ι : Type u_2} (s : Finset ι) (f : ι → Sl2Std K n) (i : Fin (n + 1)) : (∑ k ∈ s, f k) i = ∑ k ∈ s, f k i

Finite sums in V(n) are coordinatewise.

The ladder operators in coordinates

@[simp]

theorem Ado.Sl2Std.raise_apply {K : Type u_1} [CommRing K] {n : ℕ} (v : Sl2Std K n) (i : Fin (n + 1)) : (raise K n) v i = if h : ↑i < n then (↑↑i + 1) * v ⟨↑i + 1, ⋯⟩ else 0

The raising operator in coordinates.

@[simp]

theorem Ado.Sl2Std.lower_apply {K : Type u_1} [CommRing K] {n : ℕ} (v : Sl2Std K n) (i : Fin (n + 1)) : (lower K n) v i = if h : 0 < ↑i then (↑n - ↑↑i + 1) * v ⟨↑i - 1, ⋯⟩ else 0

The lowering operator in coordinates.

@[simp]

theorem Ado.Sl2Std.diag_apply {K : Type u_1} [CommRing K] {n : ℕ} (v : Sl2Std K n) (i : Fin (n + 1)) : (diag K n) v i = (↑n - 2 * ↑↑i) * v i

The Cartan operator in coordinates.

theorem Ado.Sl2Std.raise_lower_apply {K : Type u_1} [CommRing K] {n : ℕ} (v : Sl2Std K n) (i : Fin (n + 1)) : (raise K n) ((lower K n) v) i = (↑↑i + 1) * (↑n - ↑↑i) * v i

Raising after lowering is diagonal, with eigenvalue (i + 1)(n - i) at index i. The statement is uniform in i: at the top of the string, i = n, the raising operator reads past the end and returns 0, and the coefficient n - i vanishes to match.

theorem Ado.Sl2Std.lower_raise_apply {K : Type u_1} [CommRing K] {n : ℕ} (v : Sl2Std K n) (i : Fin (n + 1)) : (lower K n) ((raise K n) v) i = ↑↑i * (↑n - ↑↑i + 1) * v i

Lowering after raising is diagonal, with eigenvalue i(n - i + 1) at index i.

theorem Ado.Sl2Std.lie_raise_lower {K : Type u_1} [CommRing K] {n : ℕ} : ⁅raise K n, lower K n⁆ = diag K n

The sl₂ relation ⁅e, f⁆ = h for the ladder operators: the two diagonal operators of Ado.Sl2Std.raise_lower_apply and Ado.Sl2Std.lower_raise_apply differ by n - 2i.

theorem Ado.Sl2Std.lie_diag_raise {K : Type u_1} [CommRing K] {n : ℕ} : ⁅diag K n, raise K n⁆ = 2 • raise K n

The sl₂ relation ⁅h, e⁆ = 2e for the ladder operators.

theorem Ado.Sl2Std.lie_diag_lower {K : Type u_1} [CommRing K] {n : ℕ} : ⁅diag K n, lower K n⁆ = -(2 • lower K n)

The sl₂ relation ⁅h, f⁆ = -2f for the ladder operators.

The representation

noncomputable def Ado.Sl2Std.rep (K : Type u_1) [CommRing K] (n : ℕ) : ↥(LieAlgebra.SpecialLinear.sl (Fin 2) K) →ₗ⁅K⁆ Module.End K (Sl2Std K n)

The standard representation of sl (Fin 2) K on V(n), sending the standard basis (e, f, h) of Ado.slFinTwoBasis to the three ladder operators, which obey the same relations.

Equations

• Ado.Sl2Std.rep K n = Ado.lieHomOfSl2Basis (Ado.slFinTwoBasis K) ⋯ ⋯ ⋯ (Ado.Sl2Std.raise K n) (Ado.Sl2Std.lower K n) (Ado.Sl2Std.diag K n) ⋯ ⋯ ⋯

@[instance_reducible]

noncomputable instance Ado.Sl2Std.instLieRingModule (K : Type u_1) [CommRing K] (n : ℕ) : LieRingModule (↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) (Sl2Std K n)

V(n) is a Lie ring module over sl (Fin 2) K, by transport along Ado.Sl2Std.rep.

Equations

• Ado.Sl2Std.instLieRingModule K n = LieRingModule.compLieHom (Ado.Sl2Std K n) (Ado.Sl2Std.rep K n)

instance Ado.Sl2Std.instLieModule (K : Type u_1) [CommRing K] (n : ℕ) : LieModule K (↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) (Sl2Std K n)

V(n) is a Lie module over sl (Fin 2) K.

instance Ado.Sl2Std.instFree (K : Type u_1) [CommRing K] (n : ℕ) : Module.Free K (Sl2Std K n)

instance Ado.Sl2Std.instFinite (K : Type u_1) [CommRing K] (n : ℕ) : Module.Finite K (Sl2Std K n)

instance Ado.Sl2Std.instNontrivial (K : Type u_1) (n : ℕ) [Nontrivial K] : Nontrivial (Sl2Std K n)

noncomputable def Ado.Sl2Std.basis (K : Type u_1) [CommRing K] (n : ℕ) : Module.Basis (Fin (n + 1)) K (Sl2Std K n)

The coordinate basis v₀, …, vₙ of V(n), a weight basis for the Cartan operator.

Equations

• Ado.Sl2Std.basis K n = Pi.basisFun K (Fin (n + 1))

theorem Ado.Sl2Std.basis_eq {K : Type u_1} [CommRing K] {n : ℕ} (i : Fin (n + 1)) : (basis K n) i = Pi.single i 1

The coordinate basis consists of the standard unit vectors.

@[simp]

theorem Ado.Sl2Std.basis_repr_apply {K : Type u_1} [CommRing K] {n : ℕ} (v : Sl2Std K n) (i : Fin (n + 1)) : ((basis K n).repr v) i = v i

Coordinates of a vector in the coordinate basis are its values.

@[simp]

theorem Ado.Sl2Std.basis_apply {K : Type u_1} [CommRing K] {n : ℕ} (i j : Fin (n + 1)) : (basis K n) i j = if j = i then 1 else 0

The coordinates of a coordinate basis vector.

theorem Ado.Sl2Std.lie_eq_rep_apply {K : Type u_1} [CommRing K] {n : ℕ} (x : ↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) (v : Sl2Std K n) : ⁅x, v⁆ = ((rep K n) x) v

The action of sl (Fin 2) K on V(n) is the one given by Ado.Sl2Std.rep. This is the elimination lemma for Ado.Sl2Std.instLieRingModule, which is that action transported along Ado.Sl2Std.rep.

theorem Ado.Sl2Std.rep_apply_basis {K : Type u_1} [CommRing K] {n : ℕ} (i : Fin 3) : (rep K n) ((slFinTwoBasis K) i) = ![raise K n, lower K n, diag K n] i

The representation sends the standard basis of sl (Fin 2) K to the ladder operators.

theorem Ado.Sl2Std.lie_slFinTwoBasis_zero {K : Type u_1} [CommRing K] {n : ℕ} (v : Sl2Std K n) : ⁅(slFinTwoBasis K) 0, v⁆ = (raise K n) v

The element e of the standard sl₂ triple acts on V(n) as the raising operator.

theorem Ado.Sl2Std.lie_slFinTwoBasis_one {K : Type u_1} [CommRing K] {n : ℕ} (v : Sl2Std K n) : ⁅(slFinTwoBasis K) 1, v⁆ = (lower K n) v

The element f of the standard sl₂ triple acts on V(n) as the lowering operator.

theorem Ado.Sl2Std.lie_slFinTwoBasis_two {K : Type u_1} [CommRing K] {n : ℕ} (v : Sl2Std K n) : ⁅(slFinTwoBasis K) 2, v⁆ = (diag K n) v

The element h of the standard sl₂ triple acts on V(n) as the Cartan operator.

theorem Ado.Sl2Std.toEnd_slFinTwoBasis_one {K : Type u_1} [CommRing K] {n : ℕ} : (LieModule.toEnd K (↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) (Sl2Std K n)) ((slFinTwoBasis K) 1) = lower K n

The lowering operator is the endomorphism by which f acts, which is the form in which TauCeti/Algebra/Lie/Sl2/WeightString.lean writes the weight string.

theorem Ado.Sl2Std.finrank_eq {K : Type u_1} [CommRing K] {n : ℕ} [StrongRankCondition K] : Module.finrank K (Sl2Std K n) = n + 1

V(n) has rank n + 1, the value that Ado.finrank_eq_of_hasPrimitiveVectorWith forces on any irreducible with a primitive vector of weight n.

The ladder on the coordinate basis

theorem Ado.Sl2Std.raise_basis {K : Type u_1} [CommRing K] {n : ℕ} (i : Fin (n + 1)) : (raise K n) ((basis K n) i) = ↑↑i • (basis K n) ⟨↑i - 1, ⋯⟩

The raising operator on the coordinate basis: e · vᵢ = i · vᵢ₋₁. The vanishing coefficient at i = 0 makes the statement uniform, the index i - 1 there being irrelevant.

theorem Ado.Sl2Std.raise_basis_zero {K : Type u_1} [CommRing K] {n : ℕ} : (raise K n) ((basis K n) 0) = 0

The raising operator kills the highest weight vector v₀.

theorem Ado.Sl2Std.diag_basis {K : Type u_1} [CommRing K] {n : ℕ} (i : Fin (n + 1)) : (diag K n) ((basis K n) i) = (↑n - 2 * ↑↑i) • (basis K n) i

The Cartan operator on the coordinate basis: h · vᵢ = (n - 2i) · vᵢ.

theorem Ado.Sl2Std.lower_basis {K : Type u_1} [CommRing K] {n : ℕ} (i : Fin (n + 1)) (h : ↑i < n) : (lower K n) ((basis K n) i) = (↑n - ↑↑i) • (basis K n) ⟨↑i + 1, ⋯⟩

The lowering operator on the coordinate basis: f · vᵢ = (n - i) · vᵢ₊₁, for i < n.

@[simp]

theorem Ado.Sl2Std.lower_basis_last {K : Type u_1} [CommRing K] {n : ℕ} : (lower K n) ((basis K n) (Fin.last n)) = 0

The lowering operator kills the lowest weight vector vₙ. This is the counterpart at the bottom of the string of Ado.Sl2Std.raise_basis_zero, and the case i = n that Ado.Sl2Std.lower_basis leaves out.

theorem Ado.Sl2Std.lower_pow_basis_zero {K : Type u_1} [CommRing K] {n : ℕ} (i : Fin (n + 1)) : (lower K n ^ ↑i) ((basis K n) 0) = (∏ j ∈ Finset.range ↑i, (↑n - ↑j)) • (basis K n) i

The lowering operator walks v₀ along the coordinate basis. After i steps the highest weight vector has become vᵢ, scaled by the product n(n - 1)⋯(n - i + 1) of the coefficients picked up on the way. This is the weight string of V(n), read in coordinates.

The coordinate basis indexed by the naturals

noncomputable def Ado.Sl2Std.basisVector (K : Type u_1) [CommRing K] (n i : ℕ) : Sl2Std K n

The i-th vector of the coordinate basis of V(n), extended by zero for i past the end of the weight string. Indexing by ℕ rather than by Fin (n + 1) lets finite sums use natural indices without carrying bounds through every rewrite.

Equations

• Ado.Sl2Std.basisVector K n i = if h : i < n + 1 then (Ado.Sl2Std.basis K n) ⟨i, h⟩ else 0

@[simp]

theorem Ado.Sl2Std.basisVector_apply {K : Type u_1} [CommRing K] {n i : ℕ} (j : Fin (n + 1)) : basisVector K n i j = if ↑j = i then 1 else 0

theorem Ado.Sl2Std.basisVector_eq_basis {K : Type u_1} [CommRing K] {n i : ℕ} (h : i < n + 1) : basisVector K n i = (basis K n) ⟨i, h⟩

Inside the weight string the extension by zero is the coordinate basis vector itself.

theorem Ado.Sl2Std.basisVector_eq_zero {K : Type u_1} [CommRing K] {n i : ℕ} (h : n < i) : basisVector K n i = 0

Past the end of the weight string the extension by zero vanishes.

theorem Ado.Sl2Std.diag_basisVector {K : Type u_1} [CommRing K] {n i : ℕ} : (diag K n) (basisVector K n i) = (↑n - 2 * ↑i) • basisVector K n i

The Cartan operator scales the i-th coordinate basis vector by n - 2i, uniformly in i: past the end of the string both sides vanish.

theorem Ado.Sl2Std.raise_basisVector {K : Type u_1} [CommRing K] {n i : ℕ} (hi : i ≤ n) : (raise K n) (basisVector K n i) = ↑i • basisVector K n (i - 1)

The raising operator sends the i-th coordinate basis vector to i times the (i-1)-st, for i inside the weight string.

theorem Ado.Sl2Std.lower_basisVector {K : Type u_1} [CommRing K] {n i : ℕ} : (lower K n) (basisVector K n i) = (↑n - ↑i) • basisVector K n (i + 1)

The lowering operator sends the i-th coordinate basis vector to (n - i) times the (i+1)-st, uniformly in i: past the end of the weight string both sides vanish.

theorem Ado.Sl2Std.hasPrimitiveVectorWith (K : Type u_1) [CommRing K] (n : ℕ) [Nontrivial K] : ⋯.HasPrimitiveVectorWith ((basis K n) 0) ↑n

v₀ is a primitive vector of weight n for the standard sl₂ triple of sl (Fin 2) K: it is nonzero, h scales it by n, and e kills it.

Powers of the ladder and Cartan operators

theorem Ado.Sl2Std.raise_pow_apply_of_le {K : Type u_1} [CommRing K] {n k : ℕ} (v : Sl2Std K n) (i : Fin (n + 1)) (h : ↑i + k ≤ n) : (raise K n ^ k) v i = ↑((↑i + k).descFactorial k) * v ⟨↑i + k, ⋯⟩

When i + k ≤ n, eᵏ acts on coordinate i by scaling coordinate i + k by (i + k)_(k).

theorem Ado.Sl2Std.raise_pow_apply_eq_zero {K : Type u_1} [CommRing K] {n : ℕ} (k : ℕ) (v : Sl2Std K n) (i : Fin (n + 1)) (h : n < ↑i + k) : (raise K n ^ k) v i = 0

Each application of the raising operator reads the coordinates one place further along, so eᵏ reads past the end of the string once i + k > n.

@[simp]

theorem Ado.Sl2Std.raise_pow_apply {K : Type u_1} [CommRing K] {n : ℕ} (k : ℕ) (v : Sl2Std K n) (i : Fin (n + 1)) : (raise K n ^ k) v i = if h : ↑i + k ≤ n then ↑((↑i + k).descFactorial k) * v ⟨↑i + k, ⋯⟩ else 0

The k-th power of the raising operator reads coordinate i + k with coefficient (i + k)_(k), and vanishes when i + k > n.

theorem Ado.Sl2Std.raise_pow_eq_zero {K : Type u_1} [CommRing K] {n : ℕ} : raise K n ^ (n + 1) = 0

The raising operator is nilpotent on V(n), of exponent at most n + 1.

@[simp]

theorem Ado.Sl2Std.raise_zero {K : Type u_1} [CommRing K] : raise K 0 = 0

On the trivial standard module the raising operator vanishes.

theorem Ado.Sl2Std.isNilpotent_raise {K : Type u_1} [CommRing K] {n : ℕ} : IsNilpotent (raise K n)

The raising operator of V(n) is nilpotent.

theorem Ado.Sl2Std.lower_pow_apply_of_le {K : Type u_1} [CommRing K] {n k : ℕ} (v : Sl2Std K n) (i : Fin (n + 1)) (h : k ≤ ↑i) : (lower K n ^ k) v i = ↑((n - ↑i + k).descFactorial k) * v ⟨↑i - k, ⋯⟩

When k ≤ i, fᵏ acts on coordinate i by scaling coordinate i - k by (n - i + k)_(k).

theorem Ado.Sl2Std.lower_pow_apply_eq_zero {K : Type u_1} [CommRing K] {n : ℕ} (k : ℕ) (v : Sl2Std K n) (i : Fin (n + 1)) (h : ↑i < k) : (lower K n ^ k) v i = 0

Each application of the lowering operator reads the coordinates one place earlier along, so fᵏ reads past the beginning of the string once i < k.

@[simp]

theorem Ado.Sl2Std.lower_pow_apply {K : Type u_1} [CommRing K] {n : ℕ} (k : ℕ) (v : Sl2Std K n) (i : Fin (n + 1)) : (lower K n ^ k) v i = if h : k ≤ ↑i then ↑((n - ↑i + k).descFactorial k) * v ⟨↑i - k, ⋯⟩ else 0

The k-th power of the lowering operator reads coordinate i - k with coefficient (n - i + k)_(k), and vanishes when k > i.

theorem Ado.Sl2Std.lower_pow_eq_zero {K : Type u_1} [CommRing K] {n : ℕ} : lower K n ^ (n + 1) = 0

The lowering operator is nilpotent on V(n), of exponent at most n + 1.

@[simp]

theorem Ado.Sl2Std.lower_zero {K : Type u_1} [CommRing K] : lower K 0 = 0

On the trivial standard module the lowering operator vanishes.

theorem Ado.Sl2Std.isNilpotent_lower {K : Type u_1} [CommRing K] {n : ℕ} : IsNilpotent (lower K n)

The lowering operator of V(n) is nilpotent.

@[simp]

theorem Ado.Sl2Std.diag_pow_apply {K : Type u_1} [CommRing K] {n : ℕ} (k : ℕ) (v : Sl2Std K n) (i : Fin (n + 1)) : (diag K n ^ k) v i = (↑n - 2 * ↑↑i) ^ k * v i

The k-th power of the Cartan operator acts diagonally with eigenvalue (n - 2i)ᵏ on coordinate i.

theorem Ado.Sl2Std.isSl2Triple_diag_raise_lower {K : Type u_1} [CommRing K] {n : ℕ} (hn : ↑n ≠ 0) : IsSl2Triple (diag K n) (raise K n) (lower K n)

The standard-module Cartan and ladder operators form an sl₂ triple whenever the highest weight is nonzero in the coefficient ring.

The Cartan eigenspaces

theorem Ado.Sl2Std.eigenspace_diag {K : Type u_1} [CommRing K] [IsDomain K] {n : ℕ} [CharZero K] (i : Fin (n + 1)) : (diag K n).eigenspace (↑n - 2 * ↑↑i) = K ∙ (basis K n) i

The Cartan eigenspaces of V(n) are the coordinate lines. The eigenspace of h for the weight n - 2i is exactly the line spanned by vᵢ: a vector of that eigenvalue has its jth coordinate killed by 2(i - j), which in characteristic zero vanishes only at j = i.

theorem Ado.Sl2Std.eigenspace_diag_eq_bot {K : Type u_1} [CommRing K] [IsDomain K] {n : ℕ} {μ : K} (hμ : ∀ (i : Fin (n + 1)), μ ≠ ↑n - 2 * ↑↑i) : (diag K n).eigenspace μ = ⊥

The weights of V(n) are exactly n, n - 2, …, -n: no other scalar is an eigenvalue of the Cartan operator, every coordinate of a would-be eigenvector being killed. Characteristic zero is not needed here: it is what makes those n + 1 weights distinct, not what makes them the only ones.

The kernel of the raising operator

theorem Ado.Sl2Std.eq_smul_basis_zero_of_raise_eq_zero {K : Type u_1} [CommRing K] [IsDomain K] {n : ℕ} [CharZero K] {v : Sl2Std K n} (h : (raise K n) v = 0) : v = v 0 • (basis K n) 0

The kernel of the raising operator is the highest weight line. In characteristic zero the coefficients i + 1 are nonzero, so a vector killed by e has all coordinates but the zeroth equal to zero.

The kernel of the lowering operator

theorem Ado.Sl2Std.eq_smul_basis_last_of_lower_eq_zero {K : Type u_1} [CommRing K] [IsDomain K] {n : ℕ} [CharZero K] {v : Sl2Std K n} (h : (lower K n) v = 0) : v = v (Fin.last n) • (basis K n) (Fin.last n)

The kernel of the lowering operator is the lowest weight line. In characteristic zero the coefficients n - i + 1 are nonzero until the end of the string, so a vector killed by f has all coordinates but the last equal to zero.

The multiplicity of the weights

theorem Ado.Sl2Std.finrank_eigenspace_diag {K : Type u_1} [Field K] [CharZero K] {n : ℕ} (i : Fin (n + 1)) : Module.finrank K ↥((diag K n).eigenspace (↑n - 2 * ↑↑i)) = 1

The weights of V(n) have multiplicity one: each Cartan eigenspace is a line.

Irreducibility

theorem Ado.Sl2Std.eq_top_of_raise_mem_of_lower_mem {K : Type u_1} [Field K] [CharZero K] {n : ℕ} (N : Submodule K (Sl2Std K n)) (hN : N ≠ ⊥) (hraise : ∀ w ∈ N, (raise K n) w ∈ N) (hlower : ∀ w ∈ N, (lower K n) w ∈ N) : N = ⊤

The engine of irreducibility. A nonzero subspace of V(n) stable under the raising and lowering operators is the whole of V(n): raising produces the highest weight vector, lowering walks it along the coordinate basis, and that basis spans.

instance Ado.Sl2Std.isIrreducible {K : Type u_1} [Field K] [CharZero K] {n : ℕ} : LieModule.IsIrreducible K (↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) (Sl2Std K n)

V(n) is an irreducible sl (Fin 2) K-module.

instance Ado.Sl2Std.isIrreducible_toLieSubalgebra {K : Type u_1} [Field K] [CharZero K] {n : ℕ} : LieModule.IsIrreducible K (↥(IsSl2Triple.toLieSubalgebra K ⋯)) (Sl2Std K n)

V(n) is irreducible over the subalgebra generated by the standard sl₂ triple. This is the form of irreducibility that the classification of TauCeti/Algebra/Lie/Sl2/WeightString.lean asks for; here the two forms agree, since the standard triple generates all of sl (Fin 2) K (Ado.toLieSubalgebra_isSl2Triple_single_eq_top), so Ado.isIrreducible_of_eq_top carries the one to the other.

noncomputable def Ado.Sl2Std.lieModuleEquiv {K : Type u_1} [Field K] [CharZero K] {n : ℕ} {M : Type u_2} [AddCommGroup M] [Module K M] [LieRingModule (↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) M] [LieModule K (↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) M] [IsNoetherian K M] [LieModule.IsIrreducible K (↥(IsSl2Triple.toLieSubalgebra K ⋯)) M] {m : M} (P : ⋯.HasPrimitiveVectorWith m ↑n) : M ≃ₗ⁅K,↥(IsSl2Triple.toLieSubalgebra K ⋯)⁆ Sl2Std K n

The classification of the finite-dimensional irreducible sl₂-modules. A Noetherian module over sl (Fin 2) K which is irreducible over the subalgebra of the standard triple and carries a primitive vector of weight n is equivalent to V(n). Together with Ado.Sl2Std.hasPrimitiveVectorWith and Ado.Sl2Std.isIrreducible_toLieSubalgebra this exhibits V(n) as the irreducible of highest weight n: existence here, uniqueness in Ado.lieModuleEquivOfHasPrimitiveVectorWith.

Equations

• Ado.Sl2Std.lieModuleEquiv P = Ado.lieModuleEquivOfHasPrimitiveVectorWith P ⋯

theorem Ado.Sl2Std.lieModuleEquiv_apply_basis {K : Type u_1} [Field K] [CharZero K] {n : ℕ} {M : Type u_2} [AddCommGroup M] [Module K M] [LieRingModule (↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) M] [LieModule K (↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) M] [IsNoetherian K M] [LieModule.IsIrreducible K (↥(IsSl2Triple.toLieSubalgebra K ⋯)) M] {m : M} (P : ⋯.HasPrimitiveVectorWith m ↑n) (i : Fin (n + 1)) : (lieModuleEquiv P) ((basisOfHasPrimitiveVectorWith P) i) = (∏ j ∈ Finset.range ↑i, (↑n - ↑j)) • (basis K n) i

The classification read in coordinates: the ladder basis m, f • m, …, fⁿ • m of M goes to the coordinate basis of V(n), position by position, scaled by the coefficients n(n - 1)⋯(n - i + 1) that the lowering operator picks up on the way down (Ado.Sl2Std.lower_pow_basis_zero).

The standard module of an arbitrary generating triple

noncomputable def Ado.Sl2Std.repOfIsSl2Triple {K : Type u} [CommRing K] [IsDomain K] [CharZero K] {L : Type u_1} [LieRing L] [LieAlgebra K L] [Module.IsTorsionFree K L] {h e f : L} (t : IsSl2Triple h e f) (htop : IsSl2Triple.toLieSubalgebra K t = ⊤) (n : ℕ) : L →ₗ⁅K⁆ Module.End K (Sl2Std K n)

The standard representation of a Lie algebra generated by an sl₂ triple on V(n), sending the triple (e, f, h) to the three ladder operators. It is built exactly as Ado.Sl2Std.rep is, from the basis Ado.basisOfIsSl2Triple, which obeys the same relations as the standard basis of sl (Fin 2) K.

Equations

• Ado.Sl2Std.repOfIsSl2Triple t htop n = Ado.lieHomOfSl2Basis (Ado.basisOfIsSl2Triple t htop) ⋯ ⋯ ⋯ (Ado.Sl2Std.raise K n) (Ado.Sl2Std.lower K n) (Ado.Sl2Std.diag K n) ⋯ ⋯ ⋯

theorem Ado.Sl2Std.repOfIsSl2Triple_apply_basis {K : Type u} [CommRing K] [IsDomain K] [CharZero K] {L : Type u_1} [LieRing L] [LieAlgebra K L] [Module.IsTorsionFree K L] {h e f : L} (t : IsSl2Triple h e f) (htop : IsSl2Triple.toLieSubalgebra K t = ⊤) (n : ℕ) (i : Fin 3) : (repOfIsSl2Triple t htop n) ((basisOfIsSl2Triple t htop) i) = ![raise K n, lower K n, diag K n] i

The representation of a Lie algebra generated by an sl₂ triple sends the basis of the triple to the ladder operators.

@[simp]

theorem Ado.Sl2Std.repOfIsSl2Triple_apply_e {K : Type u} [CommRing K] [IsDomain K] [CharZero K] {L : Type u_1} [LieRing L] [LieAlgebra K L] [Module.IsTorsionFree K L] {h e f : L} (t : IsSl2Triple h e f) (htop : IsSl2Triple.toLieSubalgebra K t = ⊤) (n : ℕ) : (repOfIsSl2Triple t htop n) e = raise K n

The element e of the triple acts on V(n) as the raising operator.

@[simp]

theorem Ado.Sl2Std.repOfIsSl2Triple_apply_f {K : Type u} [CommRing K] [IsDomain K] [CharZero K] {L : Type u_1} [LieRing L] [LieAlgebra K L] [Module.IsTorsionFree K L] {h e f : L} (t : IsSl2Triple h e f) (htop : IsSl2Triple.toLieSubalgebra K t = ⊤) (n : ℕ) : (repOfIsSl2Triple t htop n) f = lower K n

The element f of the triple acts on V(n) as the lowering operator.

@[simp]

theorem Ado.Sl2Std.repOfIsSl2Triple_apply_h {K : Type u} [CommRing K] [IsDomain K] [CharZero K] {L : Type u_1} [LieRing L] [LieAlgebra K L] [Module.IsTorsionFree K L] {h e f : L} (t : IsSl2Triple h e f) (htop : IsSl2Triple.toLieSubalgebra K t = ⊤) (n : ℕ) : (repOfIsSl2Triple t htop n) h = diag K n

The element h of the triple acts on V(n) as the Cartan operator.

theorem Ado.exists_isIrreducible_hasPrimitiveVectorWith {K : Type u} [Field K] [CharZero K] {L : Type u_1} [LieRing L] [LieAlgebra K L] {h e f : L} (t : IsSl2Triple h e f) (htop : IsSl2Triple.toLieSubalgebra K t = ⊤) (n : ℕ) : ∃ (V : Type u) (x : AddCommGroup V) (x_1 : Module K V) (x_2 : LieRingModule L V) (_ : LieModule K L V) (v : V), FiniteDimensional K V ∧ LieModule.IsIrreducible K L V ∧ t.HasPrimitiveVectorWith v ↑n

Existence of the standard irreducible V(n). For every n : ℕ, a Lie algebra generated by an sl₂ triple has a finite-dimensional module, irreducible over the whole algebra, carrying a primitive vector of weight n: it is Ado.Sl2Std K n with the action transported along Ado.Sl2Std.repOfIsSl2Triple, which is the reusable form of this statement.

Together with Ado.finrank_eq_of_hasPrimitiveVectorWith and Ado.lieModuleEquivOfHasPrimitiveVectorWith this pins down the modules that carry a primitive vector of weight n and are irreducible over the subalgebra of the triple: for each n : ℕ there is one, it has rank n + 1, and any two are equivalent. That every finite-dimensional irreducible carries a primitive vector is a further statement, proved in TauCeti/Algebra/Lie/Sl2/Classification.lean (Ado.exists_hasPrimitiveVectorWith), so this is the existence half of the classification rather than the whole of it.