The root subgroups of the special linear group

For distinct indices i ≠ j, the elementary matrices

xᵢⱼ(c) = 1 + c Eᵢⱼ

have determinant one. This file promotes them to a morphism of affine group schemes

xᵢⱼ : 𝔾ₐ → SLₙ

over an arbitrary commutative base ring. The construction first forms the natural homomorphism on algebra-valued points using Mathlib's Matrix.SpecialLinearGroup.transvection. Full faithfulness of the functor of points then recovers the coordinate Hopf-algebra morphism O(SLₙ) → O(𝔾ₐ), and relative spectrum gives the group-scheme morphism.

The resulting morphism is not merely another presentation of the already constructed general-linear root subgroup. Its composite with the determinant-kernel inclusion is proved to be TauCeti.GeneralLinear.rootSubgroup. Thus the construction records scheme-theoretically that the type-A root subgroup lands in determinant one, over every base ring.

Main definitions

• TauCeti.SpecialLinear.rootSubgroupPoints: the homomorphism on algebra-valued points.
• TauCeti.SpecialLinear.rootSubgroupPointsMap: the natural transformation on Hopf-points functors.
• TauCeti.SpecialLinear.rootSubgroupCoordinateMap: the coordinate morphism O(SLₙ) → O(𝔾ₐ).
• TauCeti.SpecialLinear.rootSubgroup: the affine group-scheme morphism 𝔾ₐ → SLₙ.

Main results

• TauCeti.SpecialLinear.pointsMulEquiv_rootSubgroupPoints: under the special-linear point equivalence, the root subgroup point is the elementary transvection of its additive parameter.
• TauCeti.SpecialLinear.rootSubgroupPoints_injective: the root subgroup is injective on points.
• TauCeti.SpecialLinear.mapValue_rootSubgroupPoints: the root subgroup on points is natural in the value algebra.
• TauCeti.SpecialLinear.coordinateMap_comp_rootSubgroupCoordinateMap: the coordinate-level factorization of the general-linear root subgroup.
• TauCeti.SpecialLinear.schemePointsMulEquiv_rootSubgroup: the root subgroup is the elementary transvection on scheme-valued points.
• TauCeti.SpecialLinear.rootSubgroup_comp_groupSchemeι: the corresponding factorization of group schemes.

References

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

noncomputable def TauCeti.SpecialLinear.rootSubgroupPoints {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} {A : Type w} [CommRing A] [Algebra R A] (hij : i ≠ j) : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra R) →ₐ[R] A) →* WithConv (↑(coordinateHopfAlgebra R N) →ₐ[R] A)

The root subgroup homomorphism on A-points, sending the additive parameter to its determinant-one elementary matrix.

Equations

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

@[simp]

theorem TauCeti.SpecialLinear.pointsMulEquiv_rootSubgroupPoints {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} {A : Type w} [CommRing A] [Algebra R A] (hij : i ≠ j) (f : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra R) →ₐ[R] A)) : (pointsMulEquiv R N) ((rootSubgroupPoints hij) f) = Matrix.SpecialLinearGroup.transvection hij (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f))

Under the special-linear point equivalence, the root subgroup point is the elementary transvection of its additive parameter.

theorem TauCeti.SpecialLinear.rootSubgroupPoints_injective {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} {A : Type w} [CommRing A] [Algebra R A] (hij : i ≠ j) : Function.Injective ⇑(rootSubgroupPoints hij)

The special-linear root subgroup is a monomorphism on algebra-valued points.

theorem TauCeti.SpecialLinear.mapValue_rootSubgroupPoints {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} {A : Type w} [CommRing A] [Algebra R A] {B : Type w} [CommRing B] [Algebra R B] (φ : A →ₐ[R] B) (hij : i ≠ j) (f : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra R) →ₐ[R] A)) : (AlgHom.mapValue φ) ((rootSubgroupPoints hij) f) = (rootSubgroupPoints hij) ((AlgHom.mapValue φ) f)

The special-linear root subgroup on points is natural in the value algebra.

noncomputable def TauCeti.SpecialLinear.rootSubgroupPointsMap {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} (hij : i ≠ j) : HopfAlgebra.pointsFunctor ⟶ HopfAlgebra.pointsFunctor

The natural transformation on group-valued points whose components are the special-linear root subgroup homomorphisms.

Equations

• TauCeti.SpecialLinear.rootSubgroupPointsMap hij = { app := fun (A : CommAlgCat R) => GrpCat.ofHom (TauCeti.SpecialLinear.rootSubgroupPoints hij), naturality := ⋯ }

@[simp]

theorem TauCeti.SpecialLinear.rootSubgroupPointsMap_app {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} (hij : i ≠ j) (A : CommAlgCat R) : (rootSubgroupPointsMap hij).app A = GrpCat.ofHom (rootSubgroupPoints hij)

The component of the natural points map at a value algebra is the special-linear root subgroup homomorphism.

noncomputable def TauCeti.SpecialLinear.rootSubgroupCoordinateMap {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} (hij : i ≠ j) : coordinateHopfAlgebra R N ⟶ AdditiveGroup.coordinateHopfAlgebra R

The coordinate morphism of the special-linear root subgroup, recovered from its natural action on points.

Equations

• TauCeti.SpecialLinear.rootSubgroupCoordinateMap hij = TauCeti.CommHopfAlgCat.homOfPointsMap (TauCeti.SpecialLinear.rootSubgroupPointsMap hij)

theorem TauCeti.SpecialLinear.mapPointsFunctor_rootSubgroupCoordinateMap {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} (hij : i ≠ j) : CommHopfAlgCat.mapPointsFunctor (rootSubgroupCoordinateMap hij) = rootSubgroupPointsMap hij

Precomposition by the coordinate morphism is the constructed natural map on points.

@[simp]

theorem TauCeti.SpecialLinear.mapPointsFunctor_rootSubgroupCoordinateMap_app {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} (hij : i ≠ j) (A : CommAlgCat R) (f : ↑(HopfAlgebra.points A)) : (CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (rootSubgroupCoordinateMap hij)).app A)) f = (rootSubgroupPoints hij) f

On a same-universe algebra, the coordinate morphism induces the previously constructed special-linear root subgroup map.

@[simp]

theorem TauCeti.SpecialLinear.coordinateMap_comp_rootSubgroupCoordinateMap {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} (hij : i ≠ j) : CategoryTheory.CategoryStruct.comp (coordinateMap R N) (rootSubgroupCoordinateMap hij) = GeneralLinear.rootSubgroupCoordinateMap hij

The quotient coordinate map followed by the special-linear root coordinate map is the general-linear root coordinate map.

theorem TauCeti.SpecialLinear.rootSubgroupCoordinateMap_surjective {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} (hij : i ≠ j) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (rootSubgroupCoordinateMap hij))

The special-linear root-subgroup coordinate morphism is surjective over any commutative base ring.

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

The root subgroup of SLₙ attached to εᵢ - εⱼ, as a morphism of affine group schemes over the base ring.

Equations

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

theorem TauCeti.SpecialLinear.rootSubgroup_def {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} (hij : i ≠ j) : rootSubgroup hij = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧R).map (rootSubgroupCoordinateMap hij).op) (CategoryTheory.eqToHom ⋯))

The root subgroup is relative spectrum applied contravariantly to its coordinate Hopf-algebra morphism, transported across the named presentations of 𝔾ₐ and SLₙ.

@[simp]

theorem TauCeti.SpecialLinear.schemePointsMulEquiv_rootSubgroup {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} (A : Type u) [CommRing A] [Algebra R A] (hij : i ≠ j) (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (AdditiveGroup.groupScheme R).X) : (schemePointsMulEquiv N A) (CategoryTheory.CategoryStruct.comp p (rootSubgroup hij).hom.hom) = Matrix.SpecialLinearGroup.transvection hij (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) p))

The root subgroup on scheme-valued points: composing an A-point of 𝔾ₐ with the special-linear root subgroup gives the determinant-one transvection of its additive parameter.

@[simp]

theorem TauCeti.SpecialLinear.rootSubgroup_comp_groupSchemeι {R : Type u} [CommRing R] {N : ℕ} {i j : Fin N} (hij : i ≠ j) : CategoryTheory.CategoryStruct.comp (rootSubgroup hij) (groupSchemeι R N) = GeneralLinear.rootSubgroup hij

The special-linear root subgroup followed by the determinant-kernel inclusion is the general-linear root subgroup.