Closed additive root subgroups of the special linear group

The elementary root map xᵢⱼ : 𝔾ₐ → SLₙ is a closed immersion over every commutative ring. Its composite with SLₙ → GLₙ is the general-linear root map, so the surjectivity of that coordinate morphism gives surjectivity of the special-linear coordinate morphism as well.

Thus rootSubgroupClosedSubgroup is a closed subgroup scheme isomorphic to 𝔾ₐ through its specified root map, as required to use the elementary root maps in a pinning. The isomorphism rootSubgroupClosedSubgroupIso records this parametrization, and its inverse followed by the inclusion recovers the original root map.

References

• J. S. Milne, Algebraic Groups (2017), §21.
• R. W. Carter, Simple Groups of Lie Type (1972), §11.3.

instance TauCeti.SpecialLinear.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 elementary root map identifies 𝔾ₐ with a closed subscheme of SLₙ.

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

The closed additive root subgroup of SLₙ attached to εᵢ - εⱼ, with its elementary parametrization.

Equations

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

@[simp]

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

The special-linear root map represents its named closed root subgroup.

noncomputable def TauCeti.SpecialLinear.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 special-linear root subgroup is canonically isomorphic to 𝔾ₐ.

Equations

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

@[simp]

theorem TauCeti.SpecialLinear.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 parametrization followed by the closed subgroup inclusion is the special-linear root map.