Documentation

TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Scheme.Classification

Closed subgroup schemes and Hopf ideals #

For a commutative Hopf algebra H over a commutative ring R, this file classifies the closed subgroup subobjects of the affine group scheme Spec H. A closed subgroup scheme is an ordinary categorical subobject whose representative arrow is a closed immersion on underlying schemes. The closed-immersion condition is pulled back through the forgetful functors, so it is independent of the representative chosen for the subobject.

A Hopf ideal I determines the closed subgroup Spec (H ⧸ I) ⟶ Spec H. Inclusion of Hopf ideals reverses inclusion of closed subgroup schemes, and every closed subgroup arises in this way. The classification is therefore packaged as an order isomorphism from the order dual of the Hopf ideals of H.

Main declarations #

References #

The references state the classical correspondence. The proof here works over an arbitrary commutative base ring and uses categorical subobjects to identify isomorphic presentations.

source
noncomputable def TauCeti.CommHopfAlgCat.quotientClosedSubgroup {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) :
ClosedSubgroupScheme ((AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H))

The closed subgroup scheme of Spec H cut out by the Hopf ideal I.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.quotientClosedSubgroup_coe {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) :
    ↑(quotientClosedSubgroup H I) = CategoryTheory.Subobject.mk (quotientSpecι H I)

    The subobject underlying quotientClosedSubgroup is represented by the quotient closed immersion Spec (H ⧸ I) ⟶ Spec H.

    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.quotientClosedSubgroup_le_iff {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {I J : HopfIdeal R ↑H} :
    quotientClosedSubgroup H I ≤ quotientClosedSubgroup H J ↔ J ≤ I

    Inclusion of quotient closed subgroup schemes is exactly reverse inclusion of their defining Hopf ideals.

    source
    noncomputable def TauCeti.CommHopfAlgCat.hopfIdealOrderIsoClosedSubgroup {R : Type u} [CommRing R] (H : CommHopfAlgCat R) :
    (HopfIdeal R ↑H)ᵒᵈ ≃o ClosedSubgroupScheme ((AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H))

    Hopf ideals of H, ordered by reverse inclusion, are order-isomorphic to the closed subgroup schemes of Spec H.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.CommHopfAlgCat.hopfIdealOrderIsoClosedSubgroup_apply {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : (HopfIdeal R ↑H)ᵒᵈ) :
      (hopfIdealOrderIsoClosedSubgroup H) I = quotientClosedSubgroup H (OrderDual.ofDual I)

      The forward direction of the closed-subgroup classification sends a Hopf ideal to its quotient closed subgroup scheme.

      source
      @[simp]
      theorem TauCeti.CommHopfAlgCat.hopfIdealOrderIsoClosedSubgroup_apply_symm_apply {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (P : ClosedSubgroupScheme ((AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H))) :
      quotientClosedSubgroup H (OrderDual.ofDual ((hopfIdealOrderIsoClosedSubgroup H).symm P)) = P

      Every closed subgroup scheme is the quotient closed subgroup cut out by the Hopf ideal recovered by the inverse classification.

      source
      @[simp]
      theorem TauCeti.CommHopfAlgCat.hopfIdealOrderIsoClosedSubgroup_symm_apply_quotientClosedSubgroup {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) :
      (hopfIdealOrderIsoClosedSubgroup H).symm (quotientClosedSubgroup H I) = OrderDual.toDual I

      Applying the inverse classification to a quotient closed subgroup recovers its defining Hopf ideal.

      source
      theorem TauCeti.CommHopfAlgCat.hopfIdealOrderIsoClosedSubgroup_symm_apply_eq_ker {R : Type u} [CommRing R] (H K : CommHopfAlgCat R) (P : ClosedSubgroupScheme ((AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H))) (e : (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op K) ≅ CategoryTheory.Subobject.underlying.obj ↑P) (f : H ⟶ K) (hf : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)) (hmap_f : (AlgebraicGeometry.hopfSpec ↧R).map f.op = CategoryTheory.CategoryStruct.comp e.hom (↑P).arrow) :
      (hopfIdealOrderIsoClosedSubgroup H).symm P = OrderDual.toDual (HopfIdeal.kerOfSurjective (CommHopfAlgCat.Hom.hom f) hf)

      Given an explicit affine presentation of a closed subgroup scheme, the inverse classification recovers the Hopf ideal that is the kernel of its surjective coordinate morphism.

      source
      theorem TauCeti.CommHopfAlgCat.quotientClosedSubgroup_factors_hopfSpec_map_iff {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (J : HopfIdeal R ↑H) (f : H ⟶ K) :
      (↑(quotientClosedSubgroup H J)).Factors ((AlgebraicGeometry.hopfSpec ↧R).map f.op) ↔ J.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom f)).toRingHom

      A quotient closed subgroup contains a represented affine group morphism exactly when its defining Hopf ideal is killed by the corresponding coordinate morphism.

      source
      theorem TauCeti.CommHopfAlgCat.quotientClosedSubgroup_commonKernel_le_iff {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {ι : Type u_1} {K : ι → CommHopfAlgCat R} (f : (i : ι) → H ⟶ K i) (P : ClosedSubgroupScheme ((AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H))) :
      quotientClosedSubgroup H (commonKernelHopfIdeal f) ≤ P ↔ ∀ (i : ι), (↑P).Factors ((AlgebraicGeometry.hopfSpec ↧R).map (f i).op)

      The quotient closed subgroup cut out by a common-kernel Hopf ideal is the smallest closed subgroup through which every represented member of the family factors.

      source
      theorem TauCeti.CommHopfAlgCat.mk_quotientSpecMapOfLe_eq_quotientClosedSubgroup {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {I J : HopfIdeal R ↑H} (hIJ : I ≤ J) :
      ClosedSubgroupScheme.mk (quotientSpecMapOfLe H hIJ) = quotientClosedSubgroup (quotient H I) (HopfIdeal.kerOfSurjective (CommHopfAlgCat.Hom.hom (quotientMapOfLe H hIJ)) ⋯)

      The closed subgroup represented by a quotient-to-quotient map is the quotient closed subgroup cut out by the kernel of that map.