Documentation

TauCeti.Algebra.AlgebraicGroup.Center.Reduced

The reduced center of an affine group #

The center of an affine group can be nonreduced, even when the ambient group is smooth. This file constructs its reduction in Hopf coordinates. First quotient by the center ideal, then quotient that coordinate algebra by its nilradical. Equivalently, the reduced center is cut out in the ambient coordinate algebra by the radical of the center ideal.

Assuming the tensor square of the reduced center coordinate algebra is reduced, its nilradical forms a Hopf ideal; this sufficient commutative-algebra hypothesis is kept explicit by TauCeti.HopfIdeal.reduction. The construction records both the nested quotient and the single ambient defining ideal, together with their canonical identification.

This is the reduced-center input for proving that the center of a semisimple affine group is finite. Semisimplicity trivializes the smooth connected identity component of this reduction; the finite component-group theorem then makes the reduction finite, after which nilpotence of the thickening controls the original center.

Main declarations #

References #

source
noncomputable def TauCeti.CommHopfAlgCat.reducedCenterDefiningIdeal {k : Type u} [Field k] (H : CommHopfAlgCat k) [IsReduced (TensorProduct k (↑(centerCoordinateHopfAlgebra H) ⧸ nilradical ↑(centerCoordinateHopfAlgebra H)) (↑(centerCoordinateHopfAlgebra H) ⧸ nilradical ↑(centerCoordinateHopfAlgebra H)))] :
HopfIdeal k ↑H

The Hopf ideal in the ambient coordinate algebra cutting out the reduced center.

It is the inverse image of the nilradical Hopf ideal of the center coordinate algebra.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.CommHopfAlgCat.centerDefiningIdeal_le_reducedCenterDefiningIdeal {k : Type u} [Field k] (H : CommHopfAlgCat k) [IsReduced (TensorProduct k (↑(centerCoordinateHopfAlgebra H) ⧸ nilradical ↑(centerCoordinateHopfAlgebra H)) (↑(centerCoordinateHopfAlgebra H) ⧸ nilradical ↑(centerCoordinateHopfAlgebra H)))] :
    centerDefiningIdeal H ≤ reducedCenterDefiningIdeal H

    The center ideal is contained in the reduced-center ideal. Contravariantly, the reduced center is a closed subgroup of the center.

    source
    theorem TauCeti.CommHopfAlgCat.isCentral_reducedCenterDefiningIdeal {k : Type u} [Field k] (H : CommHopfAlgCat k) [IsReduced (TensorProduct k (↑(centerCoordinateHopfAlgebra H) ⧸ nilradical ↑(centerCoordinateHopfAlgebra H)) (↑(centerCoordinateHopfAlgebra H) ⧸ nilradical ↑(centerCoordinateHopfAlgebra H)))] :
    (reducedCenterDefiningIdeal H).IsCentral

    The ideal defining the reduced center is central.

    source
    @[reducible, inline]
    noncomputable abbrev TauCeti.CommHopfAlgCat.reducedCenterCoordinateHopfAlgebra {k : Type u} [Field k] (H : CommHopfAlgCat k) [IsReduced (TensorProduct k (↑(centerCoordinateHopfAlgebra H) ⧸ nilradical ↑(centerCoordinateHopfAlgebra H)) (↑(centerCoordinateHopfAlgebra H) ⧸ nilradical ↑(centerCoordinateHopfAlgebra H)))] :
    CommHopfAlgCat k

    The coordinate Hopf algebra of the reduced center, formed by quotienting the center by its nilradical.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem TauCeti.CommHopfAlgCat.isReduced_reducedCenterCoordinateHopfAlgebra {k : Type u} [Field k] (H : CommHopfAlgCat k) [IsReduced (TensorProduct k (↑(centerCoordinateHopfAlgebra H) ⧸ nilradical ↑(centerCoordinateHopfAlgebra H)) (↑(centerCoordinateHopfAlgebra H) ⧸ nilradical ↑(centerCoordinateHopfAlgebra H)))] :
      IsReduced ↑(reducedCenterCoordinateHopfAlgebra H)

      The reduced-center coordinate algebra is reduced.

      source
      @[simp]
      theorem TauCeti.CommHopfAlgCat.reducedCenterDefiningIdeal_toIdeal {k : Type u} [Field k] (H : CommHopfAlgCat k) [IsReduced (TensorProduct k (↑(centerCoordinateHopfAlgebra H) ⧸ nilradical ↑(centerCoordinateHopfAlgebra H)) (↑(centerCoordinateHopfAlgebra H) ⧸ nilradical ↑(centerCoordinateHopfAlgebra H)))] :
      (reducedCenterDefiningIdeal H).toIdeal = (centerDefiningIdeal H).toIdeal.radical

      The ambient ideal defining the reduced center is the radical of the center ideal.

      source
      @[simp]
      theorem TauCeti.CommHopfAlgCat.mem_reducedCenterDefiningIdeal {k : Type u} [Field k] (H : CommHopfAlgCat k) [IsReduced (TensorProduct k (↑(centerCoordinateHopfAlgebra H) ⧸ nilradical ↑(centerCoordinateHopfAlgebra H)) (↑(centerCoordinateHopfAlgebra H) ⧸ nilradical ↑(centerCoordinateHopfAlgebra H)))] {x : ↑H} :
      x ∈ reducedCenterDefiningIdeal H ↔ x ∈ (centerDefiningIdeal H).toIdeal.radical

      An element belongs to the reduced-center ideal exactly when it belongs to the radical of the center ideal.

      source
      noncomputable def TauCeti.CommHopfAlgCat.quotientReducedCenterIso {k : Type u} [Field k] (H : CommHopfAlgCat k) [IsReduced (TensorProduct k (↑(centerCoordinateHopfAlgebra H) ⧸ nilradical ↑(centerCoordinateHopfAlgebra H)) (↑(centerCoordinateHopfAlgebra H) ⧸ nilradical ↑(centerCoordinateHopfAlgebra H)))] :
      quotient H (reducedCenterDefiningIdeal H) ≅ reducedCenterCoordinateHopfAlgebra H

      The quotient by the ambient reduced-center ideal is canonically the iterated quotient formed by taking the center and then killing its nilradical.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TauCeti.CommHopfAlgCat.mkQuotient_comp_quotientReducedCenterIso_hom {k : Type u} [Field k] (H : CommHopfAlgCat k) [IsReduced (TensorProduct k (↑(centerCoordinateHopfAlgebra H) ⧸ nilradical ↑(centerCoordinateHopfAlgebra H)) (↑(centerCoordinateHopfAlgebra H) ⧸ nilradical ↑(centerCoordinateHopfAlgebra H)))] :
        CategoryTheory.CategoryStruct.comp (mkQuotient H (reducedCenterDefiningIdeal H)) (quotientReducedCenterIso H).hom = CategoryTheory.CategoryStruct.comp (mkQuotient H (centerDefiningIdeal H)) (mkQuotient (centerCoordinateHopfAlgebra H) (HopfIdeal.reduction k ↑(centerCoordinateHopfAlgebra H)))

        The canonical reduced-center isomorphism commutes with the ambient and iterated quotient morphisms.

        source
        theorem TauCeti.CommHopfAlgCat.isReduced_quotient_reducedCenterDefiningIdeal {k : Type u} [Field k] (H : CommHopfAlgCat k) [IsReduced (TensorProduct k (↑(centerCoordinateHopfAlgebra H) ⧸ nilradical ↑(centerCoordinateHopfAlgebra H)) (↑(centerCoordinateHopfAlgebra H) ⧸ nilradical ↑(centerCoordinateHopfAlgebra H)))] :
        IsReduced ↑(quotient H (reducedCenterDefiningIdeal H))

        The ambient quotient model of the reduced center has reduced coordinate ring.

        source
        theorem TauCeti.CommHopfAlgCat.reducedCenterDefiningIdeal_le_of_centerDefiningIdeal_le_of_isReduced_quotient {k : Type u} [Field k] (H : CommHopfAlgCat k) [IsReduced (TensorProduct k (↑(centerCoordinateHopfAlgebra H) ⧸ nilradical ↑(centerCoordinateHopfAlgebra H)) (↑(centerCoordinateHopfAlgebra H) ⧸ nilradical ↑(centerCoordinateHopfAlgebra H)))] (I : HopfIdeal k ↑H) (hcenter : centerDefiningIdeal H ≤ I) [IsReduced ↑(quotient H I)] :
        reducedCenterDefiningIdeal H ≤ I

        The reduced-center ideal is contained in every central Hopf ideal whose quotient is reduced.

        source
        theorem TauCeti.CommHopfAlgCat.smooth_reducedCenterCoordinateHopfAlgebra {k : Type u} [Field k] (G : CommHopfAlgCat k) [IsReduced (TensorProduct k (↑(centerCoordinateHopfAlgebra G) ⧸ nilradical ↑(centerCoordinateHopfAlgebra G)) (↑(centerCoordinateHopfAlgebra G) ⧸ nilradical ↑(centerCoordinateHopfAlgebra G)))] [IsAlgClosed k] [Algebra.FiniteType k ↑(reducedCenterCoordinateHopfAlgebra G)] :
        Algebra.Smooth k ↑(reducedCenterCoordinateHopfAlgebra G)

        Over an algebraically closed field, a finite-type reduced center is smooth.