Base change of the standard special-linear pinning

The standard pinning of SL_{r+1} is compatible with scalar extension between nontrivial commutative rings with connected spectra. Bourbaki numbering identifies its simple roots over both rings. The equivalence below identifies the scalar-extended simple root spaces with the new simple root spaces and preserves their chosen generators. Its ambient equation uses the geometric cotangent-dual base-change comparison, so it certifies compatibility of the chosen trivializations, not just abstract rank-one freeness.

The other pinning data already commute with base change: SpecialLinear.splitMaximalTorus_baseChange_comapOfIso treats the parametrized torus, and SpecialLinear.UpperTriangular.map_baseChangeHopfIdeal_definingHopfIdeal treats its Borel. The computation rules standardPinning_torus and standardPinning_borel identify those data in the assembled pinning. Together these results identify the integral pinning after extension to any nontrivial ring with connected spectrum.

References

• B. Conrad, Reductive Group Schemes (2014), §5.1.
• J. S. Milne, Algebraic Groups (2017), §21, Example 21.2.
• The construction uses SpecialLinear.standardPinning and its normalized standardPinning_rootSpaceEquiv_apply_coe computation rule.

noncomputable def TauCeti.SpecialLinear.standardPinningRootSpaceBaseChangeEquiv (R : Type u) (K : Type v) [CommRing R] [CommRing K] [Algebra R K] [Nontrivial R] [Nontrivial K] [ConnectedSpace (PrimeSpectrum R)] [ConnectedSpace (PrimeSpectrum K)] (r : ℕ) (i : Fin r) : TensorProduct R K ↥(Derivation.adjointWeightSpace (CommHopfAlgCat.Hom.hom (standardPinning R r).torus.coordinateMap) (Multiplicative.ofAdd ↑(standardPinningSimpleRootEquiv i))) ≃ₗ[K] ↥(Derivation.adjointWeightSpace (CommHopfAlgCat.Hom.hom (standardPinning K r).torus.coordinateMap) (Multiplicative.ofAdd ↑(standardPinningSimpleRootEquiv i)))

Scalar extension of the simple root space numbered i, preserving the trivialization chosen by the standard pinning.

Equations

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

@[simp]

theorem TauCeti.SpecialLinear.standardPinningRootSpaceBaseChangeEquiv_tmul (R : Type u) (K : Type v) [CommRing R] [CommRing K] [Algebra R K] [Nontrivial R] [Nontrivial K] [ConnectedSpace (PrimeSpectrum R)] [ConnectedSpace (PrimeSpectrum K)] (r : ℕ) (i : Fin r) (c : K) (b : R) : (standardPinningRootSpaceBaseChangeEquiv R K r i) (c ⊗ₜ[R] ((standardPinning R r).rootSpaceEquiv (standardPinningSimpleRootEquiv i)) b) = ((standardPinning K r).rootSpaceEquiv (standardPinningSimpleRootEquiv i)) (c * (algebraMap R K) b)

The simple-root base-change equivalence preserves the chosen scalar coordinates.

@[simp]

theorem TauCeti.SpecialLinear.standardPinningRootSpaceBaseChangeEquiv_symm_apply (R : Type u) (K : Type v) [CommRing R] [CommRing K] [Algebra R K] [Nontrivial R] [Nontrivial K] [ConnectedSpace (PrimeSpectrum R)] [ConnectedSpace (PrimeSpectrum K)] (r : ℕ) (i : Fin r) (c : K) : (standardPinningRootSpaceBaseChangeEquiv R K r i).symm (((standardPinning K r).rootSpaceEquiv (standardPinningSimpleRootEquiv i)) c) = c ⊗ₜ[R] ((standardPinning R r).rootSpaceEquiv (standardPinningSimpleRootEquiv i)) 1

The inverse simple-root comparison expresses a chosen vector over K as its scalar coordinate times the chosen generator over R.

theorem TauCeti.SpecialLinear.standardPinningRootSpaceBaseChangeEquiv_tmul_coe (R : Type u) (K : Type v) [CommRing R] [CommRing K] [Algebra R K] [Nontrivial R] [Nontrivial K] [ConnectedSpace (PrimeSpectrum R)] [ConnectedSpace (PrimeSpectrum K)] (r : ℕ) (i : Fin r) (c : K) (x : ↥(Derivation.adjointWeightSpace (CommHopfAlgCat.Hom.hom (standardPinning R r).torus.coordinateMap) (Multiplicative.ofAdd ↑(standardPinningSimpleRootEquiv i)))) : ↑((standardPinningRootSpaceBaseChangeEquiv R K r i) (c ⊗ₜ[R] x)) = (cotangentDualBaseChangeEquiv R K (r + 1)) (c ⊗ₜ[R] ↑x)

Forgetting the root-space restrictions identifies the base-change equivalence with the geometric scalar extension of the ambient Lie algebra.

@[simp]

theorem TauCeti.SpecialLinear.standardPinningRootSpaceBaseChangeEquiv_apply_coe (R : Type u) (K : Type v) [CommRing R] [CommRing K] [Algebra R K] [Nontrivial R] [Nontrivial K] [ConnectedSpace (PrimeSpectrum R)] [ConnectedSpace (PrimeSpectrum K)] (r : ℕ) (i : Fin r) (x : TensorProduct R K ↥(Derivation.adjointWeightSpace (CommHopfAlgCat.Hom.hom (standardPinning R r).torus.coordinateMap) (Multiplicative.ofAdd ↑(standardPinningSimpleRootEquiv i)))) : ↑((standardPinningRootSpaceBaseChangeEquiv R K r i) x) = (cotangentDualBaseChangeEquiv R K (r + 1)) ((LinearMap.baseChange K (Derivation.adjointWeightSpace (CommHopfAlgCat.Hom.hom (standardPinning R r).torus.coordinateMap) (Multiplicative.ofAdd ↑(standardPinningSimpleRootEquiv i))).subtype) x)

The entire scalar-extended simple root space maps into the corresponding simple root space by the ambient geometric comparison.

@[simp]

theorem TauCeti.SpecialLinear.cotangentDualBaseChangeEquiv_tmul_standardPinning_rootVector (R : Type u) (K : Type v) [CommRing R] [CommRing K] [Algebra R K] [Nontrivial R] [Nontrivial K] [ConnectedSpace (PrimeSpectrum R)] [ConnectedSpace (PrimeSpectrum K)] (r : ℕ) (i : Fin r) (c : K) : (cotangentDualBaseChangeEquiv R K (r + 1)) (c ⊗ₜ[R] (standardPinning R r).rootVector (standardPinningSimpleRootEquiv i)) = c • (standardPinning K r).rootVector (standardPinningSimpleRootEquiv i)

Scalar extension preserves the normalized simple-root generators of the standard pinning. The rule runs before simplification of the dependent cotangent presentations.