Base change of general-linear root subgroups

The coordinate-algebra base-change isomorphisms of GLₙ and 𝔾ₐ carry the scalar extension of the elementary root map to the elementary root map over the new ring. In particular, they preserve its additive parameter, with no invertibility, flatness, or reducedness assumption on the base extension. This compatibility is needed to transport normalized root subgroups between integral and field-valued constructions.

The calculation uses rootSubgroupCoordinateMap_apply_X and the existing coordinate base-change isomorphisms, rather than reconstructing either morphism from points.

References

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

theorem TauCeti.GeneralLinear.baseChangeMap_rootSubgroupCoordinateMap_comp_baseChangeIso_hom (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] {n : ℕ} {i j : Fin n} (hij : i ≠ j) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap (rootSubgroupCoordinateMap hij)) (AdditiveGroup.coordinateHopfAlgebraBaseChangeIso R K).hom = CategoryTheory.CategoryStruct.comp (coordinateHopfAlgebraBaseChangeIso R K n).hom (rootSubgroupCoordinateMap hij)

The normalized general-linear root map commutes with scalar extension, under the canonical coordinate-algebra identifications of GLₙ and 𝔾ₐ.

theorem TauCeti.GeneralLinear.baseChangeMap_rootSubgroupCoordinateMap_comp_baseChangeIso_hom_assoc (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] {n : ℕ} {i j : Fin n} (hij : i ≠ j) {Z : CommHopfAlgCat K} (h : AdditiveGroup.coordinateHopfAlgebra K ⟶ Z) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap (rootSubgroupCoordinateMap hij)) (CategoryTheory.CategoryStruct.comp (AdditiveGroup.coordinateHopfAlgebraBaseChangeIso R K).hom h) = CategoryTheory.CategoryStruct.comp (coordinateHopfAlgebraBaseChangeIso R K n).hom (CategoryTheory.CategoryStruct.comp (rootSubgroupCoordinateMap hij) h)

The normalized general-linear root map commutes with scalar extension, under the canonical coordinate-algebra identifications of GLₙ and 𝔾ₐ.