Documentation

TauCeti.Algebra.AlgebraicGroup.GeneralLinear.DiagonalTorus.Maximal

Maximality of the diagonal torus in the general linear group #

Over any field, the diagonal torus of GL_n is a maximal torus. Over an algebraically closed field, it is moreover maximal among reduced commutative closed subgroup schemes. In Hopf coordinates, its defining ideal is the kernel of the surjective restriction morphism from O(GL_n) to the Laurent coordinate ring of the split torus.

The proof compares algebraically closed points. A reduced commutative closed subgroup containing the diagonal torus gives a commutative matrix subgroup containing all invertible diagonal matrices. The point-level centralizer calculation says that this subgroup is exactly the diagonal torus. Reduced finite-type point separation then upgrades equality of point subgroups to equality of their defining Hopf ideals.

This statement is stronger than maximality among tori: every torus is reduced and commutative, whereas the competing subgroup below need not itself be a torus or connected.

Main declarations #

References #

This completes the standard GL_n maximal-torus example required by Layer 7, "Borel subgroups, maximal tori", of the ReductiveGroups roadmap. Together with the existing adjoint root spaces and normalizer quotient, it validates the torus used by the packaged GL_n root datum and Weyl group.

source
noncomputable def TauCeti.GeneralLinear.diagonalTorusDefiningIdeal (k : Type u) [Field k] (n : ℕ) :
HopfIdeal k ↑(coordinateHopfAlgebra k n)

The Hopf ideal defining the diagonal torus inside the coordinate Hopf algebra of GL_n.

It is the ordinary kernel of the surjective restriction morphism to the split-torus coordinate ring, packaged as a Hopf ideal.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.GeneralLinear.mem_diagonalTorusDefiningIdeal (k : Type u) [Field k] (n : ℕ) (x : ↑(coordinateHopfAlgebra k n)) :
    x ∈ diagonalTorusDefiningIdeal k n ↔ (CommHopfAlgCat.Hom.hom diagonalTorusCoordinateMap) x = 0

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

    source
    noncomputable def TauCeti.GeneralLinear.diagonalTorusCoordinateIso (k : Type u) [Field k] (n : ℕ) :
    FiniteTypeCommHopfAlgCat.quotient { obj := coordinateHopfAlgebra k n, property := ⋯ } (diagonalTorusDefiningIdeal k n) ≅ DiagonalizableGroup.coordinateRing k (SplitTorus.characterGroup (ULift.{u, 0} (Fin n)))

    The quotient by the diagonal-torus defining ideal is its Laurent coordinate Hopf algebra.

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

      The diagonal-torus quotient isomorphism identifies the quotient morphism with the canonical restriction to diagonal coordinates.

      source
      @[simp]
      theorem TauCeti.GeneralLinear.map_baseChangeHopfIdeal_diagonalTorusDefiningIdeal (k : Type u) [Field k] (n : ℕ) (K : Type u) [Field K] [Algebra k K] :
      (CommHopfAlgCat.baseChangeHopfIdeal (diagonalTorusDefiningIdeal k n)).map (CommHopfAlgCat.Hom.hom (coordinateHopfAlgebraBaseChangeIso k K n).hom) = diagonalTorusDefiningIdeal K n

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

      source
      theorem TauCeti.GeneralLinear.splitTorusCommHopfAlgProperty_quotient_diagonalTorusDefiningIdeal (k : Type u) [Field k] (n : ℕ) :
      splitTorusCommHopfAlgProperty k (FiniteTypeCommHopfAlgCat.quotient { obj := coordinateHopfAlgebra k n, property := ⋯ } (diagonalTorusDefiningIdeal k n))

      The quotient coordinate Hopf algebra of the diagonal torus is a split torus of rank n.

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

      The quotient coordinate Hopf algebra of the diagonal torus is a torus.

      source
      theorem TauCeti.GeneralLinear.quotientPointsSubgroup_diagonalTorusDefiningIdeal (k : Type u) [Field k] (n : ℕ) (A : CommAlgCat k) :
      CommHopfAlgCat.quotientPointsSubgroup (coordinateHopfAlgebra k n) (diagonalTorusDefiningIdeal k n) A = (GrpCat.Hom.hom ((CommHopfAlgCat.mapPointsFunctor diagonalTorusCoordinateMap).app A)).range

      The points cut out by diagonalTorusDefiningIdeal are exactly the diagonal-torus points.

      source
      theorem TauCeti.GeneralLinear.eq_diagonalTorusDefiningIdeal_of_le_of_isCocomm (k : Type u) [Field k] (n : ℕ) [IsAlgClosed k] (I : HopfIdeal k ↑(coordinateHopfAlgebra k n)) [IsReduced ↑(CommHopfAlgCat.quotient (coordinateHopfAlgebra k n) I)] [Coalgebra.IsCocomm k ↑(CommHopfAlgCat.quotient (coordinateHopfAlgebra k n) I)] (hI : I ≤ diagonalTorusDefiningIdeal k n) :
      I = diagonalTorusDefiningIdeal k n

      The diagonal torus of GL_n is maximal among reduced commutative closed subgroup schemes over an algebraically closed field.

      If I cuts out a reduced commutative closed subgroup containing the diagonal torus, then I is the diagonal-torus defining ideal. Containment is written contravariantly as I ≤ diagonalTorusDefiningIdeal k n; commutativity is the cocommutativity of the quotient coordinate Hopf algebra.

      source
      theorem TauCeti.GeneralLinear.isMaximalTorus_diagonalTorusDefiningIdeal (k : Type u) [Field k] (n : ℕ) :
      HopfIdeal.IsMaximalTorus k (coordinateHopfAlgebra k n) (diagonalTorusDefiningIdeal k n)

      The diagonal torus of GL_n is a maximal torus over every field. Maximality is checked after base change to an algebraic closure, where the stronger pointwise maximality theorem applies, and then descended using faithful flatness.