The upper-triangular closed subgroup scheme of SL₂

The lower-left coordinate in O(SL₂) generates a Hopf ideal. Its quotient represents the upper-triangular determinant-one matrices: over every commutative algebra A, the points cut out by this ideal identify with the existing subgroup TauCeti.SL2Borel A.

Over a field, this closed subgroup is maximal among closed subgroups whose coordinate algebra is reduced and whose geometric points are solvable. In particular, it is maximal among smooth closed subgroups with solvable geometric points. This is a direct rank-two maximality statement; that the upper-triangular subgroup is a Borel subgroup is proved in every rank in TauCeti.Algebra.AlgebraicGroup.SpecialLinear.UpperTriangular.Borel.

Main declarations

• TauCeti.SpecialLinear.Borel.definingHopfIdeal: the lower-left-coordinate Hopf ideal in O(SL₂).
• TauCeti.SpecialLinear.Borel.definingHopfIdeal_eq_upperTriangular_definingHopfIdeal: it is the rank-two case of the upper-triangular Hopf ideal of SLₙ.
• TauCeti.SpecialLinear.Borel.definingHopfIdeal_toIdeal: its underlying ideal is generated by the lower-left coordinate.
• TauCeti.SpecialLinear.Borel.coordinateMap_ker: the kernel of the quotient coordinate map is the lower-left-coordinate ideal.
• TauCeti.SpecialLinear.Borel.mem_definingPointsSubgroup_iff: its algebra-valued points are precisely the matrices in SL2Borel.
• TauCeti.SpecialLinear.Borel.pointsMulEquiv: the resulting equivalence from quotient Hopf points to SL2Borel.
• TauCeti.SpecialLinear.Borel.definingHopfIdeal_le_of_le_of_isReduced_of_geometricallySolvable: maximality among closed subgroups with reduced coordinate algebra and solvable geometric points.
• TauCeti.SpecialLinear.Borel.definingHopfIdeal_le_of_le_of_smooth_of_geometricallySolvable: maximality among smooth closed subgroups with solvable geometric points.

References

• J. S. Milne, Algebraic Groups (2017), Chapters 12 and 21.
• R. W. Carter, Simple Groups of Lie Type (1972), Section 8.2.
• The Hopf ideal and maximality argument adapt TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Borel.
• The point-subgroup and point-equivalence API adapts TauCeti.Algebra.AlgebraicGroup.SpecialLinear.Basic.
• The maximal-solvability input is TauCeti.SL2Borel.le_of_isSolvable_of_infinite from TauCeti.LinearAlgebra.Matrix.SpecialLinearGroup.Borel.

noncomputable def TauCeti.SpecialLinear.Borel.lowerLeftCoordinate (R : Type u) [CommRing R] : ↑(SpecialLinear.coordinateHopfAlgebra R 2)

The lower-left coordinate of the generic determinant-one 2 × 2 matrix.

Equations

• TauCeti.SpecialLinear.Borel.lowerLeftCoordinate R = (CommHopfAlgCat.Hom.hom (TauCeti.SpecialLinear.coordinateMap R 2)) (TauCeti.GeneralLinear.Borel.lowerLeftCoordinate R)

theorem TauCeti.SpecialLinear.Borel.lowerLeftCoordinate_def (R : Type u) [CommRing R] : lowerLeftCoordinate R = (CommHopfAlgCat.Hom.hom (SpecialLinear.coordinateMap R 2)) (GeneralLinear.Borel.lowerLeftCoordinate R)

The lower-left coordinate is the image of its general-linear counterpart.

noncomputable def TauCeti.SpecialLinear.Borel.definingHopfIdeal (R : Type u) [CommRing R] : HopfIdeal R ↑(SpecialLinear.coordinateHopfAlgebra R 2)

The Hopf ideal cutting out upper-triangular matrices inside SL₂.

It is the image of the general-linear upper-triangular Hopf ideal under the determinant-one quotient map.

Equations

• TauCeti.SpecialLinear.Borel.definingHopfIdeal R = (TauCeti.GeneralLinear.Borel.definingHopfIdeal R).map (CommHopfAlgCat.Hom.hom (TauCeti.SpecialLinear.coordinateMap R 2))

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

The special-linear Borel ideal is the image of the general-linear Borel ideal under the determinant-one quotient map.

theorem TauCeti.SpecialLinear.Borel.definingHopfIdeal_eq_upperTriangular_definingHopfIdeal (R : Type u) [CommRing R] : definingHopfIdeal R = UpperTriangular.definingHopfIdeal R 2

The special-linear Borel ideal is the rank-two case of the upper-triangular Hopf ideal of SLₙ.

theorem TauCeti.SpecialLinear.Borel.definingHopfIdeal_toIdeal (R : Type u) [CommRing R] : (definingHopfIdeal R).toIdeal = Ideal.span {lowerLeftCoordinate R}

The underlying ideal of the special-linear Borel Hopf ideal is generated by the lower-left coordinate.

@[reducible, inline]

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

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

Equations

• TauCeti.SpecialLinear.Borel.coordinateHopfAlgebra R = TauCeti.CommHopfAlgCat.quotient (TauCeti.SpecialLinear.coordinateHopfAlgebra R 2) (TauCeti.SpecialLinear.Borel.definingHopfIdeal R)

@[reducible, inline]

noncomputable abbrev TauCeti.SpecialLinear.Borel.coordinateMap (R : Type u) [CommRing R] : SpecialLinear.coordinateHopfAlgebra R 2 ⟶ coordinateHopfAlgebra R

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

Equations

• TauCeti.SpecialLinear.Borel.coordinateMap R = TauCeti.CommHopfAlgCat.mkQuotient (TauCeti.SpecialLinear.coordinateHopfAlgebra R 2) (TauCeti.SpecialLinear.Borel.definingHopfIdeal R)

theorem TauCeti.SpecialLinear.Borel.coordinateMap_apply (R : Type u) [CommRing R] (h : ↑(SpecialLinear.coordinateHopfAlgebra R 2)) : (CommHopfAlgCat.Hom.hom (coordinateMap R)) h = (Ideal.Quotient.mkₐ R (definingHopfIdeal R).toIdeal) h

The upper-triangular quotient coordinate morphism sends an ambient coordinate to its quotient class.

theorem TauCeti.SpecialLinear.Borel.coordinateMap_ker (R : Type u) [CommRing R] : RingHom.ker (↑(CommHopfAlgCat.Hom.hom (coordinateMap R))).toRingHom = Ideal.span {lowerLeftCoordinate R}

The kernel of the upper-triangular quotient coordinate morphism is the principal lower-left-coordinate ideal.

@[simp]

theorem TauCeti.SpecialLinear.Borel.coordinateMap_lowerLeftCoordinate (R : Type u) [CommRing R] : (CommHopfAlgCat.Hom.hom (coordinateMap R)) (lowerLeftCoordinate R) = 0

The lower-left coordinate vanishes in the upper-triangular quotient coordinate algebra.

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

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

@[simp]

theorem TauCeti.SpecialLinear.Borel.mem_definingPointsSubgroup_iff (R : Type u) [CommRing R] {A : Type w} [CommRing A] [Algebra R A] (g : ↑(HopfAlgebra.points ↧A)) : g ∈ CommHopfAlgCat.quotientPointsSubgroup (SpecialLinear.coordinateHopfAlgebra R 2) (definingHopfIdeal R) ↧A ↔ (SpecialLinear.pointsMulEquiv R 2) g ∈ SL2Borel A

An algebra-valued point belongs to the subgroup cut out in SL₂ exactly when its matrix is upper triangular, equivalently when it belongs to SL2Borel.

noncomputable def TauCeti.SpecialLinear.Borel.pointsMulEquiv (R : Type u) [CommRing R] {A : Type w} [CommRing A] [Algebra R A] : ↑(HopfAlgebra.points ↧A) ≃* ↥(SL2Borel A)

The group of algebra-valued points of the upper-triangular special-linear coordinate Hopf algebra is the standard Borel subgroup SL2Borel.

Equations

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

@[simp]

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

Under the Borel and special-linear point equivalences, the quotient-point inclusion is the ordinary inclusion of the standard Borel into SL₂.

@[simp]

theorem TauCeti.SpecialLinear.Borel.quotientPointsHom_pointsMulEquiv_symm (R : Type u) [CommRing R] {A : Type w} [CommRing A] [Algebra R A] (g : ↥(SL2Borel A)) : (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (SpecialLinear.coordinateHopfAlgebra R 2) (definingHopfIdeal R) ↧A)) ((pointsMulEquiv R).symm g) = (SpecialLinear.pointsMulEquiv R 2).symm ↑g

The ambient point attached to a standard Borel matrix is the special-linear point attached to its ordinary inclusion.

@[simp]

theorem TauCeti.SpecialLinear.Borel.pointsMulEquiv_mapValue (R : Type u) [CommRing R] {A : Type w} [CommRing A] [Algebra R A] {B : Type u_1} [CommRing B] [Algebra R B] (phi : A →ₐ[R] B) (f : ↑(HopfAlgebra.points ↧A)) : (pointsMulEquiv R) (WithConv.toConv (phi.comp f.ofConv)) = (SL2Borel.map phi.toRingHom) ((pointsMulEquiv R) f)

The standard Borel point equivalence is natural in the value algebra.

theorem TauCeti.SpecialLinear.Borel.definingHopfIdeal_le_of_le_of_isReduced_of_geometricallySolvable {k : Type u} [Field k] (I : HopfIdeal k ↑(SpecialLinear.coordinateHopfAlgebra k 2)) (hIB : I ≤ definingHopfIdeal k) [IsReduced ↑(CommHopfAlgCat.quotient (SpecialLinear.coordinateHopfAlgebra k 2) I)] (hIsolvable : geometricallySolvablePointsCommHopfAlgProperty k (CommHopfAlgCat.quotient (SpecialLinear.coordinateHopfAlgebra k 2) I)) : definingHopfIdeal k ≤ I

The standard upper-triangular Hopf ideal in O(SL₂) is maximal, in the reverse ideal order corresponding to inclusion of closed subgroups, among closed subgroups with reduced coordinate algebra and solvable geometric points.

theorem TauCeti.SpecialLinear.Borel.definingHopfIdeal_le_of_le_of_smooth_of_geometricallySolvable {k : Type u} [Field k] (I : HopfIdeal k ↑(SpecialLinear.coordinateHopfAlgebra k 2)) (hIB : I ≤ definingHopfIdeal k) (hIsmooth : smoothCommHopfAlgProperty k (CommHopfAlgCat.quotient (SpecialLinear.coordinateHopfAlgebra k 2) I)) (hIsolvable : geometricallySolvablePointsCommHopfAlgProperty k (CommHopfAlgCat.quotient (SpecialLinear.coordinateHopfAlgebra k 2) I)) : definingHopfIdeal k ≤ I

The standard upper-triangular Hopf ideal in O(SL₂) is maximal, in the reverse ideal order corresponding to inclusion of closed subgroups, among smooth closed subgroups with solvable geometric points.