Pinnings with a chosen split maximal torus over a connected base

A pinning consists of a split maximal torus, a Borel containing it, and a generator of its Lie algebra's root space for each simple root. The positive roots are the nontrivial adjoint weights whose entire root space lies in the Lie algebra of the Borel. The simple roots are the positive roots which cannot be written as the sum of two positive roots. Thus the indexing of the generators is determined by the group, torus, and Borel; it is not an independently supplied root system. The base spectrum is required to be connected: on a disconnected base different components can select opposite positive systems, so global characters alone need not index all fiberwise simple roots.

Pinning records generators as linear equivalences from the base ring onto the simple root spaces. This expresses generation and freeness, rather than merely choosing nonzero vectors, which would be insufficient over a ring. Smoothness and finite type remain explicit hypotheses; reductivity over the base is certified by the data.

References

• B. Conrad, Reductive Group Schemes (2014), §5.1.
• J. S. Milne, Algebraic Groups (2017), §21.1 (positive and simple roots).

def TauCeti.SplitMaximalTorus.IsPositiveRoot {R : Type u} [CommRing R] {H : CommHopfAlgCat R} [Algebra.FiniteType R ↑H] {r : ℕ} [Module.Projective R (Bialgebra.CotangentSpace R ↑H)] (T : SplitMaximalTorus R H r) (B : HopfIdeal R ↑H) (α : ULift.{u, 0} (Fin r) →₀ ℤ) : Prop

A positive root relative to a closed subgroup is a nontrivial adjoint weight whose root space lies in the subgroup's tangent Lie algebra. For a Borel containing the torus in a reductive group over a connected base, this is its positive root system. Characters are written additively in the exponent lattice of the torus.

Equations

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

theorem TauCeti.SplitMaximalTorus.isPositiveRoot_iff {R : Type u} [CommRing R] {H : CommHopfAlgCat R} [Algebra.FiniteType R ↑H] {r : ℕ} [Module.Projective R (Bialgebra.CotangentSpace R ↑H)] (T : SplitMaximalTorus R H r) (B : HopfIdeal R ↑H) (α : ULift.{u, 0} (Fin r) →₀ ℤ) : T.IsPositiveRoot B α ↔ Multiplicative.ofAdd α ∈ Derivation.nontrivialAdjointWeights (CommHopfAlgCat.Hom.hom T.coordinateMap) ∧ ∀ x ∈ Derivation.adjointWeightSpace (CommHopfAlgCat.Hom.hom T.coordinateMap) (Multiplicative.ofAdd α), Derivation.cotangentLinearEquiv x ∈ B.lieSubalgebra

The adjoint-weight and tangent-containment characterization of positivity.

def TauCeti.SplitMaximalTorus.IsSimpleRoot {R : Type u} [CommRing R] {H : CommHopfAlgCat R} [Algebra.FiniteType R ↑H] {r : ℕ} [Module.Projective R (Bialgebra.CotangentSpace R ↑H)] (T : SplitMaximalTorus R H r) (B : HopfIdeal R ↑H) (α : ULift.{u, 0} (Fin r) →₀ ℤ) : Prop

A simple root is a positive root which is not the sum of two positive roots.

Equations

• T.IsSimpleRoot B α = (T.IsPositiveRoot B α ∧ ∀ (β γ : ULift.{?u.1, 0} (Fin r) →₀ ℤ), T.IsPositiveRoot B β → T.IsPositiveRoot B γ → α ≠ β + γ)

theorem TauCeti.SplitMaximalTorus.isSimpleRoot_iff {R : Type u} [CommRing R] {H : CommHopfAlgCat R} [Algebra.FiniteType R ↑H] {r : ℕ} [Module.Projective R (Bialgebra.CotangentSpace R ↑H)] (T : SplitMaximalTorus R H r) (B : HopfIdeal R ↑H) (α : ULift.{u, 0} (Fin r) →₀ ℤ) : T.IsSimpleRoot B α ↔ T.IsPositiveRoot B α ∧ ∀ (β γ : ULift.{u, 0} (Fin r) →₀ ℤ), T.IsPositiveRoot B β → T.IsPositiveRoot B γ → α ≠ β + γ

The indecomposable-positive-root characterization of simplicity.

structure TauCeti.Pinning (R : Type u) [CommRing R] (H : CommHopfAlgCat R) [Algebra.FiniteType R ↑H] [Algebra.Smooth R ↑H] [ConnectedSpace (PrimeSpectrum R)] (r : ℕ) : Type u

A pinning over a connected base of a smooth finite-type reductive affine group with a split maximal torus: a Borel containing the torus and trivializations of all simple root spaces. Only the intrinsically determined simple roots index the trivializations.

• reductive : reductiveCommHopfAlgPropertyOver R (FiniteTypeCommHopfAlgCat.of R ↑H)

  Reductivity over the base, including all geometric fibers.

• torus : SplitMaximalTorus R H r

  The chosen parametrized split maximal torus.

• borel : HopfIdeal R ↑H

  The ideal cutting out the chosen Borel subgroup.

• isBorel : HopfIdeal.IsBorelOver R H self.borel

  The subgroup is a Borel over the base.

• borel_le_torus : self.borel ≤ self.torus.definingIdeal

  The torus lies in the Borel; inclusions of defining ideals reverse subgroup inclusions.

• rootSpaceEquiv (α : { α : ULift.{u, 0} (Fin r) →₀ ℤ // self.torus.IsSimpleRoot self.borel α }) : R ≃ₗ[R] ↥(Derivation.adjointWeightSpace (CommHopfAlgCat.Hom.hom self.torus.coordinateMap) (Multiplicative.ofAdd ↑α))

  A generator, including its rank-one freeness certificate, for every simple root space.

theorem TauCeti.Pinning.ext_iff {R : Type u} {inst✝ : CommRing R} {H : CommHopfAlgCat R} {inst✝¹ : Algebra.FiniteType R ↑H} {inst✝² : Algebra.Smooth R ↑H} {inst✝³ : ConnectedSpace (PrimeSpectrum R)} {r : ℕ} {x y : Pinning R H r} : x = y ↔ x.torus = y.torus ∧ x.borel = y.borel ∧ x.rootSpaceEquiv ≍ y.rootSpaceEquiv

theorem TauCeti.Pinning.ext {R : Type u} {inst✝ : CommRing R} {H : CommHopfAlgCat R} {inst✝¹ : Algebra.FiniteType R ↑H} {inst✝² : Algebra.Smooth R ↑H} {inst✝³ : ConnectedSpace (PrimeSpectrum R)} {r : ℕ} {x y : Pinning R H r} (torus : x.torus = y.torus) (borel : x.borel = y.borel) (rootSpaceEquiv : x.rootSpaceEquiv ≍ y.rootSpaceEquiv) : x = y

noncomputable def TauCeti.Pinning.rootVector {R : Type u} [CommRing R] {H : CommHopfAlgCat R} [Algebra.FiniteType R ↑H] {r : ℕ} [Algebra.Smooth R ↑H] [ConnectedSpace (PrimeSpectrum R)] (P : Pinning R H r) (α : { α : ULift.{u, 0} (Fin r) →₀ ℤ // P.torus.IsSimpleRoot P.borel α }) : Module.Dual R (Bialgebra.CotangentSpace R ↑H)

The chosen root vector is the image of 1 in the trivialized simple root space.

Equations

• P.rootVector α = ↑((P.rootSpaceEquiv α) 1)

@[simp]

theorem TauCeti.Pinning.rootVector_def {R : Type u} [CommRing R] {H : CommHopfAlgCat R} [Algebra.FiniteType R ↑H] {r : ℕ} [Algebra.Smooth R ↑H] [ConnectedSpace (PrimeSpectrum R)] (P : Pinning R H r) (α : { α : ULift.{u, 0} (Fin r) →₀ ℤ // P.torus.IsSimpleRoot P.borel α }) : P.rootVector α = ↑((P.rootSpaceEquiv α) 1)

A pinning's root vector is the image of the unit under its root-space equivalence.

@[simp]

theorem TauCeti.Pinning.rootVector_mem {R : Type u} [CommRing R] {H : CommHopfAlgCat R} [Algebra.FiniteType R ↑H] {r : ℕ} [Algebra.Smooth R ↑H] [ConnectedSpace (PrimeSpectrum R)] (P : Pinning R H r) (α : { α : ULift.{u, 0} (Fin r) →₀ ℤ // P.torus.IsSimpleRoot P.borel α }) : P.rootVector α ∈ Derivation.adjointWeightSpace (CommHopfAlgCat.Hom.hom P.torus.coordinateMap) (Multiplicative.ofAdd ↑α)

A chosen root vector belongs to the weight space of its simple root.