Adjoint roots, root spaces, and root-subgroup differentials of SLₙ

The differential of the elementary root subgroup xᵢⱼ : 𝔾ₐ → SLₙ identifies Lie(𝔾ₐ) with the corresponding weight space of the integral adjoint comodule. The additive unit tangent vector maps to the normalized root vector Eᵢⱼ. This connects the root subgroup and root-vector normalizations used in a pinning.

The identification persists after extension to every commutative coefficient algebra: the differential's image is the scalar extension of the adjoint root line. The base ring and coefficient algebra may have nilpotents or zero divisors.

Over every nontrivial commutative base ring, the nontrivial adjoint weights of SL_{r+1} are exactly the roots of diagonalRootDatum. The root indices are canonically equivalent to the full nontrivial weight set, identifying the root lines to which a pinning assigns generators.

The calculation combines tangentMatrix_derivationComp_rootSubgroup with adjointWeightSpace_root_eq_span and the existing cotangent-duality and tangent scalar-extension equivalences.

References

• J. S. Milne, Algebraic Groups (2017), §21.1 and Example 21.2.
• B. Conrad, Reductive Group Schemes, §5.1 (root subgroups and pinnings).
• The root-index API follows TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Root.Adjoint.

@[simp]

theorem TauCeti.SpecialLinear.cotangentLinearEquiv_symm_derivationComp_rootSubgroup {R : Type u} [CommRing R] {r : ℕ} (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) (d : Derivation R (↑(AdditiveGroup.coordinateHopfAlgebra R)) (Bialgebra.CounitAlgebra R (↑(AdditiveGroup.coordinateHopfAlgebra R)) R)) : Derivation.cotangentLinearEquiv.symm ((derivationComp (CommHopfAlgCat.Hom.hom (rootSubgroupCoordinateMap ⋯))) d) = AdditiveGroup.gaTangentLinearEquiv d • rootVector p

The root-subgroup differential sends the additive tangent parameter to that multiple of the normalized adjoint root vector, in the cotangent-dual model.

noncomputable def TauCeti.SpecialLinear.rootDifferentialEquiv {R : Type u} [CommRing R] {r : ℕ} (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) : Derivation R (↑(AdditiveGroup.coordinateHopfAlgebra R)) (Bialgebra.CounitAlgebra R (↑(AdditiveGroup.coordinateHopfAlgebra R)) R) ≃ₗ[R] ↥(Derivation.adjointWeightSpace (CommHopfAlgCat.Hom.hom (diagonalTorusCoordinateMap r R)) (Multiplicative.ofAdd ((diagonalRootDatum r).root p)))

The differential of the root subgroup, as an isomorphism onto the adjoint root space over the base ring.

Equations

• TauCeti.SpecialLinear.rootDifferentialEquiv p = TauCeti.AdditiveGroup.gaTangentLinearEquiv.trans (TauCeti.SpecialLinear.rootSpaceEquiv p)

@[simp]

theorem TauCeti.SpecialLinear.rootDifferentialEquiv_apply_coe {R : Type u} [CommRing R] {r : ℕ} (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) (d : Derivation R (↑(AdditiveGroup.coordinateHopfAlgebra R)) (Bialgebra.CounitAlgebra R (↑(AdditiveGroup.coordinateHopfAlgebra R)) R)) : ↑((rootDifferentialEquiv p) d) = Derivation.cotangentLinearEquiv.symm ((derivationComp (CommHopfAlgCat.Hom.hom (rootSubgroupCoordinateMap ⋯))) d)

Forgetting the weight-space restriction recovers the actual root-subgroup differential, expressed by cotangent duality.

@[simp]

theorem TauCeti.SpecialLinear.rootDifferentialEquiv_symm_apply {R : Type u} [CommRing R] {r : ℕ} (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) (x : ↥(Derivation.adjointWeightSpace (CommHopfAlgCat.Hom.hom (diagonalTorusCoordinateMap r R)) (Multiplicative.ofAdd ((diagonalRootDatum r).root p)))) : (rootDifferentialEquiv p).symm x = AdditiveGroup.gaTangentLinearEquiv.symm ((rootSpaceEquiv p).symm x)

The inverse differential recovers the additive tangent parameter of a root vector from its root-space coordinate.

theorem TauCeti.SpecialLinear.tangentScalarExtensionEquiv_tmul_rootVector {R : Type u} [CommRing R] {r : ℕ} {B : Type v} [CommRing B] [Algebra R B] (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) (c : B) : Derivation.tangentScalarExtensionEquiv (c ⊗ₜ[R] rootVector p) = (derivationComp (CommHopfAlgCat.Hom.hom (rootSubgroupCoordinateMap ⋯))) (AdditiveGroup.gaTangentLinearEquiv.symm c)

After coefficient extension, the root vector with parameter c is the root-subgroup differential of the additive tangent vector with parameter c. For simplification, Derivation.tangentScalarExtensionEquiv_tmul is the general pure-tensor normal form; this identity is for explicit rewriting.

theorem TauCeti.SpecialLinear.range_derivationCompLieHom_rootSubgroup_eq_adjointWeightSpace_baseChange {R : Type u} [CommRing R] {r : ℕ} {B : Type v} [CommRing B] [Algebra R B] (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) : (derivationCompLieHom (CommHopfAlgCat.Hom.hom (rootSubgroupCoordinateMap ⋯))).range.toSubmodule = Submodule.map (↑Derivation.tangentScalarExtensionEquiv) (Submodule.baseChange B (Derivation.adjointWeightSpace (CommHopfAlgCat.Hom.hom (diagonalTorusCoordinateMap r R)) (Multiplicative.ofAdd ((diagonalRootDatum r).root p))))

Over every commutative coefficient algebra, the image of the root-subgroup differential is exactly the scalar extension of its integral adjoint root space.

@[simp]

theorem TauCeti.SpecialLinear.ofAdd_root_mem_nontrivialAdjointWeights {R : Type u} [CommRing R] {r : ℕ} [Nontrivial R] (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) : Multiplicative.ofAdd ((diagonalRootDatum r).root p) ∈ Derivation.nontrivialAdjointWeights (CommHopfAlgCat.Hom.hom (diagonalTorusCoordinateMap r R))

Every root of the diagonal root datum occurs as a nontrivial adjoint weight of SL_{r+1}.

theorem TauCeti.SpecialLinear.mem_nontrivialAdjointWeights_iff_exists_diagonalRoot {R : Type u} [CommRing R] {r : ℕ} [Nontrivial R] (α : Multiplicative (ULift.{u, 0} (Fin r) →₀ ℤ)) : α ∈ Derivation.nontrivialAdjointWeights (CommHopfAlgCat.Hom.hom (diagonalTorusCoordinateMap r R)) ↔ ∃ (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))), α = Multiplicative.ofAdd ((diagonalRootDatum r).root p)

The nontrivial adjoint weights of SL_{r+1} relative to its diagonal torus are exactly the roots of its diagonal root datum. No field or reducedness assumption is needed.

theorem TauCeti.SpecialLinear.range_ofAdd_diagonalRootDatum_root_eq_nontrivialAdjointWeights {R : Type u} [CommRing R] {r : ℕ} [Nontrivial R] : (Set.range fun (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) => Multiplicative.ofAdd ((diagonalRootDatum r).root p)) = Derivation.nontrivialAdjointWeights (CommHopfAlgCat.Hom.hom (diagonalTorusCoordinateMap r R))

The root set of the diagonal root datum is the entire nontrivial adjoint weight set of the special linear group.

noncomputable def TauCeti.SpecialLinear.diagonalRootIndexEquivNontrivialAdjointWeights {R : Type u} [CommRing R] {r : ℕ} [Nontrivial R] : SplitTorus.CoordinateRootIndex (Fin (r + 1)) ≃ { α : ↑(SplitTorus.characterGroup (ULift.{u, 0} (Fin r))) // α ∈ Derivation.nontrivialAdjointWeights (CommHopfAlgCat.Hom.hom (diagonalTorusCoordinateMap r R)) }

Ordered pairs of distinct matrix indices canonically index all nontrivial adjoint weights of SL_{r+1}.

Equations

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

@[simp]

theorem TauCeti.SpecialLinear.diagonalRootIndexEquivNontrivialAdjointWeights_apply {R : Type u} [CommRing R] {r : ℕ} [Nontrivial R] (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) : ↑(diagonalRootIndexEquivNontrivialAdjointWeights p) = Multiplicative.ofAdd ((diagonalRootDatum r).root p)

The root-index equivalence sends an index to its root character.