Documentation

TauCeti.Algebra.AlgebraicGroup.Unipotent.Semisimple

Semisimple unipotent affine groups are trivial #

Over a perfect field, a point that is both semisimple and unipotent is the identity. This file turns that pointwise fact into a scheme-theoretic rigidity statement: if a reduced finite-type commutative Hopf algebra has only semisimple and unipotent geometric points, then its counit is an isomorphism with the base field. Reducedness is essential because geometric points do not detect infinitesimal group schemes such as μₚ and αₚ in characteristic p.

The main application is to diagonalizable groups. Every point of a diagonalizable group is semisimple, and semisimplicity is reflected by a closed immersion. It follows that every reduced finite-type closed subgroup of a diagonalizable group whose geometric points are unipotent is the trivial group. This is the rigidity input for the reductive-groups roadmap: once the unipotent radical is constructed, it proves that the unipotent radical of a torus is trivial.

Main declarations #

References #

This advances Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap. It supplies the trivial-unipotent-subgroup argument needed to prove that tori are reductive, using the geometric unipotence and diagonalizable-group semisimplicity developed in Layers 4 and 5.

source
theorem TauCeti.HopfAlgebra.IsSemisimplePoint.eq_one_of_isUnipotent {k H L : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [Field L] [Algebra k L] [PerfectField L] {g : WithConv (H →ₐ[k] L)} (hsemisimple : IsSemisimplePoint g) (hunipotent : IsUnipotentPoint g) :
g = 1

A point that is both semisimple and unipotent is the identity.

source
theorem TauCeti.FiniteTypeCommHopfAlgCat.counitBialgHom_bijective_of_geometricallySemisimple_of_geometricallyUnipotent {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) [IsReduced ↑H.obj] (hsemisimple : geometricallySemisimplePointsCommHopfAlgProperty k H.obj) (hunipotent : geometricallyUnipotentPointsCommHopfAlgProperty k H.obj) :
Function.Bijective ⇑(Bialgebra.counitBialgHom k ↑H.obj)

The counit of a reduced finite-type commutative Hopf algebra is bijective when every geometric point is both semisimple and unipotent.

source
noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.counitBialgEquivOfGeometricallySemisimpleUnipotent {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) [IsReduced ↑H.obj] (hsemisimple : geometricallySemisimplePointsCommHopfAlgProperty k H.obj) (hunipotent : geometricallyUnipotentPointsCommHopfAlgProperty k H.obj) :
↑H.obj ≃ₐc[k] k

A reduced finite-type affine group whose geometric points are all semisimple and unipotent is the trivial group: its counit is a bialgebra equivalence with the base field.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.FiniteTypeCommHopfAlgCat.counitBialgEquivOfGeometricallySemisimpleUnipotent_apply {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) [IsReduced ↑H.obj] (hsemisimple : geometricallySemisimplePointsCommHopfAlgProperty k H.obj) (hunipotent : geometricallyUnipotentPointsCommHopfAlgProperty k H.obj) (x : ↑H.obj) :
    (H.counitBialgEquivOfGeometricallySemisimpleUnipotent hsemisimple hunipotent) x = CoalgebraStruct.counit x

    The equivalence from a geometrically semisimple and unipotent affine group to the base field is its counit.

    source
    @[simp]
    theorem TauCeti.FiniteTypeCommHopfAlgCat.counitBialgEquivOfGeometricallySemisimpleUnipotent_symm_apply {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) [IsReduced ↑H.obj] (hsemisimple : geometricallySemisimplePointsCommHopfAlgProperty k H.obj) (hunipotent : geometricallyUnipotentPointsCommHopfAlgProperty k H.obj) (r : k) :
    (H.counitBialgEquivOfGeometricallySemisimpleUnipotent hsemisimple hunipotent).symm r = (algebraMap k ↑H.obj) r

    The inverse counit equivalence is the structure map from the base field.

    source
    theorem TauCeti.FiniteTypeCommHopfAlgCat.eq_augmentation_of_geometricallySemisimple_of_geometricallyUnipotent {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) (I : HopfIdeal k ↑H.obj) [IsReduced ↑(H.quotient I).obj] (hsemisimple : geometricallySemisimplePointsCommHopfAlgProperty k (H.quotient I).obj) (hunipotent : geometricallyUnipotentPointsCommHopfAlgProperty k (H.quotient I).obj) :
    I = HopfIdeal.augmentation k ↑H.obj

    A Hopf ideal is the augmentation ideal when its quotient is reduced, finite type, and has only semisimple and unipotent geometric points. Equivalently, the closed subgroup cut out by the ideal is trivial.

    source
    noncomputable def TauCeti.DiagonalizableGroup.quotientCounitBialgEquivOfGeometricallyUnipotent (k : Type u) [Field k] (G : FGCommGrpCat) (I : HopfIdeal k ↑(coordinateRing k G).obj) [IsReduced ↑((coordinateRing k G).quotient I).obj] (hI : geometricallyUnipotentPointsCommHopfAlgProperty k ((coordinateRing k G).quotient I).obj) :
    ↑((coordinateRing k G).quotient I).obj ≃ₐc[k] k

    A reduced finite-type closed subgroup of a diagonalizable group is trivial when all of its geometric points are unipotent.

    The closed subgroup is represented by the quotient of k[G] by I. No normality or connectedness hypothesis is needed: every quotient point embeds into the diagonalizable ambient group, hence is semisimple, and a semisimple unipotent point is the identity.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.DiagonalizableGroup.quotientCounitBialgEquivOfGeometricallyUnipotent_apply (k : Type u) [Field k] (G : FGCommGrpCat) (I : HopfIdeal k ↑(coordinateRing k G).obj) [IsReduced ↑((coordinateRing k G).quotient I).obj] (hI : geometricallyUnipotentPointsCommHopfAlgProperty k ((coordinateRing k G).quotient I).obj) (x : ↑((coordinateRing k G).quotient I).obj) :
      (quotientCounitBialgEquivOfGeometricallyUnipotent k G I hI) x = CoalgebraStruct.counit x

      The equivalence for a geometrically unipotent closed subgroup is its counit.

      source
      @[simp]
      theorem TauCeti.DiagonalizableGroup.quotientCounitBialgEquivOfGeometricallyUnipotent_symm_apply (k : Type u) [Field k] (G : FGCommGrpCat) (I : HopfIdeal k ↑(coordinateRing k G).obj) [IsReduced ↑((coordinateRing k G).quotient I).obj] (hI : geometricallyUnipotentPointsCommHopfAlgProperty k ((coordinateRing k G).quotient I).obj) (r : k) :
      (quotientCounitBialgEquivOfGeometricallyUnipotent k G I hI).symm r = (algebraMap k ↑((coordinateRing k G).quotient I).obj) r

      The inverse equivalence for a geometrically unipotent closed subgroup is the structure map.

      source
      theorem TauCeti.DiagonalizableGroup.eq_augmentation_of_geometricallyUnipotent (k : Type u) [Field k] (G : FGCommGrpCat) (I : HopfIdeal k ↑(coordinateRing k G).obj) [IsReduced ↑((coordinateRing k G).quotient I).obj] (hI : geometricallyUnipotentPointsCommHopfAlgProperty k ((coordinateRing k G).quotient I).obj) :
      I = HopfIdeal.augmentation k ↑(coordinateRing k G).obj

      The defining Hopf ideal of a reduced finite-type unipotent closed subgroup of a diagonalizable group is the augmentation ideal. Thus the closed subgroup is the identity subgroup, not merely abstractly isomorphic to it.