Documentation

TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Borel

The upper-triangular Borel subgroup scheme of GL₂ #

For a commutative ring R, this file specializes the standard upper-triangular subgroup of GL_n to rank two. For the weights (1, 0) the only forbidden coordinate is the lower-left one, so the defining Hopf ideal in the coordinate Hopf algebra of GL₂ is the principal ideal (X₁₀).

Everything else about this subgroup is the general-rank UpperTriangular API at n = 2: the closed subgroup scheme TauCeti.GeneralLinear.UpperTriangular.groupScheme R 2, its closed immersion TauCeti.GeneralLinear.UpperTriangular.inclusion R 2 into GL₂, the description of its points as upper-triangular matrices (TauCeti.GeneralLinear.UpperTriangular.pointsMulEquiv), and the fact that it is a Borel subgroup over every field (TauCeti.GeneralLinear.UpperTriangular.isBorel_definingHopfIdeal).

Main declarations #

References #

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

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

Equations
Instances For
    source
    theorem TauCeti.GeneralLinear.Borel.lowerLeftCoordinate_def (R : Type u) [CommRing R] :
    lowerLeftCoordinate R = (coordinateHopfAlgebraAlgEquiv R 2) ((coordinateRingMap R 2) (MvPolynomial.X (1, 0)))

    The lower-left coordinate is the image of the corresponding generic matrix variable.

    source
    @[reducible, inline]
    abbrev TauCeti.GeneralLinear.Borel.weights :
    Fin 2 → ℤ

    The weights (1, 0) whose weight parabolic is the standard upper-triangular Borel.

    Equations
    Instances For
      source
      theorem TauCeti.GeneralLinear.Borel.weightParabolicRelationSet_weights (R : Type u) [CommRing R] :
      weightParabolicRelationSet R weights = {lowerLeftCoordinate R}

      For the weights (1, 0), the weight-parabolic relation set is the singleton containing the lower-left coordinate.

      source
      @[reducible, inline]
      noncomputable abbrev TauCeti.GeneralLinear.Borel.definingHopfIdeal (R : Type u) [CommRing R] :
      HopfIdeal R ↑(GeneralLinear.coordinateHopfAlgebra R 2)

      The Hopf ideal (X₁₀) cutting out the upper-triangular matrices inside GL₂.

      Equations
      Instances For
        source
        theorem TauCeti.GeneralLinear.Borel.definingHopfIdeal_toIdeal (R : Type u) [CommRing R] :
        (definingHopfIdeal R).toIdeal = Ideal.span {lowerLeftCoordinate R}

        The underlying ideal of the Borel Hopf ideal is the principal ideal (X₁₀).

        source
        @[reducible, inline]
        noncomputable abbrev TauCeti.GeneralLinear.Borel.coordinateHopfAlgebra (R : Type u) [CommRing R] :
        CommHopfAlgCat R

        The coordinate Hopf algebra of the upper-triangular Borel subgroup scheme of GL₂.

        Equations
        Instances For