Integral adjoint comodule root spaces of the special linear group

For the diagonal torus of SL_{r+1} over a commutative ring, the adjoint comodule's weight space at the root ε_i - ε_j is the line generated by the normalized matrix unit E_ij. The Lie algebra is modeled as the dual of the augmentation cotangent module. Smoothness makes that module finite projective, so the existing universal-point tangent calculation detects membership in the actual comodule weight space over every base ring. mem_adjointWeightSpace_iff gives the entrywise criterion for an arbitrary character, which can also be used to exclude characters not appearing among the matrix entries.

adjointWeightSpace_root_eq_span supplies the root lines and their generators needed for pinnings over ℤ. Over a nontrivial ring these generators are nonzero. No reducedness, field, or characteristic assumption is imposed.

References

• J. S. Milne, Algebraic Groups (2017), §21.1 and Example 21.2.
• B. Conrad, Reductive Group Schemes, §5.1 (root spaces and pinnings).
• The universal-point calculation is TauCeti.SpecialLinear.adDerivation_universalDiagonalTorus_root_iff; the conversion to comodule weights uses Derivation.mem_adjointWeightSpace_iff_universalPointAction.

theorem TauCeti.SpecialLinear.mem_adjointWeightSpace_iff {R : Type u} [CommRing R] {r : ℕ} (α : Multiplicative (ULift.{u, 0} (Fin r) →₀ ℤ)) (x : Module.Dual R (Bialgebra.CotangentSpace R ↑(coordinateHopfAlgebra R (r + 1)))) : x ∈ Derivation.adjointWeightSpace (CommHopfAlgCat.Hom.hom (diagonalTorusCoordinateMap r R)) α ↔ ∀ (i j : Fin (r + 1)), SplitTorus.weightCharacter (diagonalTorusWeight r i - diagonalTorusWeight r j) ≠ α → ↑((tangentMatrix (r + 1)) (Derivation.cotangentLinearEquiv x)) i j = 0

A cotangent-dual tangent vector has weight α exactly when its matrix entries of every other weight vanish. This criterion uses the full torus coaction.

@[simp]

theorem TauCeti.SpecialLinear.mem_adjointWeightSpace_root_iff {R : Type u} [CommRing R] {r : ℕ} (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) (x : Module.Dual R (Bialgebra.CotangentSpace R ↑(coordinateHopfAlgebra R (r + 1)))) : x ∈ Derivation.adjointWeightSpace (CommHopfAlgCat.Hom.hom (diagonalTorusCoordinateMap r R)) (Multiplicative.ofAdd ((diagonalRootDatum r).root p)) ↔ (tangentMatrix (r + 1)) (Derivation.cotangentLinearEquiv x) ∈ R ∙ (LieAlgebra.SpecialLinear.single (↑p).1 (↑p).2 ⋯) 1

A cotangent-dual tangent vector lies in a root weight space of the adjoint comodule exactly when its trace-zero matrix lies in the corresponding matrix-unit line.

noncomputable def TauCeti.SpecialLinear.rootVector {R : Type u} [CommRing R] {r : ℕ} (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) : Module.Dual R (Bialgebra.CotangentSpace R ↑(coordinateHopfAlgebra R (r + 1)))

The normalized root vector of SL_{r+1} in the cotangent-dual model of its Lie algebra: the tangent vector whose trace-zero matrix is E_ij for the root ε_i - ε_j.

Equations

• TauCeti.SpecialLinear.rootVector p = Derivation.cotangentLinearEquiv.symm ((TauCeti.SpecialLinear.tangentLieEquivSl (r + 1)).symm ((LieAlgebra.SpecialLinear.single (↑p).1 (↑p).2 ⋯) 1))

@[simp]

theorem TauCeti.SpecialLinear.tangentMatrix_cotangentLinearEquiv_rootVector {R : Type u} [CommRing R] {r : ℕ} (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) : (tangentMatrix (r + 1)) (Derivation.cotangentLinearEquiv (rootVector p)) = (LieAlgebra.SpecialLinear.single (↑p).1 (↑p).2 ⋯) 1

The matrix of a normalized cotangent-dual root vector is its normalized matrix unit.

theorem TauCeti.SpecialLinear.adjointWeightSpace_root_eq_span {R : Type u} [CommRing R] {r : ℕ} (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) : Derivation.adjointWeightSpace (CommHopfAlgCat.Hom.hom (diagonalTorusCoordinateMap r R)) (Multiplicative.ofAdd ((diagonalRootDatum r).root p)) = R ∙ rootVector p

Each integral adjoint root space is generated by its normalized root vector.

theorem TauCeti.SpecialLinear.rootVector_smul_left_injective {R : Type u} [CommRing R] {r : ℕ} (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) : Function.Injective fun (c : R) => c • rootVector p

Multiplication by a normalized root vector is injective, including over rings with zero divisors. Its distinguished matrix entry recovers the scalar.

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

Each integral adjoint root space is a free rank-one module, with scalar 1 corresponding to its normalized root vector.

Equations

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

@[simp]

theorem TauCeti.SpecialLinear.rootSpaceEquiv_apply_coe {R : Type u} [CommRing R] {r : ℕ} (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) (c : R) : ↑((rootSpaceEquiv p) c) = c • rootVector p

The root-space parametrization sends a scalar to that multiple of the normalized root vector.

theorem TauCeti.SpecialLinear.rootSpaceEquiv_symm_apply_smul {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)))) : (rootSpaceEquiv p).symm x • rootVector p = ↑x

The coefficient from the inverse root-space parametrization reconstructs the vector.

@[simp]

theorem TauCeti.SpecialLinear.rootSpaceEquiv_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)))) : (rootSpaceEquiv p).symm x = ↑((tangentMatrix (r + 1)) (Derivation.cotangentLinearEquiv ↑x)) (↑p).1 (↑p).2

The inverse root-space parametrization is the distinguished matrix entry.

theorem TauCeti.SpecialLinear.rootVector_ne_zero {R : Type u} [CommRing R] {r : ℕ} [Nontrivial R] (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) : rootVector p ≠ 0

The normalized root vector is nonzero over every nontrivial commutative base ring.