The diagonal torus in the special-linear Borel

The standard rank-r diagonal torus of SL_{r+1} factors through the upper-triangular subgroup scheme over every commutative ring. The factored coordinate morphism is surjective, so the resulting morphism T → B is a closed immersion. Its composite with B → SL_{r+1} recovers the standard torus, and its algebra-valued points are the same diagonal matrices in fundamental-weight coordinates.

This gives the represented containment of the chosen torus in the chosen Borel used in a standard type-A pinning. The elementary Hopf-ideal containment SpecialLinear.UpperTriangular.definingHopfIdeal_le_diagonalTorusDefiningIdeal supplies the factorization, including over nonreduced base rings, without using reductivity or maximality of the torus.

The construction uses CommHopfAlgCat.liftQuotient and SpecialLinear.diagonalTorusCoordinateMap. Its general-linear analogue is GeneralLinear.UpperTriangular.diagonalTorusCoordinateMap.

References

• J. S. Milne, Algebraic Groups (2017), §21, Example 21.2.
• B. Conrad, Reductive Group Schemes (2014), §5.1 (pinnings).

theorem TauCeti.SpecialLinear.UpperTriangular.definingHopfIdeal_le_diagonalTorusDefiningIdeal (r : ℕ) (R : Type u) [CommRing R] : definingHopfIdeal R (r + 1) ≤ diagonalTorusDefiningIdeal r R

The standard diagonal torus of SL_{r+1} lies in the upper-triangular subgroup over every commutative base ring. The order of Hopf ideals reverses inclusion of closed subgroups.

noncomputable def TauCeti.SpecialLinear.UpperTriangular.diagonalTorusCoordinateMap (r : ℕ) (R : Type u) [CommRing R] : coordinateHopfAlgebra R (r + 1) ⟶ (DiagonalizableGroup.coordinateRing R (SplitTorus.characterGroup (ULift.{u, 0} (Fin r)))).obj

Restriction from the special-linear upper-triangular coordinate algebra to its standard diagonal torus, in fundamental-weight coordinates.

Equations

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

@[simp]

theorem TauCeti.SpecialLinear.UpperTriangular.coordinateMap_comp_diagonalTorusCoordinateMap (r : ℕ) (R : Type u) [CommRing R] : CategoryTheory.CategoryStruct.comp (coordinateMap R (r + 1)) (diagonalTorusCoordinateMap r R) = SpecialLinear.diagonalTorusCoordinateMap r R

The factored coordinate map recovers restriction from SL_{r+1} to its diagonal torus.

@[simp]

theorem TauCeti.SpecialLinear.UpperTriangular.coordinateMap_comp_diagonalTorusCoordinateMap_assoc (r : ℕ) (R : Type u) [CommRing R] {Z : CommHopfAlgCat R} (h : ↧(MonoidAlgebra R ↑(SplitTorus.characterGroup (ULift.{u, 0} (Fin r)))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (coordinateMap R (r + 1)) (CategoryTheory.CategoryStruct.comp (diagonalTorusCoordinateMap r R) h) = CategoryTheory.CategoryStruct.comp (SpecialLinear.diagonalTorusCoordinateMap r R) h

The factored coordinate map recovers restriction from SL_{r+1} to its diagonal torus.

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

The torus-coordinate restriction from the Borel is surjective over every base ring.

@[simp]

theorem TauCeti.SpecialLinear.UpperTriangular.pointsMulEquiv_diagonalTorusCoordinateMap (r : ℕ) (R : Type u) [CommRing R] {A : Type v} [CommRing A] [Algebra R A] (f : WithConv (MonoidAlgebra R ↑(SplitTorus.characterGroup (ULift.{u, 0} (Fin r))) →ₐ[R] A)) : ↑((pointsMulEquiv R (r + 1)) (WithConv.toConv (f.ofConv.comp ↑(CommHopfAlgCat.Hom.hom (diagonalTorusCoordinateMap r R))))) = (SpecialLinear.pointsMulEquiv R (r + 1)) ((diagonalTorusPoints r R A) f)

Under the upper-triangular point equivalence, the factored torus map gives the same special-linear diagonal matrix as the ambient torus map.

noncomputable def TauCeti.SpecialLinear.UpperTriangular.diagonalTorus (r : ℕ) (R : Type u) [CommRing R] : SplitTorus.groupScheme R (ULift.{u, 0} (Fin r)) ⟶ CommHopfAlgCat.quotientSpec (SpecialLinear.coordinateHopfAlgebra R (r + 1)) (definingHopfIdeal R (r + 1))

The standard diagonal torus as a morphism into the represented special-linear upper-triangular subgroup.

Equations

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

@[simp]

theorem TauCeti.SpecialLinear.UpperTriangular.diagonalTorus_comp_quotientSpecι (r : ℕ) (R : Type u) [CommRing R] : CategoryTheory.CategoryStruct.comp (diagonalTorus r R) (CommHopfAlgCat.quotientSpecι (SpecialLinear.coordinateHopfAlgebra R (r + 1)) (definingHopfIdeal R (r + 1))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((AlgebraicGeometry.hopfSpec ↧R).map (SpecialLinear.diagonalTorusCoordinateMap r R).op)

Inclusion of the factored torus into SL_{r+1} recovers the spectrum of the standard diagonal-torus coordinate morphism.

@[simp]

theorem TauCeti.SpecialLinear.UpperTriangular.diagonalTorus_comp_quotientSpecι_assoc (r : ℕ) (R : Type u) [CommRing R] {Z : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))} (h : (AlgebraicGeometry.algSpec ↧R).mapGrp.obj ((commHopfAlgCatEquivCogrpCommAlgCat R).functor.leftOp.obj (Opposite.op (SpecialLinear.coordinateHopfAlgebra R (r + 1)))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (diagonalTorus r R) (CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.quotientSpecι (SpecialLinear.coordinateHopfAlgebra R (r + 1)) (definingHopfIdeal R (r + 1))) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.algSpec ↧R).mapGrp.map ((commHopfAlgCatEquivCogrpCommAlgCat R).functor.leftOp.map (SpecialLinear.diagonalTorusCoordinateMap r R).op)) h)

Inclusion of the factored torus into SL_{r+1} recovers the spectrum of the standard diagonal-torus coordinate morphism.

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

The standard torus is a closed subgroup scheme of the special-linear Borel.