Generation of the type-B spin carrier by root subgroups

The full-weight type-Bₙ₊₁ spin carrier is defined from its positive and negative numbered simple-root subgroups together with its split weight torus. This file proves that the weight torus is redundant at every rank: the carrier is already the subgroup scheme generated by the root subgroups alone, the two defining Hopf ideals agree over ℤ and after base change, and a morphism out of the carrier is determined by its restrictions to the root subgroups.

Each simple root string through a spin weight has length at most two, so every numbered root generator squares to zero on the spin module. The Chevalley rank-one identity

x_α(u) x_{-α}(-u⁻¹) x_α(u) = h_α(u) n_α,      n_α = x_α(1) x_{-α}(-1) x_α(1),

then exhibits each coroot value at an arbitrary unit as a product of root subgroup elements. No coprimality condition on the coordinates of the root is needed, and none is available at rank two: the long simple root of B₂ has Cartan row (2, -2), so its values on the weight torus are the squares of units rather than all units.

Applying the pointwise containment to the universal point of the torus, over the coordinate ring of the split torus itself, shows that the torus is also redundant scheme-theoretically: the toral-closure defining ideal over ℤ equals the ideal cut out by the numbered root subgroups alone, so the carrier is the root-generated Kostant group scheme. This is an equality of integral carriers and of their transports; it does not say that the subgroup generated anew over a non-flat base is the base change of the integral carrier.

Main results

• TauCeti.TypeBSpinCarrier.coordinateCocharacter_mem_elementarySubgroup: every coroot value of the carrier, at every unit of every value ring, lies in the group generated by the numbered root subgroups.
• TauCeti.TypeBSpinCarrier.weightTorusSubgroup_le_elementarySubgroup: the weight torus lies in the elementary subgroup over every commutative ring.
• TauCeti.TypeBSpinCarrier.weightTorusSubsystemSubgroup_univ_eq_elementarySubgroup: adjoining the weight torus to all numbered root subgroups gives exactly the elementary subgroup.
• TauCeti.TypeBSpinCarrier.definingIdeal_eq_kostantGeneratedDefiningIdeal: the integral toral-closure carrier is already cut out by the root subgroups alone.
• TauCeti.TypeBSpinCarrier.groupScheme_eq_kostantGeneratedGroupScheme and TauCeti.TypeBSpinCarrier.isIso_kostantGeneratedToToral: the carrier is the root-generated Kostant group scheme, and the canonical comparison between them is an isomorphism.
• TauCeti.TypeBSpinCarrier.baseChangeDefiningIdeal_eq_kostantGeneratedGeneralLinearBaseChangeIdeal states the same equality of ideals after base change to any commutative ring.
• TauCeti.TypeBSpinCarrier.groupScheme_hom_ext_of_rootSubgroup: a morphism out of the carrier is determined by its restrictions to the numbered root subgroups alone.

References

• R. Steinberg, Lectures on Chevalley Groups, Section 3.
• R. W. Carter, Simple Groups of Lie Type, Sections 6.4 and 7.1.
• TauCeti.Algebra.Lie.Symplectic.StandardCarrier.ToralGeneration, which runs the same square-zero argument on the standard type-C carrier.
• TauCeti.Algebra.Lie.Orthogonal.TypeD.SpinCarrier.Generation, the corresponding statement for the type-D spin carrier.
• TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.GeckLattice.SchemeGeneration, which the scheme-theoretic section of this file follows.

Generation of the weight torus

theorem TauCeti.TypeBSpinCarrier.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 typeBSimpleRootGeneratorFamily typeBSimpleCorootGenerator (rep n) (lattice n).toAddSubgroup ⋯ ⋯ A

Every coroot value of the full-weight type-Bₙ₊₁ spin carrier lies in the group generated by the numbered root subgroups, at every unit of every value ring.

theorem TauCeti.TypeBSpinCarrier.weightTorusSubgroup_le_elementarySubgroup (n : ℕ) (A : CommAlgCat ℤ) : UniversalEnvelopingAlgebra.kostantTorusSubgroup (lattice n).toAddSubgroup (latticeBasis n) (basisWeight n) ↑A ≤ UniversalEnvelopingAlgebra.kostantElementarySubgroup typeBSimpleRootGeneratorFamily typeBSimpleCorootGenerator (rep n) (lattice n).toAddSubgroup ⋯ ⋯ A

Over every commutative ring the type-B full-spin weight torus on the base-changed admissible lattice is contained in the elementary group generated by the positive and negative numbered simple root subgroups.

theorem TauCeti.TypeBSpinCarrier.weightTorusSubsystemSubgroup_univ_eq_elementarySubgroup (n : ℕ) (A : CommAlgCat ℤ) : UniversalEnvelopingAlgebra.kostantTorusSubsystemSubgroup typeBSimpleRootGeneratorFamily typeBSimpleCorootGenerator (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) (basisWeight n) Set.univ A = UniversalEnvelopingAlgebra.kostantElementarySubgroup typeBSimpleRootGeneratorFamily typeBSimpleCorootGenerator (rep n) (lattice n).toAddSubgroup ⋯ ⋯ A

Over every commutative ring, adjoining the type-B full-spin weight torus to all positive and negative numbered simple root subgroups does not enlarge their elementary subgroup.

Scheme-theoretic generation

theorem TauCeti.TypeBSpinCarrier.definingIdeal_eq_kostantGeneratedDefiningIdeal (n : ℕ) : definingIdeal n = UniversalEnvelopingAlgebra.kostantGeneratedDefiningIdeal typeBSimpleRootGeneratorFamily typeBSimpleCorootGenerator (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n)

The full-weight type-Bₙ₊₁ spin 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.TypeBSpinCarrier.groupScheme_eq_kostantGeneratedGroupScheme (n : ℕ) : groupScheme n = UniversalEnvelopingAlgebra.kostantGeneratedGroupScheme typeBSimpleRootGeneratorFamily typeBSimpleCorootGenerator (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n)

The full-weight type-Bₙ₊₁ spin carrier is the group scheme generated by its numbered positive and negative simple root subgroups.

instance TauCeti.TypeBSpinCarrier.isIso_kostantGeneratedToToral (n : ℕ) : CategoryTheory.IsIso (UniversalEnvelopingAlgebra.kostantGeneratedToToral typeBSimpleRootGeneratorFamily typeBSimpleCorootGenerator (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) (basisWeight n))

The canonical inclusion of the root-generated type-Bₙ₊₁ spin carrier into its toral closure is an isomorphism.

theorem TauCeti.TypeBSpinCarrier.baseChangeDefiningIdeal_eq_kostantGeneratedGeneralLinearBaseChangeIdeal (n : ℕ) (A : Type v) [CommRing A] : baseChangeDefiningIdeal n A = UniversalEnvelopingAlgebra.kostantGeneratedGeneralLinearBaseChangeIdeal typeBSimpleRootGeneratorFamily typeBSimpleCorootGenerator (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) A

After base change to any commutative ring, the transported type-Bₙ₊₁ carrier ideal is the transport of the root-generated integral ideal. This does not identify it with the common kernel of the root-subgroup maps formed anew over that ring.

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

Two morphisms out of the type-Bₙ₊₁ spin carrier agree as soon as they agree on its numbered root subgroups. This drops the weight-torus hypothesis of TauCeti.TypeBSpinCarrier.groupScheme_hom_ext, which root generation of the carrier makes redundant.