The standard pinning of the special linear group

For SL_{r+1}, the determinant-one diagonal torus and upper-triangular Borel determine the consecutive simple roots ε_i - ε_(i+1). The normalized matrix units E_(i,i+1) trivialize their integral adjoint root spaces and give the standard pinning. This works over every nontrivial commutative ring with connected spectrum, in particular over ℤ, with no restriction on characteristic or reducedness. The weight characterizations below do not require connectedness of the base.

The positive-root and simple-root characterizations identify the intrinsic definitions with the base of SpecialLinear.diagonalRootDatum. The construction uses SpecialLinear.rootSpaceEquiv, SpecialLinear.splitMaximalTorus, and the existing upper-triangular tangent calculation. Indecomposability of the base is supplied by TauCeti.mem_support_iff_isPos_and_forall_ne_add.

References

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

@[simp]

theorem TauCeti.SpecialLinear.isPositiveRoot_diagonalRoot_iff {R : Type u} [CommRing R] [Nontrivial R] {r : ℕ} (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) : (splitMaximalTorus R r).IsPositiveRoot (UpperTriangular.definingHopfIdeal R (r + 1)) ((diagonalRootDatum r).root p) ↔ (diagonalRootBase r).IsPos p

The intrinsic positive roots for the standard special-linear torus and Borel are exactly the positive roots of its diagonal root datum.

theorem TauCeti.SpecialLinear.isPositiveRoot_iff_exists_diagonalRoot {R : Type u} [CommRing R] [Nontrivial R] {r : ℕ} (α : ULift.{u, 0} (Fin r) →₀ ℤ) : (splitMaximalTorus R r).IsPositiveRoot (UpperTriangular.definingHopfIdeal R (r + 1)) α ↔ ∃ (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))), α = (diagonalRootDatum r).root p ∧ (diagonalRootBase r).IsPos p

Every intrinsic positive root is a positive root of the diagonal root datum.

@[simp]

theorem TauCeti.SpecialLinear.isSimpleRoot_diagonalRoot_iff {R : Type u} [CommRing R] [Nontrivial R] {r : ℕ} (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) : (splitMaximalTorus R r).IsSimpleRoot (UpperTriangular.definingHopfIdeal R (r + 1)) ((diagonalRootDatum r).root p) ↔ p ∈ (diagonalRootBase r).support

The intrinsic simple roots are precisely the members of the consecutive-root base.

theorem TauCeti.SpecialLinear.isSimpleRoot_iff_exists_diagonalSimpleRoot {R : Type u} [CommRing R] [Nontrivial R] {r : ℕ} (α : ULift.{u, 0} (Fin r) →₀ ℤ) : (splitMaximalTorus R r).IsSimpleRoot (UpperTriangular.definingHopfIdeal R (r + 1)) α ↔ ∃ (i : Fin r), α = (diagonalRootDatum r).root (diagonalSimpleRootIndex r i)

The consecutive simple roots exhaust the actual simple adjoint weights selected by the upper-triangular Borel.

noncomputable def TauCeti.SpecialLinear.diagonalSimpleRootEquiv {R : Type u} [CommRing R] [Nontrivial R] {r : ℕ} : Fin r ≃ { α : ULift.{u, 0} (Fin r) →₀ ℤ // (splitMaximalTorus R r).IsSimpleRoot (UpperTriangular.definingHopfIdeal R (r + 1)) α }

Bourbaki numbering as an equivalence onto the intrinsic simple roots of the standard special-linear torus and Borel.

Equations

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

@[simp]

theorem TauCeti.SpecialLinear.diagonalSimpleRootEquiv_apply {R : Type u} [CommRing R] [Nontrivial R] {r : ℕ} (i : Fin r) : ↑(diagonalSimpleRootEquiv i) = (diagonalRootDatum r).root (diagonalSimpleRootIndex r i)

The intrinsic simple root at number i is the consecutive coordinate difference.

noncomputable def TauCeti.SpecialLinear.standardPinning (R : Type u) [CommRing R] [Nontrivial R] [ConnectedSpace (PrimeSpectrum R)] (r : ℕ) : Pinning R (coordinateHopfAlgebra R (r + 1)) r

The standard integral pinning of SL_{r+1}: diagonal torus, upper-triangular Borel, and normalized consecutive matrix-unit root vectors.

Equations

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

@[simp]

theorem TauCeti.SpecialLinear.standardPinning_torus {R : Type u} [CommRing R] [Nontrivial R] {r : ℕ} [ConnectedSpace (PrimeSpectrum R)] : (standardPinning R r).torus = splitMaximalTorus R r

@[simp]

theorem TauCeti.SpecialLinear.standardPinning_borel {R : Type u} [CommRing R] [Nontrivial R] {r : ℕ} [ConnectedSpace (PrimeSpectrum R)] : (standardPinning R r).borel = UpperTriangular.definingHopfIdeal R (r + 1)

noncomputable def TauCeti.SpecialLinear.standardPinningSimpleRootEquiv {R : Type u} [CommRing R] [Nontrivial R] {r : ℕ} [ConnectedSpace (PrimeSpectrum R)] : Fin r ≃ { α : ULift.{u, 0} (Fin r) →₀ ℤ // (standardPinning R r).torus.IsSimpleRoot (standardPinning R r).borel α }

Bourbaki numbering of the simple roots in the dependent type of the standard pinning.

Equations

• TauCeti.SpecialLinear.standardPinningSimpleRootEquiv = TauCeti.SpecialLinear.diagonalSimpleRootEquiv

@[simp]

theorem TauCeti.SpecialLinear.standardPinningSimpleRootEquiv_apply {R : Type u} [CommRing R] [Nontrivial R] {r : ℕ} [ConnectedSpace (PrimeSpectrum R)] (i : Fin r) : ↑(standardPinningSimpleRootEquiv i) = (diagonalRootDatum r).root (diagonalSimpleRootIndex r i)

The pinning's numbered simple root has the consecutive-difference character.

@[simp]

theorem TauCeti.SpecialLinear.standardPinning_rootSpaceEquiv_apply_coe {R : Type u} [CommRing R] [Nontrivial R] {r : ℕ} [ConnectedSpace (PrimeSpectrum R)] (i : Fin r) (c : R) : ↑(((standardPinning R r).rootSpaceEquiv (standardPinningSimpleRootEquiv i)) c) = c • rootVector (diagonalSimpleRootIndex r i)

The chosen simple-root trivialization uses the normalized consecutive matrix unit. This computation identifies the pinning's generators with the root-subgroup differentials.

@[simp]

theorem TauCeti.SpecialLinear.standardPinning_rootVector {R : Type u} [CommRing R] [Nontrivial R] {r : ℕ} [ConnectedSpace (PrimeSpectrum R)] (i : Fin r) : (standardPinning R r).rootVector (standardPinningSimpleRootEquiv i) = rootVector (diagonalSimpleRootIndex r i)

The standard pinning chooses the normalized consecutive matrix-unit root vectors.