The diagonal torus in the upper-triangular group

The standard diagonal torus of GLₙ factors through its upper-triangular subgroup scheme. In Hopf coordinates, the diagonal-torus morphism kills every generic matrix coordinate strictly below the diagonal, so it descends uniquely through the quotient defining the upper-triangular group. Applying relative spectrum gives the inclusion T → B, whose composite with B → GLₙ is the standard diagonal torus.

This supplies the containment of the standard maximal torus in the standard Borel candidate for the general-rank GLₙ example in Layer 7 of the ReductiveGroups roadmap. It supersedes the rank-two-only construction formerly in TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Borel.

Main declarations

• TauCeti.GeneralLinear.UpperTriangular.diagonalTorusCoordinateMap: the coordinate morphism from the upper-triangular coordinate algebra to the diagonal-torus coordinate algebra.
• TauCeti.GeneralLinear.UpperTriangular.diagonalTorus: the diagonal torus as a group-scheme morphism into the upper-triangular group.
• TauCeti.GeneralLinear.UpperTriangular.diagonalTorus_comp_inclusion: the factorization recovers the standard diagonal torus in GLₙ.

References

• J. S. Milne, Algebraic Groups (2017), Sections 12 and 21.
• T. A. Springer, Linear Algebraic Groups, second edition (1998), Sections 6.2 and 8.1.

theorem TauCeti.GeneralLinear.UpperTriangular.diagonalTorusPoints_mem (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)) : diagonalTorusPoints f ∈ CommHopfAlgCat.quotientPointsSubgroup (GeneralLinear.coordinateHopfAlgebra R n) (definingHopfIdeal R n) ↧A

Every diagonal-torus point belongs to the upper-triangular subgroup.

noncomputable def TauCeti.GeneralLinear.UpperTriangular.diagonalTorusCoordinateMap (R : Type u) [CommRing R] (n : ℕ) : coordinateHopfAlgebra R n ⟶ ↧(MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin n) →₀ ℤ)))

The coordinate morphism of the diagonal torus factored through the upper-triangular coordinate algebra.

Equations

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

@[simp]

theorem TauCeti.GeneralLinear.UpperTriangular.coordinateMap_comp_diagonalTorusCoordinateMap (R : Type u) [CommRing R] (n : ℕ) : CategoryTheory.CategoryStruct.comp (coordinateMap R n) (diagonalTorusCoordinateMap R n) = GeneralLinear.diagonalTorusCoordinateMap

Precomposing the factored diagonal-torus coordinate morphism with the upper-triangular quotient map recovers the ambient diagonal-torus coordinate morphism.

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

The standard diagonal torus as a morphism into the upper-triangular subgroup scheme.

Equations

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

theorem TauCeti.GeneralLinear.UpperTriangular.diagonalTorus_def (R : Type u) [CommRing R] (n : ℕ) : diagonalTorus R n = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧R).map (diagonalTorusCoordinateMap R n).op) (CategoryTheory.eqToHom ⋯))

The diagonal torus into the upper-triangular group is relative spectrum applied contravariantly to its factored coordinate morphism.

@[simp]

theorem TauCeti.GeneralLinear.UpperTriangular.diagonalTorus_comp_inclusion (R : Type u) [CommRing R] (n : ℕ) : CategoryTheory.CategoryStruct.comp (diagonalTorus R n) (inclusion R n) = GeneralLinear.diagonalTorus

Composing the diagonal torus inside the upper-triangular subgroup with its inclusion into GLₙ gives the standard diagonal torus of GLₙ.

@[simp]

theorem TauCeti.GeneralLinear.UpperTriangular.pointsMulEquiv_diagonalTorusCoordinateMap (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 R n) (WithConv.toConv (f.ofConv.comp ↑(CommHopfAlgCat.Hom.hom (diagonalTorusCoordinateMap R n))))) = (GeneralLinear.pointsMulEquiv n) (diagonalTorusPoints f)

Under the upper-triangular and general-linear point equivalences, the factored coordinate morphism gives the same diagonal matrix as the ambient diagonal-torus morphism.