Documentation

TauCeti.Algebra.AlgebraicGroup.SpecialLinear.Borel.Geometry

Geometry of the standard Borel subgroup of SL₂ #

The upper-triangular determinant-one subgroup of SL₂ is smooth, geometrically connected, and geometrically solvable. Its coordinate algebra has the explicit presentation

R[T, T⁻¹][X],

where T is the upper-left diagonal entry and X is the upper-right entry. This presentation also makes geometric connectedness transparent: after extending a field, the coordinate ring remains a polynomial ring over a Laurent polynomial domain.

Smoothness is the rank-two case of smoothness of the upper-triangular subgroup of SLₙ, which follows from the infinitesimal lifting property for upper-triangular determinant-one matrices across nilpotent quotients.

The subgroup here is the rank-two upper-triangular subgroup of SLₙ (TauCeti.SpecialLinear.Borel.definingHopfIdeal_eq_upperTriangular_definingHopfIdeal). That it is a Borel subgroup, and that the Borel subgroups are its conjugates, is proved in every rank in TauCeti.Algebra.AlgebraicGroup.SpecialLinear.UpperTriangular.Borel.

Main declarations #

References #

Polynomial-Laurent presentation #

source
noncomputable def TauCeti.SpecialLinear.Borel.tautologicalPoint (R : Type u) [CommRing R] :
↥(SL2Borel ↑(coordinateHopfAlgebra R))

The tautological point of the standard Borel in its own coordinate algebra.

Equations
Instances For
    source
    noncomputable def TauCeti.SpecialLinear.Borel.diagonalUnit (R : Type u) [CommRing R] :
    (↑(coordinateHopfAlgebra R))ˣ

    The upper-left diagonal coordinate of the standard SL₂ Borel, bundled as a unit.

    Equations
    Instances For
      source
      theorem TauCeti.SpecialLinear.Borel.diagonalUnit_val (R : Type u) [CommRing R] :
      ↑(diagonalUnit R) = ↑↑(tautologicalPoint R) 0 0
      source
      noncomputable def TauCeti.SpecialLinear.Borel.upperRightCoordinate (R : Type u) [CommRing R] :
      ↑(coordinateHopfAlgebra R)

      The upper-right coordinate of the standard SL₂ Borel.

      Equations
      Instances For
        source
        theorem TauCeti.SpecialLinear.Borel.upperRightCoordinate_def (R : Type u) [CommRing R] :
        upperRightCoordinate R = ↑↑(tautologicalPoint R) 0 1
        source
        noncomputable def TauCeti.SpecialLinear.Borel.coordinateAlgEquiv (R : Type u) [CommRing R] :
        ↑(coordinateHopfAlgebra R) ≃ₐ[R] Polynomial (LaurentPolynomial R)

        Polynomial-Laurent coordinates on the standard SL₂ Borel. Its coordinate algebra is R[T, T⁻¹][X]: T records the upper-left diagonal unit and X records the free upper-right entry.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.SpecialLinear.Borel.coordinateAlgEquiv_diagonalUnit (R : Type u) [CommRing R] :
          (coordinateAlgEquiv R) ↑(diagonalUnit R) = Polynomial.C (LaurentPolynomial.T 1)

          The coordinate equivalence sends the diagonal unit to the Laurent generator.

          source
          @[simp]
          theorem TauCeti.SpecialLinear.Borel.coordinateAlgEquiv_upperRightCoordinate (R : Type u) [CommRing R] :
          (coordinateAlgEquiv R) (upperRightCoordinate R) = Polynomial.X

          The coordinate equivalence sends the upper-right coordinate to the polynomial generator.

          source
          @[simp]
          theorem TauCeti.SpecialLinear.Borel.coordinateAlgEquiv_symm_C_T (R : Type u) [CommRing R] :
          (coordinateAlgEquiv R).symm (Polynomial.C (LaurentPolynomial.T 1)) = ↑(diagonalUnit R)

          The inverse coordinate equivalence sends the Laurent generator to the diagonal unit.

          source
          @[simp]
          theorem TauCeti.SpecialLinear.Borel.coordinateAlgEquiv_symm_X (R : Type u) [CommRing R] :
          (coordinateAlgEquiv R).symm Polynomial.X = upperRightCoordinate R

          The inverse coordinate equivalence sends the polynomial generator to the upper-right coordinate.

          Base change #

          source
          noncomputable def TauCeti.SpecialLinear.Borel.coordinateHopfAlgebraBaseChangeIso (R : Type u) [CommRing R] (K : Type (max u v)) [CommRing K] [Algebra R K] :
          CommHopfAlgCat.baseChange (coordinateHopfAlgebra R) ≅ coordinateHopfAlgebra K

          Base change of the standard SL₂ Borel coordinate Hopf algebra is canonically the same coordinate Hopf algebra constructed over the new base.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem TauCeti.SpecialLinear.Borel.baseChangeMap_coordinateMap_comp_coordinateHopfAlgebraBaseChangeIso_hom (R : Type u) [CommRing R] (K : Type (max u v)) [CommRing K] [Algebra R K] :
            CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap (coordinateMap R)) (coordinateHopfAlgebraBaseChangeIso R K).hom = CategoryTheory.CategoryStruct.comp (SpecialLinear.coordinateHopfAlgebraBaseChangeIso R K 2).hom (coordinateMap K)

            The Borel base-change isomorphism commutes with the quotient coordinate morphisms from O(SL₂).

            source
            theorem TauCeti.SpecialLinear.Borel.geometricallyConnectedCommHopfAlgProperty_coordinateHopfAlgebra (k : Type u) [Field k] :
            geometricallyConnectedCommHopfAlgProperty k (coordinateHopfAlgebra k)

            The standard SL₂ Borel coordinate Hopf algebra is geometrically connected. After every field extension its coordinate ring is a polynomial ring over a Laurent polynomial domain.

            source
            instance TauCeti.SpecialLinear.Borel.instSmoothCoordinateHopfAlgebra (R : Type u) [CommRing R] :
            Algebra.Smooth R ↑(coordinateHopfAlgebra R)

            The coordinate algebra of the upper-triangular determinant-one subgroup of SL₂ is smooth over every commutative base ring, as the rank-two case of the upper-triangular subgroup of SLₙ.

            source
            theorem TauCeti.SpecialLinear.Borel.smoothCommHopfAlgProperty_coordinateHopfAlgebra (k : Type u) [Field k] :
            smoothCommHopfAlgProperty k (coordinateHopfAlgebra k)

            The standard Borel coordinate algebra is smooth over a field.

            source
            theorem TauCeti.SpecialLinear.Borel.isSolvable_points (R : Type u) [CommRing R] (A : Type u_1) [CommRing A] [Algebra R A] :
            Group.IsSolvable ↑(HopfAlgebra.points ↧A)

            Every algebra-valued point group of the standard SL₂ Borel is solvable.

            source
            theorem TauCeti.SpecialLinear.Borel.geometricallySolvablePointsCommHopfAlgProperty_coordinateHopfAlgebra (k : Type u) [Field k] :
            geometricallySolvablePointsCommHopfAlgProperty k (coordinateHopfAlgebra k)

            The standard SL₂ Borel has a solvable group of geometric points.