The standard type-A carrier is generated by its root subgroups

TauCeti.SlStd.groupScheme r is the closed subgroup scheme of GL_{r+1} over ℤ generated jointly by the Bourbaki-numbered positive and negative simple-root subgroups of sl_{r+1} and by the weight torus of the standard lattice. This file shows that the weight torus is redundant: the carrier is already the subgroup scheme generated by the root subgroups alone, the two defining Hopf ideals agree, and a morphism out of the carrier is determined by its restrictions to the root subgroups.

The criterion used is that every numbered root generator E_{i, i+1} and E_{i+1, i} squares to zero on the standard module: it writes into a coordinate it does not read from. Equivalently, the weights ε₀, …, ε_r of the standard module pair with every simple coroot to 1, 0 or -1, so each simple root string through them has length at most two. The square-zero rank-one identity then reaches the coroot value h_i(u) at an arbitrary unit u, and not merely at the values of the i-th simple root on the weight torus. That distinction is what makes the statements below uniform in the rank: at rank one the only row of the Cartan matrix is (2), whose values on the weight torus are the squares rather than all units, so the coprimality criterion for coroot values does not apply there.

Main results

• TauCeti.SlStd.isSl2Triple_rep_rootGenerator: the numbered generators at a Bourbaki node form an sl₂ triple in the standard representation.
• TauCeti.SlStd.weightTorusSubgroup_le_elementarySubgroup: over every commutative ring the represented weight torus lies in the group generated by the root subgroups.
• TauCeti.SlStd.definingIdeal_eq_kostantGeneratedDefiningIdeal and TauCeti.SlStd.groupScheme_eq_kostantGeneratedGroupScheme: the carrier is the root-generated group scheme, with TauCeti.SlStd.baseChangeDefiningIdeal_eq_kostantGeneratedGeneralLinearBaseChangeIdeal the same equality of ideals after base change to any commutative ring.
• TauCeti.SlStd.groupScheme_hom_ext_of_rootSubgroup: a morphism out of the carrier is determined by its restrictions to the numbered root subgroups, with no hypothesis on the weight torus.

References

• R. Steinberg, Lectures on Chevalley Groups, §3.
• R. W. Carter, Simple Groups of Lie Type, §§6.4 and 7.1.
• TauCeti.Algebra.Lie.Symplectic.StandardCarrier.ToralGeneration, which runs the same square-zero argument on the standard type-C carrier.

The represented sl₂ triples

theorem TauCeti.SlStd.isSl2Triple_rep_rootGenerator (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 represented generators at a Bourbaki node form an sl₂ triple: the triple of TauCeti.SlStd.isSl2Triple_rootGenerator carried along the standard representation.

Generation of the weight torus

theorem TauCeti.SlStd.coordinateCocharacter_mem_elementarySubgroup (r : ℕ) (A : CommAlgCat ℤ) (d : Fin r) (u : (↑A)ˣ) : (UniversalEnvelopingAlgebra.kostantCoordinateCocharacter (lattice r).toAddSubgroup (latticeBasis r) (weight r) (↑A) d) u ∈ UniversalEnvelopingAlgebra.kostantElementarySubgroup (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ ⋯ A

Every coroot value of the standard type-A carrier lies in the group generated by the numbered root subgroups, at every unit of every value ring.

theorem TauCeti.SlStd.weightTorusSubgroup_le_elementarySubgroup (r : ℕ) (A : CommAlgCat ℤ) : UniversalEnvelopingAlgebra.kostantTorusSubgroup (lattice r).toAddSubgroup (latticeBasis r) (weight r) ↑A ≤ UniversalEnvelopingAlgebra.kostantElementarySubgroup (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ ⋯ A

Over every commutative ring the weight torus of the standard type-A carrier lies in the group generated by its numbered root subgroups.

Scheme-theoretic generation

theorem TauCeti.SlStd.definingIdeal_eq_kostantGeneratedDefiningIdeal (r : ℕ) : definingIdeal r = UniversalEnvelopingAlgebra.kostantGeneratedDefiningIdeal (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ ⋯ (latticeBasis r)

The full-weight standard type-A_r carrier is generated scheme-theoretically by its numbered root subgroups. Adjoining the represented weight torus does not change the integral defining Hopf ideal.

theorem TauCeti.SlStd.groupScheme_eq_kostantGeneratedGroupScheme (r : ℕ) : groupScheme r = UniversalEnvelopingAlgebra.kostantGeneratedGroupScheme (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ ⋯ (latticeBasis r)

The full-weight standard type-A_r carrier is the group scheme generated by its numbered positive and negative simple root subgroups.

instance TauCeti.SlStd.isIso_kostantGeneratedToToral (r : ℕ) : CategoryTheory.IsIso (UniversalEnvelopingAlgebra.kostantGeneratedToToral (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ ⋯ (latticeBasis r) (weight r))

The canonical inclusion of the root-generated standard type-A_r carrier into its toral closure is an isomorphism.

theorem TauCeti.SlStd.baseChangeDefiningIdeal_eq_kostantGeneratedGeneralLinearBaseChangeIdeal (r : ℕ) (A : Type v) [CommRing A] : baseChangeDefiningIdeal r A = UniversalEnvelopingAlgebra.kostantGeneratedGeneralLinearBaseChangeIdeal (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ ⋯ (latticeBasis r) A

After base change to any commutative ring, the transported defining ideal of the standard type-A_r carrier is the ideal of the root-generated carrier.

theorem TauCeti.SlStd.groupScheme_hom_ext_of_rootSubgroup (r : ℕ) {Y : CommHopfAlgCat ℤ} (φ ψ : groupScheme r ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)) (hroot : ∀ (k : Fin r ⊕ Fin r), CategoryTheory.CategoryStruct.comp (rootSubgroup r k) φ = CategoryTheory.CategoryStruct.comp (rootSubgroup r k) ψ) : φ = ψ

A morphism out of the standard type-A_r carrier is determined by the numbered root subgroups, with no hypothesis on the weight torus.