Matrix root subgroups are closed additive groups

Over any commutative base ring, the root map xᵢⱼ : 𝔾ₐ → GLₙ identifies the additive group with a closed subgroup scheme. Its coordinate morphism is surjective: the (i, j) entry of the generic matrix maps to the additive parameter. This is a scheme-theoretic statement, including over nonreduced rings, rather than just injectivity on rational points.

The closed subgroup rootSubgroupClosedSubgroup retains the explicit parametrization by rootSubgroup; rootSubgroupClosedSubgroupIso identifies it with 𝔾ₐ. These closed additive subgroups are the root subgroups used in pinnings of the general and special linear groups.

References

• J. S. Milne, Algebraic Groups (2017), §21.
• R. W. Carter, Simple Groups of Lie Type (1972), §11.3.
• TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Scheme.ClosedImmersion: the closed-subgroup construction for Kostant root subgroups.

instance TauCeti.GeneralLinear.isClosedImmersion_rootSubgroup {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} (hij : i ≠ j) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (rootSubgroup hij).hom.hom)

Every matrix root map identifies 𝔾ₐ with a closed subscheme of GLₙ.

noncomputable def TauCeti.GeneralLinear.rootSubgroupClosedSubgroup {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} (hij : i ≠ j) : ClosedSubgroupScheme (groupScheme R N)

The closed additive root subgroup of GLₙ attached to εᵢ - εⱼ, parametrized by rootSubgroup hij.

Equations

• TauCeti.GeneralLinear.rootSubgroupClosedSubgroup hij = TauCeti.ClosedSubgroupScheme.mk (TauCeti.GeneralLinear.rootSubgroup hij)

@[simp]

theorem TauCeti.GeneralLinear.coe_rootSubgroupClosedSubgroup {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} (hij : i ≠ j) : ↑(rootSubgroupClosedSubgroup hij) = CategoryTheory.Subobject.mk (rootSubgroup hij)

The root map represents its named closed root subgroup.

noncomputable def TauCeti.GeneralLinear.rootSubgroupClosedSubgroupIso {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} (hij : i ≠ j) : CategoryTheory.Subobject.underlying.obj ↑(rootSubgroupClosedSubgroup hij) ≅ AdditiveGroup.groupScheme R

The closed matrix root subgroup is canonically isomorphic to the additive group scheme.

Equations

• TauCeti.GeneralLinear.rootSubgroupClosedSubgroupIso hij = TauCeti.ClosedSubgroupScheme.mkIso (TauCeti.GeneralLinear.rootSubgroup hij)

@[simp]

theorem TauCeti.GeneralLinear.rootSubgroupClosedSubgroupIso_inv_comp_arrow {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} (hij : i ≠ j) : CategoryTheory.CategoryStruct.comp (rootSubgroupClosedSubgroupIso hij).inv (↑(rootSubgroupClosedSubgroup hij)).arrow = rootSubgroup hij

The additive parametrization followed by the closed subgroup inclusion is the root map.