Scalar extension of special-linear adjoint root vectors

Scalar extension of the cotangent-dual model of Lie(SLₙ) agrees with the same model constructed over the new base ring. The comparison sends each normalized matrix-unit root vector to the corresponding root vector over that ring, retaining its parameter. This identifies the actual generators used in integral pinnings.

The ambient comparison combines Derivation.tangentScalarExtensionEquiv, SpecialLinear.tangentCoefficientLieEquiv, and cotangent duality. The geometric compatibility of the middle comparison is proved in SpecialLinear.Tangent.BaseChange.

References

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

@[simp]

theorem TauCeti.SpecialLinear.cotangentDualBaseChangeEquiv_tmul_rootVector (R : Type u) (K : Type v) [CommRing R] [CommRing K] [Algebra R K] (r : ℕ) (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) (c : K) : (cotangentDualBaseChangeEquiv R K (r + 1)) (c ⊗ₜ[R] rootVector p) = c • rootVector p

Scalar extension preserves every normalized root vector and its scalar parameter.