The diagonal torus of the general linear group scheme

The rank-N split torus has A-points Fin N → Aˣ, while the general linear group has A-points GL (Fin N) A. The diagonal embedding

(t₀, …, tₙ₋₁) ↦ diag(t₀, …, tₙ₋₁)

is natural in the commutative R-algebra A. This file uses full faithfulness of the functor of points to recover its coordinate Hopf-algebra morphism, then applies relative spectrum to obtain the group-scheme morphism TauCeti.GeneralLinear.diagonalTorus.

The diagonal torus acts on the root subgroup for εᵢ - εⱼ with that character. On algebra-valued points the pinning equation is

t xᵢⱼ(c) t⁻¹ = xᵢⱼ(tᵢ c tⱼ⁻¹).

Thus the split maximal torus and the root subgroups of the worked GLₙ construction are linked by the same equation required of a pinned Chevalley--Demazure group scheme.

Main declarations

• TauCeti.GeneralLinear.diagonalTorusPoints: the diagonal embedding on algebra-valued points.
• TauCeti.GeneralLinear.diagonalTorusCoordinateMap: its coordinate Hopf-algebra morphism.
• TauCeti.GeneralLinear.diagonalTorusCoordinateMap_X: its value on each generic matrix entry.
• TauCeti.GeneralLinear.diagonalTorusCoordinateMap_baseChange: compatibility with scalar extension and the canonical coordinate Hopf-algebra base-change isomorphisms.
• TauCeti.GeneralLinear.diagonalTorus: the corresponding group-scheme morphism.
• TauCeti.GeneralLinear.diagonalTorusPoints_mul_rootSubgroupPoints_mul_inv: the root-character conjugation equation.
• TauCeti.GeneralLinear.schemePointsMulEquiv_diagonalTorus: on scheme-valued points, composing with the diagonal torus morphism is the diagonal matrix of the coordinates.

References

• J. S. Milne, Algebraic Groups (2017), §21.
• J. E. Humphreys, Linear Algebraic Groups (1975), §26.3.
• The points-map, natural-transformation, coordinate-morphism, and relative-spectrum constructions are adapted from the formal template in TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Root.Subgroup.

This is the split-torus and root-subgroup pinning equation in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, a prerequisite for milestone L0 of the CFSGStatement roadmap.

def TauCeti.GeneralLinear.diagonalTorusCoordinates {N : ℕ} {A : Type w} [Monoid A] : (ULift.{u, 0} (Fin N) → Aˣ) →* Fin N → Aˣ

Restrict a same-universe coordinate family on ULift (Fin N) to the canonical copy of Fin N. The universe lift is required only by the current same-universe group-scheme API.

Equations

• TauCeti.GeneralLinear.diagonalTorusCoordinates = { toFun := fun (t : ULift.{?u.2, 0} (Fin N) → Aˣ) (i : Fin N) => t { down := i }, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.GeneralLinear.diagonalTorusCoordinates_apply {N : ℕ} {A : Type w} [Monoid A] (t : ULift.{u, 0} (Fin N) → Aˣ) (i : Fin N) : diagonalTorusCoordinates t i = t { down := i }

Restricting a universe-lifted coordinate family evaluates it at the canonical lift.

noncomputable def TauCeti.GeneralLinear.diagonalTorusPoints {R : Type u} [CommRing R] {N : ℕ} {A : Type w} [CommRing A] [Algebra R A] : WithConv (MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin N) →₀ ℤ)) →ₐ[R] A) →* WithConv (↑(coordinateHopfAlgebra R N) →ₐ[R] A)

The diagonal-torus homomorphism on A-points. Under the split-torus and general-linear points equivalences it is the diagonal embedding diagGL : (Fin N → Aˣ) →* GL (Fin N) A.

Equations

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

theorem TauCeti.GeneralLinear.pointsMulEquiv_diagonalTorusPoints {R : Type u} [CommRing R] {N : ℕ} {A : Type w} [CommRing A] [Algebra R A] (f : WithConv (MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin N) →₀ ℤ)) →ₐ[R] A)) : (pointsMulEquiv N) (diagonalTorusPoints f) = diagGL (diagonalTorusCoordinates (SplitTorus.pointsMulEquiv f))

Reading the image of a split-torus point as an invertible matrix gives the diagonal matrix whose diagonal entries are the coordinates of that point.

theorem TauCeti.GeneralLinear.diagonalTorusPoints_injective {R : Type u} [CommRing R] {N : ℕ} {A : Type w} [CommRing A] [Algebra R A] : Function.Injective ⇑diagonalTorusPoints

The diagonal-torus homomorphism on points is injective.

theorem TauCeti.GeneralLinear.mapValue_diagonalTorusPoints {R : Type u} [CommRing R] {N : ℕ} {A : Type w} [CommRing A] [Algebra R A] {B : Type w'} [CommRing B] [Algebra R B] (phi : A →ₐ[R] B) (f : WithConv (MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin N) →₀ ℤ)) →ₐ[R] A)) : (AlgHom.mapValue phi) (diagonalTorusPoints f) = diagonalTorusPoints ((AlgHom.mapValue phi) f)

The diagonal embedding is natural in the value algebra.

theorem TauCeti.GeneralLinear.diagonalTorusPoints_mul_rootSubgroupPoints_mul_inv {R : Type u} [CommRing R] {N : ℕ} {A : Type w} [CommRing A] [Algebra R A] {i j : Fin N} (hij : i ≠ j) (t : WithConv (MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin N) →₀ ℤ)) →ₐ[R] A)) (c : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra R) →ₐ[R] A)) : diagonalTorusPoints t * (rootSubgroupPoints hij) c * (diagonalTorusPoints t)⁻¹ = (rootSubgroupPoints hij) (AdditiveGroup.gaPointsMulEquiv.symm (Multiplicative.ofAdd (↑(SplitTorus.pointsMulEquiv t { down := i }) * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv c) * ↑(SplitTorus.pointsMulEquiv t { down := j })⁻¹)))

Conjugation by a diagonal-torus point acts on the root subgroup for εᵢ - εⱼ by the corresponding character t ↦ tᵢ tⱼ⁻¹.

noncomputable def TauCeti.GeneralLinear.diagonalTorusPointsMap {R : Type u} [CommRing R] {N : ℕ} : HopfAlgebra.pointsFunctor ⟶ HopfAlgebra.pointsFunctor

The natural transformation of group-valued functors whose component sends a coordinate family of units to the corresponding diagonal invertible matrix.

Equations

• TauCeti.GeneralLinear.diagonalTorusPointsMap = { app := fun (A : CommAlgCat R) => GrpCat.ofHom TauCeti.GeneralLinear.diagonalTorusPoints, naturality := ⋯ }

@[simp]

theorem TauCeti.GeneralLinear.diagonalTorusPointsMap_app {R : Type u} [CommRing R] {N : ℕ} (A : CommAlgCat R) : diagonalTorusPointsMap.app A = GrpCat.ofHom diagonalTorusPoints

The component of the natural diagonal-torus map at a value algebra is diagonalTorusPoints.

noncomputable def TauCeti.GeneralLinear.diagonalTorusCoordinateMap {R : Type u} [CommRing R] {N : ℕ} : coordinateHopfAlgebra R N ⟶ { X := MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin N) →₀ ℤ)), commRing := MonoidAlgebra.commRing, hopfAlgebra := MonoidAlgebra.instHopfAlgebra }

The coordinate morphism of the diagonal torus, recovered from its natural action on points. Its direction is opposite to the represented group-scheme morphism.

Equations

• TauCeti.GeneralLinear.diagonalTorusCoordinateMap = TauCeti.CommHopfAlgCat.homOfPointsMap TauCeti.GeneralLinear.diagonalTorusPointsMap

theorem TauCeti.GeneralLinear.mapPointsFunctor_diagonalTorusCoordinateMap {R : Type u} [CommRing R] {N : ℕ} : CommHopfAlgCat.mapPointsFunctor diagonalTorusCoordinateMap = diagonalTorusPointsMap

Precomposition by the diagonal-torus coordinate morphism is the previously constructed natural map on convolution points.

@[simp]

theorem TauCeti.GeneralLinear.mapPointsFunctor_diagonalTorusCoordinateMap_app {R : Type u} [CommRing R] {N : ℕ} (A : CommAlgCat R) (f : ↑(HopfAlgebra.points A)) : (CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor diagonalTorusCoordinateMap).app A)) f = diagonalTorusPoints f

On every value algebra, the map induced by the diagonal-torus coordinate morphism is diagonalTorusPoints.

@[simp]

theorem TauCeti.GeneralLinear.diagonalTorusCoordinateMap_X {R : Type u} [CommRing R] {N : ℕ} (i j : Fin N) : (CommHopfAlgCat.Hom.hom diagonalTorusCoordinateMap) ((coordinateHopfAlgebraAlgEquiv R N) ((coordinateRingMap R N) (MvPolynomial.X (i, j)))) = if i = j then MonoidAlgebra.single (Multiplicative.ofAdd (Finsupp.single { down := i } 1)) 1 else 0

The diagonal-torus coordinate morphism sends a generic matrix entry to the corresponding coordinate character on the diagonal, and to zero off the diagonal.

theorem TauCeti.GeneralLinear.diagonalTorusCoordinateMap_baseChange {N : ℕ} (R K : Type u) [CommRing R] [CommRing K] [Algebra R K] : CategoryTheory.CategoryStruct.comp (coordinateHopfAlgebraBaseChangeIso R K N).inv (CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap diagonalTorusCoordinateMap) (DiagonalizableGroup.baseChangeCoordinateHopfAlgebraIso R K (SplitTorus.characterGroup (ULift.{u, 0} (Fin N)))).hom) = diagonalTorusCoordinateMap

The diagonal-torus coordinate morphism commutes with base change. After identifying the base changes of the general-linear and split-torus coordinate Hopf algebras with their direct constructions over the new base, scalar extension of the diagonal embedding is the diagonal embedding over the new base.

noncomputable def TauCeti.GeneralLinear.diagonalTorus {R : Type u} [CommRing R] {N : ℕ} : SplitTorus.groupScheme R (ULift.{u, 0} (Fin N)) ⟶ groupScheme R N

The diagonal torus of GLₙ, as a morphism from the rank-N split torus group scheme.

Equations

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

theorem TauCeti.GeneralLinear.diagonalTorus_def {R : Type u} [CommRing R] {N : ℕ} : diagonalTorus = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec (CommRingCat.of R)).map diagonalTorusCoordinateMap.op) (CategoryTheory.eqToHom ⋯))

The diagonal torus is relative spectrum applied contravariantly to its coordinate morphism, transported across the named presentations of the split torus and general linear group.

@[simp]

theorem TauCeti.GeneralLinear.schemePointsMulEquiv_diagonalTorus {R : Type u} [CommRing R] {N : ℕ} (A : Type u) [CommRing A] [Algebra R A] (p : (AlgebraicGeometry.Spec (CommRingCat.of A)).asOver (AlgebraicGeometry.Spec (CommRingCat.of R)) ⟶ (SplitTorus.groupScheme R (ULift.{u, 0} (Fin N))).X) : (schemePointsMulEquiv N A) (CategoryTheory.CategoryStruct.comp p diagonalTorus.hom.hom) = diagGL (diagonalTorusCoordinates (SplitTorus.schemePointsMulEquiv p))

The diagonal torus on scheme-valued points: composing an A-point of the split torus with the diagonal torus morphism gives the diagonal invertible matrix whose diagonal entries are the coordinates of that point.