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

TauCeti.SpStd.groupScheme n is defined as the closed subgroup scheme of GL_(2n+2) over ℤ generated jointly by the numbered positive and negative simple-root subgroups of type C_(n+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 homomorphism out of the carrier is determined by its restrictions to the root subgroups.

The long simple root 2 e_(n+1) of C_(n+1) is the obstruction to the coprimality criterion for coroot values in the group generated by the root subgroups: its row of the Cartan matrix is (0, …, 0, -2, 2), so the values of that root on the weight torus are the squares, not all units. What is used instead is that every numbered root generator squares to zero in the standard representation, whose weights ± e_k pair with every simple coroot to 1, 0 or -1; the square-zero rank-one identity then reaches each coroot value at an arbitrary unit.

Main results

• TauCeti.SpStd.isSl2Triple_rep_rootGenerator: the represented generators at a Bourbaki node form an sl₂ triple.
• TauCeti.SpStd.weightTorusSubgroup_le_elementarySubgroup: over every commutative ring the represented weight torus lies in the group generated by the root subgroups.
• TauCeti.SpStd.definingIdeal_eq_kostantGeneratedDefiningIdeal and TauCeti.SpStd.groupScheme_eq_kostantGeneratedGroupScheme: the carrier is the root-generated group scheme.
• TauCeti.SpStd.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.

The represented sl₂ triples

theorem TauCeti.SpStd.isSl2Triple_rep_rootGenerator (n : ℕ) (i : Fin (n + 1)) : IsSl2Triple ((rep n) ((UniversalEnvelopingAlgebra.ι ℚ) (cartanGenerator n i))) ((rep n) ((UniversalEnvelopingAlgebra.ι ℚ) (rootGenerator n (Sum.inl i)))) ((rep n) ((UniversalEnvelopingAlgebra.ι ℚ) (rootGenerator n (Sum.inr i))))

The represented generators at a Bourbaki node form an sl₂ triple. This is the sl₂ triple of TauCeti.SpStd.isSl2Triple_rootGenerator carried along the standard representation.

Generation of the weight torus

theorem TauCeti.SpStd.coordinateCocharacter_mem_elementarySubgroup (n : ℕ) (A : CommAlgCat ℤ) (d : Fin (n + 1)) (u : (↑A)ˣ) : (UniversalEnvelopingAlgebra.kostantCoordinateCocharacter (lattice n).toAddSubgroup (latticeBasis n) (basisWeight n) (↑A) d) u ∈ UniversalEnvelopingAlgebra.kostantElementarySubgroup (rootGenerator n) (cartanGenerator n) (rep n) (lattice n).toAddSubgroup ⋯ ⋯ A

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

theorem TauCeti.SpStd.weightTorusSubgroup_le_elementarySubgroup (n : ℕ) (A : CommAlgCat ℤ) : UniversalEnvelopingAlgebra.kostantTorusSubgroup (lattice n).toAddSubgroup (latticeBasis n) (basisWeight n) ↑A ≤ UniversalEnvelopingAlgebra.kostantElementarySubgroup (rootGenerator n) (cartanGenerator n) (rep n) (lattice n).toAddSubgroup ⋯ ⋯ A

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

Scheme-theoretic generation

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

The full-weight standard type-C_(n+1) 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.SpStd.groupScheme_eq_kostantGeneratedGroupScheme (n : ℕ) : groupScheme n = UniversalEnvelopingAlgebra.kostantGeneratedGroupScheme (rootGenerator n) (cartanGenerator n) (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n)

The full-weight standard type-C_(n+1) carrier is the group scheme generated by its numbered positive and negative simple root subgroups.

instance TauCeti.SpStd.isIso_kostantGeneratedToToral (n : ℕ) : CategoryTheory.IsIso (UniversalEnvelopingAlgebra.kostantGeneratedToToral (rootGenerator n) (cartanGenerator n) (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) (basisWeight n))

The canonical inclusion of the root-generated standard type-C_(n+1) carrier into its toral closure is an isomorphism.

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

A morphism out of the standard type-C_(n+1) carrier is determined by the numbered root subgroups, with no hypothesis on the weight torus.

theorem TauCeti.SpStd.baseChangePresentationIdeal_eq_generated (n : ℕ) (A : Type v) [CommRing A] : UniversalEnvelopingAlgebra.kostantToralBaseChangePresentationIdeal (rootGenerator n) (cartanGenerator n) (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) (basisWeight n) A = UniversalEnvelopingAlgebra.kostantGeneratedGeneralLinearBaseChangeIdeal (rootGenerator n) (cartanGenerator n) (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) A

The transported toral and root-generated presentations of the standard type-C_(n+1) carrier agree over every commutative ring.