Documentation

TauCeti.Algebra.AlgebraicGroup.Derived.Basic

The derived subgroup of an affine group scheme #

Let H be a commutative Hopf algebra, representing an affine group scheme G. The commutator morphism G × G ⟶ G need not be a group homomorphism, so its image is not directly represented by a quotient Hopf algebra. Instead, this file defines derivedDefiningIdeal H to be the largest Hopf ideal contained in the kernel of the commutator coordinate morphism

H ⟶ H ⊗[R] H.

The quotient by this ideal represents the smallest closed subgroup scheme of G containing the commutator image. Every algebra-valued commutator belongs to its subgroup of points. Consequently, a normal closed subgroup contains the derived subgroup exactly when all of its algebra-valued point-group quotients are commutative. If the coordinate Hopf algebra is cocommutative, the derived subgroup is trivial.

Main declarations #

References #

This supplies G_der, required in Layer 6 of the ReductiveGroups roadmap, and the scheme-theoretic derived subgroup left outstanding by the Layer 5 solvability development.

source
noncomputable def TauCeti.CommHopfAlgCat.derivedDefiningIdeal {R : Type u} [CommSemiring R] (H : Type v) [CommSemiring H] [HopfAlgebra R H] :
HopfIdeal R H

The largest Hopf ideal contained in the kernel of the commutator coordinate morphism.

Its quotient represents the smallest closed subgroup scheme containing the image of the commutator morphism.

Equations
Instances For
    source
    theorem TauCeti.CommHopfAlgCat.derivedDefiningIdeal_toIdeal_le_ker {R : Type u} [CommSemiring R] (H : Type v) [CommSemiring H] [HopfAlgebra R H] :
    (derivedDefiningIdeal H).toIdeal ≤ RingHom.ker HopfAlgebra.commutatorAlgHom.toRingHom

    The derived defining ideal is killed by the commutator coordinate morphism.

    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.le_derivedDefiningIdeal_iff {R : Type u} [CommSemiring R] (H : Type v) [CommSemiring H] [HopfAlgebra R H] (I : HopfIdeal R H) :
    I ≤ derivedDefiningIdeal H ↔ I.toIdeal ≤ RingHom.ker HopfAlgebra.commutatorAlgHom.toRingHom

    A Hopf ideal is contained in the derived defining ideal exactly when the commutator coordinate morphism kills it. This is the coordinate universal property of the derived subgroup.

    source
    @[reducible, inline]
    noncomputable abbrev TauCeti.CommHopfAlgCat.derivedGroupScheme {R : Type u} [CommRing R] (H : CommHopfAlgCat R) :
    CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))

    The affine group scheme represented by the coordinate algebra of the derived subgroup.

    Equations
    Instances For
      source
      @[reducible, inline]
      noncomputable abbrev TauCeti.CommHopfAlgCat.derivedGroupSchemeι {R : Type u} [CommRing R] (H : CommHopfAlgCat R) :
      derivedGroupScheme H ⟶ (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H)

      The closed immersion of the derived group scheme into the ambient Hopf spectrum.

      Equations
      Instances For
        source
        instance TauCeti.CommHopfAlgCat.isClosedImmersion_derivedGroupSchemeι {R : Type u} [CommRing R] (H : CommHopfAlgCat R) :
        AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (derivedGroupSchemeι H).hom.hom)

        The inclusion of the derived group scheme is a closed immersion.

        source
        theorem TauCeti.CommHopfAlgCat.commutator_mem_derivedPointsSubgroup {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (A : CommAlgCat R) (g h : ↑(HopfAlgebra.points A)) :
        ⁅g, h⁆ ∈ quotientPointsSubgroup H (derivedDefiningIdeal ↑H) A

        Every commutator of algebra-valued points lies in the derived subgroup.

        source
        theorem TauCeti.CommHopfAlgCat.commutator_le_quotientPointsSubgroup_of_le_derivedDefiningIdeal {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hID : I ≤ derivedDefiningIdeal ↑H) (A : CommAlgCat R) :
        commutator ↑(HopfAlgebra.points A) ≤ quotientPointsSubgroup H I A

        If a Hopf ideal is contained in the derived defining ideal, every pointwise commutator belongs to the subgroup it cuts out.

        source
        theorem TauCeti.CommHopfAlgCat.isNormal_of_le_derivedDefiningIdeal {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hID : I ≤ derivedDefiningIdeal ↑H) :
        I.IsNormal

        Every Hopf ideal contained in the derived defining ideal is normal.

        source
        theorem TauCeti.CommHopfAlgCat.isNormal_derivedDefiningIdeal {R : Type u} [CommRing R] (H : CommHopfAlgCat R) :
        (derivedDefiningIdeal ↑H).IsNormal

        The Hopf ideal defining the derived subgroup is normal.

        source
        theorem TauCeti.CommHopfAlgCat.isMulCommutative_pointQuotient_of_le_derivedDefiningIdeal {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hID : I ≤ derivedDefiningIdeal ↑H) (A : CommAlgCat R) :
        have x := ⋯; IsMulCommutative (↑(HopfAlgebra.points A) ⧸ quotientPointsSubgroup H I A)

        If a closed subgroup contains the derived subgroup, the corresponding quotient of every algebra-valued point group is commutative.

        source
        theorem TauCeti.CommHopfAlgCat.le_derivedDefiningIdeal_iff_isNormal_and_isMulCommutative_pointQuotient {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) :
        I ≤ derivedDefiningIdeal ↑H ↔ ∃ (hI : I.IsNormal), ∀ (A : CommAlgCat R), have x := ⋯; IsMulCommutative (↑(HopfAlgebra.points A) ⧸ quotientPointsSubgroup H I A)

        A closed subgroup contains the derived subgroup exactly when it is normal and all of the corresponding point-group quotients are commutative. The converse needs no point-separation or rational-point hypothesis.

        source
        @[simp]
        theorem TauCeti.CommHopfAlgCat.derivedDefiningIdeal_eq_augmentation_iff_isCocomm {R : Type u} [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] :
        derivedDefiningIdeal H = HopfIdeal.augmentation R H ↔ Coalgebra.IsCocomm R H

        The derived subgroup of a commutative affine group is trivial exactly when the coordinate Hopf algebra is cocommutative.