The diagonal torus as a closed subgroup of the general linear group

The diagonal morphism from the rank-n split torus to GL_n is a closed immersion over every commutative base ring. This file packages its image as a closed subgroup scheme.

The proof identifies the diagonal morphism with the general diagonal representation whose weights are the standard basis of the character lattice. Those weights span, so the general closed-immersion criterion for diagonalizable-group representations applies. This avoids a second coordinate-by-coordinate proof that the restriction map on coordinate rings is surjective.

The resulting closed subgroup is the torus in the split root datum of GL_n. Proving that it is maximal among tori is a separate geometric step in Layer 7 of the ReductiveGroups roadmap.

Main declarations

• TauCeti.GeneralLinear.diagonalTorus_eq_weightTorus: the diagonal torus is the weight torus for the standard basis of its character lattice.
• TauCeti.GeneralLinear.diagonalTorus_eq_diagonalGroupSchemeHom: its equivalent description as a diagonalizable-group representation.
• TauCeti.GeneralLinear.diagonalTorusCoordinateMap_surjective: the restriction map from the coordinate ring of GL_n onto that of the diagonal torus is surjective.
• TauCeti.GeneralLinear.isClosedImmersion_diagonalTorus: the diagonal torus morphism is a closed immersion.
• TauCeti.GeneralLinear.diagonalTorusClosedSubgroup: the diagonal torus as a closed subgroup scheme of GL_n.

References

• J. S. Milne, Algebraic Groups (2017), §§12 and 21.
• TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Scheme.Torus and TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Scheme.ToralClosure.Torus, whose weight-torus closedness constructions supplied the internal template.
• TauCeti.Algebra.AlgebraicGroup.DiagonalizableGroup.Scheme.GeneralLinear, in particular DiagonalizableGroup.isClosedImmersion_diagonalGroupSchemeHom.

This advances the split maximal-torus and root-datum target in Layer 7 of the ReductiveGroups roadmap.

theorem TauCeti.GeneralLinear.diagonalTorus_eq_weightTorus (R : Type u) [CommRing R] (N : ℕ) : diagonalTorus = weightTorus fun (i : Fin N) => (Pi.basisFun ℤ (ULift.{u, 0} (Fin N))) { down := i }

The diagonal torus is the weight torus prescribed by the standard basis of its character lattice.

theorem TauCeti.GeneralLinear.diagonalTorus_eq_diagonalGroupSchemeHom (R : Type u) [CommRing R] (N : ℕ) : diagonalTorus = DiagonalizableGroup.diagonalGroupSchemeHom (SplitTorus.characterGroup (ULift.{u, 0} (Fin N))) (Pi.basisFun R (Fin N)) fun (i : Fin N) => SplitTorus.weightCharacter ((Pi.basisFun ℤ (ULift.{u, 0} (Fin N))) { down := i })

The diagonal torus is the general diagonalizable-group representation specialized to the standard basis of its character lattice.

theorem TauCeti.GeneralLinear.diagonalTorusCoordinateMap_surjective (R : Type u) [CommRing R] (N : ℕ) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom diagonalTorusCoordinateMap)

The coordinate morphism restricting functions on GL_n to the diagonal torus is surjective.

instance TauCeti.GeneralLinear.isClosedImmersion_diagonalTorus (R : Type u) [CommRing R] (N : ℕ) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left diagonalTorus.hom.hom)

The diagonal split torus is a closed subgroup scheme of GL_n over every commutative base ring.

noncomputable def TauCeti.GeneralLinear.diagonalTorusClosedSubgroup (R : Type u) [CommRing R] (N : ℕ) : ClosedSubgroupScheme (groupScheme R N)

The diagonal split torus as a closed subgroup scheme of GL_n.

Equations

• TauCeti.GeneralLinear.diagonalTorusClosedSubgroup R N = TauCeti.ClosedSubgroupScheme.mk TauCeti.GeneralLinear.diagonalTorus

@[simp]

theorem TauCeti.GeneralLinear.coe_diagonalTorusClosedSubgroup (R : Type u) [CommRing R] (N : ℕ) : ↑(diagonalTorusClosedSubgroup R N) = CategoryTheory.Subobject.mk diagonalTorus

The underlying subobject of the closed diagonal torus is represented by the diagonal torus morphism.