Documentation

TauCeti.Algebra.AlgebraicGroup.SpecialLinear.DiagonalTorus.ClosedImmersion

The diagonal torus as a closed subgroup of the special linear group #

Over every commutative ring, the diagonal torus of SL_{r+1} is cut out by the Hopf ideal of functions whose restriction to the torus vanishes, the kernel of the surjective coordinate morphism TauCeti.SpecialLinear.diagonalTorusCoordinateMap. The quotient by this ideal is the Laurent coordinate Hopf algebra of the rank-r split torus, and the ideal is compatible with scalar extension. These constructions make the diagonal torus available as a closed subgroup when studying maximal tori.

Main declarations #

References #

source
noncomputable def TauCeti.SpecialLinear.diagonalTorusDefiningIdeal (r : ℕ) (R : Type u) [CommRing R] :
HopfIdeal R ↑(coordinateHopfAlgebra R (r + 1))

The Hopf ideal defining the diagonal torus inside the coordinate Hopf algebra of SL_{r+1}: the kernel of restriction to the torus.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.SpecialLinear.mem_diagonalTorusDefiningIdeal (r : ℕ) (R : Type u) [CommRing R] (x : ↑(coordinateHopfAlgebra R (r + 1))) :
    x ∈ diagonalTorusDefiningIdeal r R ↔ (CommHopfAlgCat.Hom.hom (diagonalTorusCoordinateMap r R)) x = 0

    A function belongs to the diagonal-torus ideal precisely when its restriction vanishes.

    source
    theorem TauCeti.SpecialLinear.diagonalTorusDefiningIdeal_eq_ker (r : ℕ) (R : Type u) [CommRing R] :
    diagonalTorusDefiningIdeal r R = HopfIdeal.kerOfSurjective (CommHopfAlgCat.Hom.hom (diagonalTorusCoordinateMap r R)) ⋯

    The diagonal-torus defining ideal is the kernel of restriction to the torus.

    source
    noncomputable def TauCeti.SpecialLinear.diagonalTorusCoordinateIso (r : ℕ) (R : Type u) [CommRing R] :
    FiniteTypeCommHopfAlgCat.quotient { obj := coordinateHopfAlgebra R (r + 1), property := ⋯ } (diagonalTorusDefiningIdeal r R) ≅ DiagonalizableGroup.coordinateRing R (SplitTorus.characterGroup (ULift.{u, 0} (Fin r)))

    The quotient by the diagonal-torus ideal is the Laurent coordinate Hopf algebra of the rank-r split torus.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.SpecialLinear.mkQuotient_comp_diagonalTorusCoordinateIso_hom (r : ℕ) (R : Type u) [CommRing R] :
      CategoryTheory.CategoryStruct.comp (FiniteTypeCommHopfAlgCat.mkQuotient { obj := coordinateHopfAlgebra R (r + 1), property := ⋯ } (diagonalTorusDefiningIdeal r R)) (diagonalTorusCoordinateIso r R).hom = CategoryTheory.ObjectProperty.homMk (diagonalTorusCoordinateMap r R)

      The quotient isomorphism identifies the quotient morphism with restriction to the torus.

      source
      theorem TauCeti.SpecialLinear.splitTorusCommHopfAlgProperty_quotient_diagonalTorusDefiningIdeal (r : ℕ) (R : Type u) [CommRing R] :
      splitTorusCommHopfAlgProperty R (FiniteTypeCommHopfAlgCat.quotient { obj := coordinateHopfAlgebra R (r + 1), property := ⋯ } (diagonalTorusDefiningIdeal r R))

      The coordinate quotient defining the diagonal torus of SL_{r+1} is a split torus.

      source
      @[simp]
      theorem TauCeti.SpecialLinear.map_baseChangeHopfIdeal_diagonalTorusDefiningIdeal (r : ℕ) (R : Type u) [CommRing R] (K : Type u) [CommRing K] [Algebra R K] :
      (CommHopfAlgCat.baseChangeHopfIdeal (diagonalTorusDefiningIdeal r R)).map (CommHopfAlgCat.Hom.hom (coordinateHopfAlgebraBaseChangeIso R K (r + 1)).hom) = diagonalTorusDefiningIdeal r K

      The base-change isomorphism of special-linear coordinate Hopf algebras carries the base-changed diagonal-torus ideal onto the diagonal-torus ideal over the extended base.

      source
      theorem TauCeti.SpecialLinear.torusCommHopfAlgProperty_quotient_diagonalTorusDefiningIdeal (r : ℕ) (k : Type u) [Field k] :
      torusCommHopfAlgProperty k (FiniteTypeCommHopfAlgCat.quotient { obj := coordinateHopfAlgebra k (r + 1), property := ⋯ } (diagonalTorusDefiningIdeal r k))

      Over a field, the coordinate quotient defining the diagonal torus of SL_{r+1} is a torus.