The upper-triangular subgroup scheme of SLₙ

The matrix coordinates strictly below the diagonal generate a Hopf ideal in O(SLₙ): it is the image of the upper-triangular Hopf ideal of GLₙ under the determinant-one quotient. Its quotient represents the upper-triangular determinant-one matrices: over every commutative algebra A, the points cut out by this ideal are the matrices of SLₙ(A) that are upper triangular in GLₙ(A).

This closed subgroup is smooth over every commutative ring, because upper-triangular determinant-one matrices lift across nilpotent thickenings, and its geometric points form a solvable group. These are inputs for identifying it as a Borel subgroup of SLₙ.

Main declarations

• TauCeti.SpecialLinear.UpperTriangular.definingHopfIdeal: the upper-triangular Hopf ideal in O(SLₙ).
• TauCeti.SpecialLinear.UpperTriangular.definingHopfIdeal_toIdeal: it is generated by the coordinates strictly below the diagonal.
• TauCeti.SpecialLinear.UpperTriangular.mem_definingPointsSubgroup_iff: a point lies in the closed subgroup exactly when its matrix is upper triangular.
• TauCeti.SpecialLinear.UpperTriangular.pointsMulEquiv: the points of the quotient Hopf algebra are the upper-triangular determinant-one matrices.
• TauCeti.SpecialLinear.UpperTriangular.instSmoothCoordinateHopfAlgebra: smoothness over every commutative ring.
• TauCeti.SpecialLinear.UpperTriangular. geometricallySolvablePointsCommHopfAlgProperty_coordinateHopfAlgebra: solvability of the geometric points.

References

• J. S. Milne, Algebraic Groups (2017), Chapters 12 and 21.
• The construction generalizes the rank-two subgroup TauCeti.Algebra.AlgebraicGroup.SpecialLinear.Borel.Basic and follows the general-linear subgroup TauCeti.Algebra.AlgebraicGroup.GeneralLinear.UpperTriangular.Basic.

noncomputable def TauCeti.SpecialLinear.UpperTriangular.definingHopfIdeal (R : Type u) [CommRing R] (n : ℕ) : HopfIdeal R ↑(SpecialLinear.coordinateHopfAlgebra R n)

The Hopf ideal cutting out upper-triangular matrices inside SLₙ: the image of the general-linear upper-triangular Hopf ideal under the determinant-one quotient map.

Equations

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

theorem TauCeti.SpecialLinear.UpperTriangular.definingHopfIdeal_def (R : Type u) [CommRing R] (n : ℕ) : definingHopfIdeal R n = (GeneralLinear.UpperTriangular.definingHopfIdeal R n).map (CommHopfAlgCat.Hom.hom (SpecialLinear.coordinateMap R n))

The special-linear upper-triangular ideal is the image of the general-linear one.

theorem TauCeti.SpecialLinear.UpperTriangular.definingHopfIdeal_toIdeal (R : Type u) [CommRing R] (n : ℕ) : (definingHopfIdeal R n).toIdeal = Ideal.span (⇑(CommHopfAlgCat.Hom.hom (SpecialLinear.coordinateMap R n)) '' GeneralLinear.UpperTriangular.definingRelationSet R n)

The underlying ideal of the upper-triangular Hopf ideal of SLₙ is generated by the images of the matrix coordinates strictly below the diagonal.

theorem TauCeti.SpecialLinear.UpperTriangular.definingHopfIdeal_toIdeal_fg (R : Type u) [CommRing R] (n : ℕ) : (definingHopfIdeal R n).toIdeal.FG

The upper-triangular Hopf ideal of SLₙ is finitely generated as an ideal.

@[reducible, inline]

noncomputable abbrev TauCeti.SpecialLinear.UpperTriangular.coordinateHopfAlgebra (R : Type u) [CommRing R] (n : ℕ) : CommHopfAlgCat R

The coordinate Hopf algebra of the upper-triangular closed subgroup scheme of SLₙ.

Equations

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

@[reducible, inline]

noncomputable abbrev TauCeti.SpecialLinear.UpperTriangular.coordinateMap (R : Type u) [CommRing R] (n : ℕ) : SpecialLinear.coordinateHopfAlgebra R n ⟶ coordinateHopfAlgebra R n

The quotient coordinate morphism from O(SLₙ) to the upper-triangular coordinate Hopf algebra.

Equations

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

instance TauCeti.SpecialLinear.UpperTriangular.instAlgebraFiniteTypeCoordinateHopfAlgebra (R : Type u) [CommRing R] (n : ℕ) : Algebra.FiniteType R ↑(coordinateHopfAlgebra R n)

The upper-triangular special-linear coordinate Hopf algebra is finite type.

@[simp]

theorem TauCeti.SpecialLinear.UpperTriangular.mem_definingPointsSubgroup_iff (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] (g : ↑(HopfAlgebra.points ↧A)) : g ∈ CommHopfAlgCat.quotientPointsSubgroup (SpecialLinear.coordinateHopfAlgebra R n) (definingHopfIdeal R n) ↧A ↔ Matrix.SpecialLinearGroup.toGL ((SpecialLinear.pointsMulEquiv R n) g) ∈ upperTriangularGroup (Fin n) A

An SLₙ-point belongs to the upper-triangular closed subgroup exactly when its matrix is upper triangular.

noncomputable def TauCeti.SpecialLinear.UpperTriangular.pointsMulEquiv (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] : ↑(HopfAlgebra.points ↧A) ≃* ↥(Subgroup.comap Matrix.SpecialLinearGroup.toGL (upperTriangularGroup (Fin n) A))

The group of algebra-valued points of the upper-triangular coordinate Hopf algebra of SLₙ is the group of upper-triangular determinant-one matrices.

Equations

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

@[simp]

theorem TauCeti.SpecialLinear.UpperTriangular.pointsMulEquiv_coe (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] (f : ↑(HopfAlgebra.points ↧A)) : (SpecialLinear.pointsMulEquiv R n) ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (SpecialLinear.coordinateHopfAlgebra R n) (definingHopfIdeal R n) ↧A)) f) = ↑((pointsMulEquiv R n) f)

Under the upper-triangular and special-linear point equivalences, the quotient-point inclusion is the ordinary inclusion of upper-triangular matrices into SLₙ.

@[simp]

theorem TauCeti.SpecialLinear.UpperTriangular.quotientPointsHom_pointsMulEquiv_symm (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] (g : ↥(Subgroup.comap Matrix.SpecialLinearGroup.toGL (upperTriangularGroup (Fin n) A))) : (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (SpecialLinear.coordinateHopfAlgebra R n) (definingHopfIdeal R n) ↧A)) ((pointsMulEquiv R n).symm g) = (SpecialLinear.pointsMulEquiv R n).symm ↑g

The ambient point attached to an upper-triangular determinant-one matrix is the special-linear point attached to that matrix.

theorem TauCeti.SpecialLinear.UpperTriangular.pointsMulEquiv_mapValue (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 : ↑(HopfAlgebra.points ↧A)) : ↑((pointsMulEquiv R n) ((AlgHom.mapValue phi) f)) = (Matrix.SpecialLinearGroup.map phi.toRingHom) ↑((pointsMulEquiv R n) f)

The upper-triangular point equivalence of SLₙ is natural in the value algebra: postcomposition of points agrees with entrywise mapping of matrices.

theorem TauCeti.SpecialLinear.UpperTriangular.isSolvable_points (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] : Group.IsSolvable ↑(HopfAlgebra.points ↧A)

Every algebra-valued point group of the upper-triangular subgroup of SLₙ is solvable.

theorem TauCeti.SpecialLinear.UpperTriangular.geometricallySolvablePointsCommHopfAlgProperty_coordinateHopfAlgebra (n : ℕ) (k : Type u) [Field k] : geometricallySolvablePointsCommHopfAlgProperty k (coordinateHopfAlgebra k n)

The upper-triangular subgroup of SLₙ has a solvable group of geometric points.

instance TauCeti.SpecialLinear.UpperTriangular.instSmoothCoordinateHopfAlgebra (R : Type u) [CommRing R] (n : ℕ) : Algebra.Smooth R ↑(coordinateHopfAlgebra R n)

The upper-triangular subgroup of SLₙ is smooth over every commutative ring.

theorem TauCeti.SpecialLinear.UpperTriangular.smoothCommHopfAlgProperty_coordinateHopfAlgebra (n : ℕ) (k : Type u) [Field k] : smoothCommHopfAlgProperty k (coordinateHopfAlgebra k n)

The upper-triangular coordinate Hopf algebra of SLₙ is smooth over a field.