Kostant root subgroups for the standard sl₂ representation

This file supplies a concrete rank-one witness for the general Kostant root-step criterion. Both roots in the standard two-dimensional sl₂ representation have a unit root step on the integral coordinate lattice, so both resulting root-subgroup morphisms are closed immersions.

Main declarations

• TauCeti.Sl2Std.integralLatticeAddSubgroupBasis: the coordinate basis of the standard integral lattice, viewed as an additive subgroup.
• TauCeti.Sl2Std.repEnveloping_root_apply_basis: each root operator maps one coordinate basis vector to the other and annihilates the remaining vector.
• TauCeti.Sl2Std.kostantRootSubgroupPoints_apply_baseChange_basis_one: the resulting class-two root-subgroup action on the base-changed coordinate basis.
• TauCeti.Sl2Std.nilpotencyClass_repEnveloping_root: both root operators are nilpotent of class exactly two.
• TauCeti.Sl2Std.exists_unit_rootStep_repEnveloping_one: both root operators have a unit root step on the two-dimensional integral lattice.
• TauCeti.Sl2Std.isClosedImmersion_kostantRootSubgroup_one: both associated root subgroups are closed immersions.

noncomputable def TauCeti.Sl2Std.integralLatticeAddSubgroupBasis (n : ℕ) : Module.Basis (Fin (n + 1)) ℤ ↥(integralLattice n).toAddSubgroup

The coordinate basis of the standard integral sl₂ lattice, viewed through its underlying additive subgroup as required by the Kostant root-subgroup construction.

Equations

• TauCeti.Sl2Std.integralLatticeAddSubgroupBasis n = (Pi.basisFun ℤ (Fin (n + 1))).map (TauCeti.Sl2Std.integerCoordinatesLinearEquiv n)

@[simp]

theorem TauCeti.Sl2Std.coe_integralLatticeAddSubgroupBasis_apply (n : ℕ) (i : Fin (n + 1)) : ↑((integralLatticeAddSubgroupBasis n) i) = (basis ℚ n) i

The integral-lattice coordinate basis has the expected underlying rational basis vectors.

theorem TauCeti.Sl2Std.repEnveloping_root_apply_basis (i s : Fin 2) : ((repEnveloping ℚ 1) ((UniversalEnvelopingAlgebra.ι ℚ) (![(slFinTwoBasis ℚ) 0, (slFinTwoBasis ℚ) 1] i))) ↑((integralLatticeAddSubgroupBasis 1) s) = if s = i.rev then ↑((integralLatticeAddSubgroupBasis 1) i) else 0

Each root operator maps one integral basis vector to the other. In the standard two-dimensional sl₂ representation the raising operator sends v₁ to v₀ and kills v₀, and the lowering operator sends v₀ to v₁ and kills v₁; both index changes are Fin.rev.

theorem TauCeti.Sl2Std.nilpotencyClass_repEnveloping_root (i : Fin 2) : nilpotencyClass ((repEnveloping ℚ 1) ((UniversalEnvelopingAlgebra.ι ℚ) (![(slFinTwoBasis ℚ) 0, (slFinTwoBasis ℚ) 1] i))) = 2

Both root operators in the standard two-dimensional sl₂ representation are nilpotent of class exactly two: their square vanishes, and they are themselves nonzero.

theorem TauCeti.Sl2Std.kostantRootSubgroupPoints_apply_baseChange_basis_one {A : Type u_1} [CommRing A] (i s : Fin 2) (f : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) : ↑((UniversalEnvelopingAlgebra.kostantRootSubgroupPoints ![(slFinTwoBasis ℚ) 0, (slFinTwoBasis ℚ) 1] ![(slFinTwoBasis ℚ) 2] (repEnveloping ℚ 1) (integralLattice 1).toAddSubgroup ⋯ i ⋯) f) ((Module.Basis.baseChange A (integralLatticeAddSubgroupBasis 1)) s) = (Module.Basis.baseChange A (integralLatticeAddSubgroupBasis 1)) s + if s = i.rev then Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) • (Module.Basis.baseChange A (integralLatticeAddSubgroupBasis 1)) i else 0

A rank-one Kostant root-subgroup point acts on the base-changed integral basis by the class-two formula v_s ↦ v_s + t v_i when s = i.rev, and fixes v_s otherwise.

theorem TauCeti.Sl2Std.exists_unit_rootStep_repEnveloping_one (i : Fin 2) : ∃ (r : Fin 2) (s : Fin 2) (c : ℤ), IsUnit c ∧ ((repEnveloping ℚ 1) ((UniversalEnvelopingAlgebra.ι ℚ) (![(slFinTwoBasis ℚ) 0, (slFinTwoBasis ℚ) 1] i))) ↑((integralLatticeAddSubgroupBasis 1) s) = c • ↑((integralLatticeAddSubgroupBasis 1) r) ∧ ((repEnveloping ℚ 1) ((UniversalEnvelopingAlgebra.ι ℚ) (![(slFinTwoBasis ℚ) 0, (slFinTwoBasis ℚ) 1] i))) (((repEnveloping ℚ 1) ((UniversalEnvelopingAlgebra.ι ℚ) (![(slFinTwoBasis ℚ) 0, (slFinTwoBasis ℚ) 1] i))) ↑((integralLatticeAddSubgroupBasis 1) s)) = 0

Every root operator in the standard two-dimensional sl₂ representation has a unit root step on the integral coordinate basis. For the raising operator the step is v₁ ↦ v₀; for the lowering operator it is v₀ ↦ v₁.

theorem TauCeti.Sl2Std.isClosedImmersion_kostantRootSubgroup_one (i : Fin 2) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (UniversalEnvelopingAlgebra.kostantRootSubgroup ![(slFinTwoBasis ℚ) 0, (slFinTwoBasis ℚ) 1] ![(slFinTwoBasis ℚ) 2] (repEnveloping ℚ 1) (integralLattice 1).toAddSubgroup ⋯ i ⋯ (integralLatticeAddSubgroupBasis 1)).hom.hom)

Both Kostant root subgroups in the standard two-dimensional integral sl₂ representation are closed immersions. This is a nondegenerate instance of the general root-step criterion.