The admissible integral lattice in a standard sl₂-module

The standard irreducible sl₂-module TauCeti.Sl2Std ℚ n has its coordinate lattice

V(n)ℤ = {v | vᵢ ∈ ℤ for every i}.

This file proves that V(n)ℤ is an admissible lattice for the rank-one Kostant form. The divided raising and lowering operators act on coordinates by ordinary binomial coefficients, while the Cartan binomials act on the i-th coordinate by the generalized integer binomial coefficient (n - 2i choose k). Consequently every element of the Kostant form preserves the lattice.

The lattice is also identified with Fin (n + 1) → ℤ, proving directly that it is finite free of rank n + 1 and spans V(n) over ℚ. This is the rank-one admissible-lattice input to the Chevalley--Demazure construction in Layer 9 of the ReductiveGroups roadmap.

Main declarations

• TauCeti.Sl2Std.repEnveloping: the enveloping-algebra representation on the standard module V(n).
• TauCeti.Sl2Std.repEnveloping_ι, TauCeti.Sl2Std.repEnveloping_ι', and TauCeti.Sl2Std.repEnveloping_ι_slFinTwoBasis: evaluation on Lie algebra generators.
• TauCeti.Sl2Std.isNilpotent_repEnveloping_root: both root operators are nilpotent.
• TauCeti.Sl2Std.integralLattice: the coordinate ℤ-lattice in V(n).
• TauCeti.Sl2Std.mem_integralLattice_iff: integrality of coordinates.
• TauCeti.Sl2Std.integerCoordinatesLinearEquiv: its identification with Fin (n + 1) → ℤ.
• TauCeti.Sl2Std.coe_integerCoordinatesLinearEquiv_apply and TauCeti.Sl2Std.coe_integerCoordinatesLinearEquiv_symm_apply: coordinate characterizations of the forward and inverse identification.
• TauCeti.Sl2Std.dividedPower_raise_apply and TauCeti.Sl2Std.dividedPower_lower_apply: the integral coordinate formulas for the root divided powers.
• TauCeti.Sl2Std.ringChoose_diag_apply: the coordinate formula for Cartan binomials.
• TauCeti.Sl2Std.kostantForm_apply_mem_integralLattice: the rank-one Kostant form preserves the lattice.
• TauCeti.Sl2Std.kostantFormRep: the canonical ℤ-algebra representation of the rank-one Kostant form on the integral lattice.
• TauCeti.Sl2Std.coe_kostantFormRep_apply: compatibility with the ambient representation.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§26--27.
• J. C. Jantzen, Representations of Algebraic Groups, 2nd ed., II.1.

@[simp]

theorem TauCeti.Sl2Std.dividedPower_raise_apply {K : Type u_1} [CommRing K] {n : ℕ} [Algebra ℚ K] (k : ℕ) (v : Sl2Std K n) (i : Fin (n + 1)) : (Associative.dividedPower k (raise K n)) v i = if h : ↑i + k ≤ n then ↑((↑i + k).choose k) * v ⟨↑i + k, ⋯⟩ else 0

The k-th divided raising operator reads coordinate i + k with the integral coefficient (i + k choose k), and vanishes when that coordinate is past the end of V(n).

@[simp]

theorem TauCeti.Sl2Std.dividedPower_lower_apply {K : Type u_1} [CommRing K] {n : ℕ} [Algebra ℚ K] (k : ℕ) (v : Sl2Std K n) (i : Fin (n + 1)) : (Associative.dividedPower k (lower K n)) v i = if h : k ≤ ↑i then ↑((n - ↑i + k).choose k) * v ⟨↑i - k, ⋯⟩ else 0

The k-th divided lowering operator reads coordinate i - k with the integral coefficient (n - i + k choose k), and vanishes when k > i.

@[simp]

theorem TauCeti.Sl2Std.ringChoose_diag_apply {K : Type u_1} [CommRing K] {n : ℕ} [Algebra ℚ K] (k : ℕ) (v : Sl2Std K n) (i : Fin (n + 1)) : (Ring.choose (diag K n) k) v i = Ring.choose (↑n - 2 * ↑↑i) k * v i

The k-th Cartan binomial acts diagonally on V(n), with eigenvalue (n - 2i choose k) on coordinate i.

noncomputable def TauCeti.Sl2Std.repEnveloping (K : Type u_2) [CommRing K] (n : ℕ) : UniversalEnvelopingAlgebra K ↥(LieAlgebra.SpecialLinear.sl (Fin 2) K) →ₐ[K] Module.End K (Sl2Std K n)

The enveloping-algebra representation on the standard module V(n): the general TauCeti.UniversalEnvelopingAlgebra.representation at the Lie module V(n).

Equations

• TauCeti.Sl2Std.repEnveloping K n = TauCeti.UniversalEnvelopingAlgebra.representation K (↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) (TauCeti.Sl2Std K n)

theorem TauCeti.Sl2Std.repEnveloping_ι {K : Type u_1} [CommRing K] {n : ℕ} (x : ↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) : (repEnveloping K n) ((UniversalEnvelopingAlgebra.ι K) x) = (rep K n) x

The enveloping-algebra representation extends the standard sl₂ representation.

@[simp]

theorem TauCeti.Sl2Std.repEnveloping_ι' {K : Type u_1} [CommRing K] {n : ℕ} (x : ↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) : (repEnveloping K n) ((UniversalEnvelopingAlgebra.mkAlgHom K ↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) ((TensorAlgebra.ι K) x)) = (rep K n) x

The simp-normal form of repEnveloping_ι, stated for the canonical generators as simp writes them: ι K x unfolds to mkAlgHom K _ (TensorAlgebra.ι K x).

theorem TauCeti.Sl2Std.repEnveloping_ι_slFinTwoBasis {K : Type u_1} [CommRing K] {n : ℕ} (i : Fin 3) : (repEnveloping K n) ((UniversalEnvelopingAlgebra.ι K) ((slFinTwoBasis K) i)) = ![raise K n, lower K n, diag K n] i

The enveloping-algebra representation sends the three standard sl₂ basis elements to the raising, lowering, and Cartan operators.

theorem TauCeti.Sl2Std.isNilpotent_repEnveloping_root (K : Type u_2) [CommRing K] (n : ℕ) (i : Fin 2) : IsNilpotent ((repEnveloping K n) ((UniversalEnvelopingAlgebra.ι K) (![(slFinTwoBasis K) 0, (slFinTwoBasis K) 1] i)))

Both root operators of the enveloping-algebra representation on V(n) are nilpotent. They are the raising and lowering operators, whose (n + 1)-st powers vanish.

def TauCeti.Sl2Std.integralLattice (n : ℕ) : Submodule ℤ (Sl2Std ℚ n)

The coordinate ℤ-lattice in the rational standard sl₂-module V(n).

A vector belongs to this submodule exactly when each of its coordinates is an integer viewed in ℚ; see mem_integralLattice_iff.

Equations

• TauCeti.Sl2Std.integralLattice n = TauCeti.coordinateLattice (Fin (n + 1))

@[simp]

theorem TauCeti.Sl2Std.mem_integralLattice_iff (n : ℕ) {v : Sl2Std ℚ n} : v ∈ integralLattice n ↔ ∀ (i : Fin (n + 1)), ∃ (z : ℤ), ↑z = v i

A vector belongs to the standard integral lattice exactly when all its coordinates are integer-valued.

noncomputable def TauCeti.Sl2Std.integerCoordinatesLinearEquiv (n : ℕ) : (Fin (n + 1) → ℤ) ≃ₗ[ℤ] ↥(integralLattice n)

Integer coordinate vectors are linearly equivalent to the standard integral lattice.

Equations

• TauCeti.Sl2Std.integerCoordinatesLinearEquiv n = (TauCeti.coordinateLatticeBasis (Fin (n + 1))).equivFun.symm

@[simp]

theorem TauCeti.Sl2Std.coe_integerCoordinatesLinearEquiv_symm_apply (n : ℕ) (v : ↥(integralLattice n)) (i : Fin (n + 1)) : ↑((integerCoordinatesLinearEquiv n).symm v i) = ↑v i

Inverse evaluation of the coordinate linear equivalence yields the integer coordinates.

@[simp]

theorem TauCeti.Sl2Std.coe_integerCoordinatesLinearEquiv_apply (n : ℕ) (z : Fin (n + 1) → ℤ) (i : Fin (n + 1)) : ↑((integerCoordinatesLinearEquiv n) z) i = ↑(z i)

Forward evaluation of the coordinate linear equivalence on a coordinate vector.

instance TauCeti.Sl2Std.instFreeIntSubtypeRatMemSubmoduleIntegralLattice (n : ℕ) : Module.Free ℤ ↥(integralLattice n)

instance TauCeti.Sl2Std.instFiniteIntSubtypeRatMemSubmoduleIntegralLattice (n : ℕ) : Module.Finite ℤ ↥(integralLattice n)

@[simp]

theorem TauCeti.Sl2Std.finrank_integralLattice (n : ℕ) : Module.finrank ℤ ↥(integralLattice n) = n + 1

The standard integral lattice has rank n + 1.

theorem TauCeti.Sl2Std.dividedPower_raise_mem_integralLattice (n k : ℕ) {v : Sl2Std ℚ n} (hv : v ∈ integralLattice n) : (Associative.dividedPower k (raise ℚ n)) v ∈ integralLattice n

Every divided power of the raising operator preserves the standard integral lattice.

theorem TauCeti.Sl2Std.dividedPower_lower_mem_integralLattice (n k : ℕ) {v : Sl2Std ℚ n} (hv : v ∈ integralLattice n) : (Associative.dividedPower k (lower ℚ n)) v ∈ integralLattice n

Every divided power of the lowering operator preserves the standard integral lattice.

theorem TauCeti.Sl2Std.ringChoose_diag_mem_integralLattice (n k : ℕ) {v : Sl2Std ℚ n} (hv : v ∈ integralLattice n) : (Ring.choose (diag ℚ n) k) v ∈ integralLattice n

Every generalized binomial coefficient in the Cartan operator preserves the standard integral lattice.

theorem TauCeti.Sl2Std.span_integralLattice_eq_top (n : ℕ) : Submodule.span ℚ ↑(integralLattice n) = ⊤

The rational span of the standard integral lattice is the whole standard module.

instance TauCeti.Sl2Std.instIsLatticeIntRatIntegralLattice (n : ℕ) : Submodule.IsLattice ℚ (integralLattice n)

The restricted rank-one Kostant action

noncomputable def TauCeti.Sl2Std.kostantFormRep (n : ℕ) : ↥(UniversalEnvelopingAlgebra.kostantForm ![(slFinTwoBasis ℚ) 0, (slFinTwoBasis ℚ) 1] ![(slFinTwoBasis ℚ) 2]) →ₐ[ℤ] Module.End ℤ ↥(integralLattice n)

The canonical representation of the rank-one Kostant integral form on the standard integral lattice V(n)ℤ.

Equations

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

@[simp]

theorem TauCeti.Sl2Std.coe_kostantFormRep_apply (n : ℕ) (u : ↥(UniversalEnvelopingAlgebra.kostantForm ![(slFinTwoBasis ℚ) 0, (slFinTwoBasis ℚ) 1] ![(slFinTwoBasis ℚ) 2])) (v : ↥(integralLattice n)) : ↑(((kostantFormRep n) u) v) = ((repEnveloping ℚ n) ↑u) ↑v

The ambient action of the restricted Kostant representation agrees with the enveloping-algebra representation on the standard module.

theorem TauCeti.Sl2Std.kostantForm_apply_mem_integralLattice (n : ℕ) (u : UniversalEnvelopingAlgebra ℚ ↥(LieAlgebra.SpecialLinear.sl (Fin 2) ℚ)) (hu : u ∈ UniversalEnvelopingAlgebra.kostantForm ![(slFinTwoBasis ℚ) 0, (slFinTwoBasis ℚ) 1] ![(slFinTwoBasis ℚ) 2]) {v : Sl2Std ℚ n} (hv : v ∈ integralLattice n) : ((repEnveloping ℚ n) u) v ∈ integralLattice n

The rank-one Kostant integral form acts on the standard integral lattice.

The root-vector family is (e, f) and the Cartan family is (h), in the standard basis TauCeti.slFinTwoBasis ℚ.