Simple Weyl representatives in the type-A carrier

At the Bourbaki node i of the type A_r carrier TauCeti.SlStd.groupScheme r, the numbered root subgroups x_{α_i} and x_{-α_i} give the Weyl representative

n_i = x_{α_i}(1) x_{-α_i}(-1) x_{α_i}(1),

a point of the carrier over every commutative ring (TauCeti.SlStd.simpleWeylPoint). Conjugation by n_i interchanges the two root subgroups at i, negating the parameter, reflects the weight torus by the root α_i, and so normalizes the torus.

In coordinates n_i is the signed permutation matrix of the transposition of i and i + 1, sending e_i to -e_{i+1} and e_{i+1} to e_i. It satisfies the Chevalley relation n_i² = h_i(-1), where h_i(-1) is the torus point with value -1 at i and 1 elsewhere, and over a nontrivial ring its class in the pointwise normalizer quotient of the torus has order exactly two.

Main declarations

• TauCeti.SlStd.simpleWeylPoint: the Weyl representative at a node, as a carrier point.
• TauCeti.SlStd.simpleWeylPoint_conj_rootSubgroupPoints: n_i x_{α_i}(u) n_i⁻¹ = x_{-α_i}(-u).
• TauCeti.SlStd.simpleWeylPoint_conj_weightTorusPoints and TauCeti.SlStd.simpleWeylPoint_mem_normalizer: n_i reflects and normalizes the weight torus.
• TauCeti.SlStd.coe_simpleWeylPoint_apply: the matrix entries of n_i.
• TauCeti.SlStd.simpleWeylPoint_sq: the Chevalley relation n_i² = h_i(-1).
• TauCeti.SlStd.orderOf_simpleWeylClass: the class of n_i in the torus normalizer quotient has order two over a nontrivial ring.

References

• R. W. Carter, Simple Groups of Lie Type, §§6.4 and 7.1.
• R. Steinberg, Lectures on Chevalley Groups, §3.

theorem TauCeti.SlStd.points_eq_kostantToralPointsSubgroup (r : ℕ) (A : Type v) [CommRing A] : points r A = UniversalEnvelopingAlgebra.kostantToralPointsSubgroup (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ ⋯ (latticeBasis r) (weight r) A

The points of the type A_r carrier are the points of the generic Kostant toral closure it is cut out from.

theorem TauCeti.SlStd.isSl2Triple_rep (r : ℕ) (i : Fin r) : IsSl2Triple ((rep r) ((UniversalEnvelopingAlgebra.ι ℚ) (cartanGenerator r i))) ((rep r) ((UniversalEnvelopingAlgebra.ι ℚ) (rootGenerator r (Sum.inl i)))) ((rep r) ((UniversalEnvelopingAlgebra.ι ℚ) (rootGenerator r (Sum.inr i))))

The standard representation carries the numbered sl₂ triple at node i to an sl₂ triple of endomorphisms of the standard module.

noncomputable def TauCeti.SlStd.simpleWeylPoint (r : ℕ) (i : Fin r) (A : Type v) [CommRing A] : ↥(points r A)

The Weyl representative at the node i: x_{α_i}(1) x_{-α_i}(-1) x_{α_i}(1), as a point of the type A_r carrier.

Equations

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

theorem TauCeti.SlStd.coe_simpleWeylPoint (r : ℕ) (i : Fin r) (A : Type v) [CommRing A] : ↑(simpleWeylPoint r i A) = (Units.map ↑(LinearMap.toMatrixAlgEquiv (Module.Basis.baseChange A (latticeBasis r))).toMulEquiv) (UniversalEnvelopingAlgebra.kostantWeylGL (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ ⋯ ⋯ A)

In the coordinate basis, the Weyl representative is the matrix of the integral Weyl automorphism of the standard lattice.

@[simp]

theorem TauCeti.SlStd.map_simpleWeylPoint (r : ℕ) (i : Fin r) {A : Type u} {B : Type v} [CommRing A] [CommRing B] (φ : A →+* B) : ((pointsPresentation r A).map (pointsPresentation r B) φ) (simpleWeylPoint r i A) = simpleWeylPoint r i B

The Weyl representative is natural in the ring of points.

theorem TauCeti.SlStd.simpleWeylPoint_conj_rootSubgroupPoints (r : ℕ) (i : Fin r) (A : Type v) [CommRing A] (u : A) : simpleWeylPoint r i A * (rootSubgroupPoints r (Sum.inl i) A) (Multiplicative.ofAdd u) * (simpleWeylPoint r i A)⁻¹ = (rootSubgroupPoints r (Sum.inr i) A) (Multiplicative.ofAdd (-u))

Conjugation by the Weyl representative at i interchanges the root subgroups at i: n_i x_{α_i}(u) n_i⁻¹ = x_{-α_i}(-u).

theorem TauCeti.SlStd.simpleWeylPoint_conj_weightTorusPoints (r : ℕ) (i : Fin r) (A : Type v) [CommRing A] (s : Fin r → Aˣ) : simpleWeylPoint r i A * (weightTorusPoints r A) s * (simpleWeylPoint r i A)⁻¹ = (weightTorusPoints r A) ((weylReflectTorusPoint (rootGeneratorWeight r (Sum.inl i)) i) s)

Conjugation by the Weyl representative at i reflects the weight torus by the root α_i.

theorem TauCeti.SlStd.simpleWeylPoint_mem_normalizer (r : ℕ) (i : Fin r) (A : Type v) [CommRing A] : simpleWeylPoint r i A ∈ Subgroup.normalizer ↑(weightTorusPoints r A).range

The Weyl representative at i normalizes the weight torus.

The matrix of the Weyl representative

theorem TauCeti.SlStd.coe_simpleWeylPoint_apply (r : ℕ) (i : Fin r) (A : Type v) [CommRing A] (a b : Fin (r + 1)) : ↑↑(simpleWeylPoint r i A) a b = if a = (Equiv.swap i.castSucc i.succ) b then if b = i.castSucc then -1 else 1 else 0

The matrix of the Weyl representative at i is the signed permutation matrix of the transposition of i and i + 1: its column j is -e_{i+1} for j = i, e_i for j = i + 1, and e_j otherwise.

@[simp]

theorem TauCeti.SlStd.simpleWeylPoint_sq (r : ℕ) (i : Fin r) (A : Type v) [CommRing A] : simpleWeylPoint r i A ^ 2 = (weightTorusPoints r A) (Pi.mulSingle i (-1))

The Chevalley relation n_i² = h_i(-1): the square of the Weyl representative at i is the torus point with value -1 at i and 1 elsewhere.

theorem TauCeti.SlStd.simpleWeylPoint_conj_rootSubgroupPoints_inr (r : ℕ) (i : Fin r) (A : Type v) [CommRing A] (u : A) : simpleWeylPoint r i A * (rootSubgroupPoints r (Sum.inr i) A) (Multiplicative.ofAdd u) * (simpleWeylPoint r i A)⁻¹ = (rootSubgroupPoints r (Sum.inl i) A) (Multiplicative.ofAdd (-u))

Conjugation by the Weyl representative at i sends the negative root subgroup at i to the positive one, negating the parameter: n_i x_{-α_i}(u) n_i⁻¹ = x_{α_i}(-u).

The normalizer class

noncomputable def TauCeti.SlStd.simpleWeylNormalizerPoint (r : ℕ) (i : Fin r) (A : Type v) [CommRing A] : ↥(Subgroup.normalizer ↑(weightTorusPoints r A).range)

The Weyl representative at i, as a point of the normalizer of the weight torus.

Equations

• TauCeti.SlStd.simpleWeylNormalizerPoint r i A = ⟨TauCeti.SlStd.simpleWeylPoint r i A, ⋯⟩

@[simp]

theorem TauCeti.SlStd.coe_simpleWeylNormalizerPoint (r : ℕ) (i : Fin r) (A : Type v) [CommRing A] : ↑(simpleWeylNormalizerPoint r i A) = simpleWeylPoint r i A

noncomputable def TauCeti.SlStd.simpleWeylClass (r : ℕ) (i : Fin r) (A : Type v) [CommRing A] : (weightTorusPoints r A).range.normalizerQuotient

The class of the Weyl representative at i in the normalizer quotient of the weight torus.

Equations

• TauCeti.SlStd.simpleWeylClass r i A = (TauCeti.SlStd.weightTorusPoints r A).range.normalizerQuotientMk (TauCeti.SlStd.simpleWeylNormalizerPoint r i A)

@[simp]

theorem TauCeti.SlStd.simpleWeylClass_sq (r : ℕ) (i : Fin r) (A : Type v) [CommRing A] : simpleWeylClass r i A ^ 2 = 1

The Weyl class at i has square one.

theorem TauCeti.SlStd.simpleWeylPoint_notMem_range (r : ℕ) (i : Fin r) (A : Type v) [CommRing A] [Nontrivial A] : simpleWeylPoint r i A ∉ (weightTorusPoints r A).range

Over a nontrivial ring, the Weyl representative at i is not a torus point: its (i, i + 1) entry is 1, while torus points are diagonal.

theorem TauCeti.SlStd.simpleWeylClass_ne_one (r : ℕ) (i : Fin r) (A : Type v) [CommRing A] [Nontrivial A] : simpleWeylClass r i A ≠ 1

Over a nontrivial ring, the Weyl class at i is not the identity.

@[simp]

theorem TauCeti.SlStd.orderOf_simpleWeylClass (r : ℕ) (i : Fin r) (A : Type v) [CommRing A] [Nontrivial A] : orderOf (simpleWeylClass r i A) = 2

Over a nontrivial ring, the Weyl class at i has order exactly two in the normalizer quotient of the weight torus.