Closed subgroup schemes from Hopf ideals

A Hopf ideal I in a commutative Hopf algebra H determines a quotient commutative Hopf algebra H ⧸ I. Applying relative spectrum contravariantly to the quotient morphism gives a morphism of group objects

Spec(H ⧸ I) ⟶ Spec(H)

over Spec R. Its underlying morphism of schemes is a closed immersion because the coordinate map is surjective. Thus the construction retains the scheme structure cut out by I, rather than only the induced inclusion on ordinary points.

If I ≤ J, the quotient-to-quotient coordinate map H ⧸ I ⟶ H ⧸ J gives a closed immersion Spec(H ⧸ J) ⟶ Spec(H ⧸ I). The ambient triangle, identity, and composition laws below record that these closed subgroup schemes depend contravariantly on the Hopf ideal. For a finite-type coordinate Hopf algebra, the quotient group scheme remains locally of finite type over the base.

The pinned affine-group-scheme bridge requires the base ring and the Hopf-algebra carrier to lie in the same universe, which is reflected in all scheme-level declarations in this file.

Main declarations

• TauCeti.CommHopfAlgCat.quotientSpec: the group scheme represented by H ⧸ I.
• TauCeti.CommHopfAlgCat.isAffine_quotientSpec: its underlying scheme is affine.
• TauCeti.CommHopfAlgCat.quotientSpecι: its group-object morphism to the group scheme represented by H.
• TauCeti.CommHopfAlgCat.isClosedImmersion_quotientSpecι: the underlying scheme morphism of quotientSpecι is a closed immersion.
• TauCeti.CommHopfAlgCat.quotientSpecMapOfLe: the closed subgroup morphism induced by I ≤ J.
• TauCeti.FiniteTypeCommHopfAlgCat.locallyOfFiniteType_quotientSpec: a finite-type Hopf algebra has quotient group schemes locally of finite type over Spec R.

References

Milne, Algebraic Groups, Definition 3.10 and Propositions 3.12 and 3.15, describes Hopf-ideal quotients and their relation to closed subgroup schemes over a field. The forward construction used here works over an arbitrary commutative ring and is supplied by Tau Ceti's quotient Hopf algebra API together with Mathlib's affine Spec and closed-immersion APIs.

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.quotientSpec {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec (CommRingCat.of R)))

The affine group scheme represented by the quotient Hopf algebra H ⧸ I.

The same-universe restriction on H is imposed by Mathlib's current hopfSpec construction.

Equations

• TauCeti.CommHopfAlgCat.quotientSpec H I = (AlgebraicGeometry.hopfSpec (CommRingCat.of R)).obj (Opposite.op (TauCeti.CommHopfAlgCat.quotient H I))

instance TauCeti.CommHopfAlgCat.isAffine_quotientSpec {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) : AlgebraicGeometry.IsAffine (quotientSpec H I).X.left

The scheme underlying a Hopf-ideal quotient group scheme is affine: it is the spectrum of the quotient Hopf algebra.

noncomputable def TauCeti.CommHopfAlgCat.quotientSpecι {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) : quotientSpec H I ⟶ (AlgebraicGeometry.hopfSpec (CommRingCat.of R)).obj (Opposite.op H)

The group-object morphism Spec(H ⧸ I) ⟶ Spec(H) induced contravariantly by the quotient Hopf-algebra morphism H ⟶ H ⧸ I.

Equations

• TauCeti.CommHopfAlgCat.quotientSpecι H I = (AlgebraicGeometry.hopfSpec (CommRingCat.of R)).map (TauCeti.CommHopfAlgCat.mkQuotient H I).op

theorem TauCeti.CommHopfAlgCat.quotientSpecι_def {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) : quotientSpecι H I = (AlgebraicGeometry.hopfSpec (CommRingCat.of R)).map (mkQuotient H I).op

quotientSpecι is the image under hopfSpec of the opposite quotient morphism.

instance TauCeti.CommHopfAlgCat.isClosedImmersion_quotientSpecι {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (quotientSpecι H I).hom.hom)

The underlying scheme morphism of quotientSpecι is a closed immersion. Thus the quotient Hopf algebra defines a closed subgroup scheme of the affine group scheme represented by H.

noncomputable def TauCeti.CommHopfAlgCat.quotientSpecMapOfLe {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {I J : HopfIdeal R ↑H} (hIJ : I ≤ J) : quotientSpec H J ⟶ quotientSpec H I

If I ≤ J, the quotient coordinate map H ⧸ I ⟶ H ⧸ J induces the group-object morphism Spec(H ⧸ J) ⟶ Spec(H ⧸ I).

Equations

• TauCeti.CommHopfAlgCat.quotientSpecMapOfLe H hIJ = (AlgebraicGeometry.hopfSpec (CommRingCat.of R)).map (TauCeti.CommHopfAlgCat.quotientMapOfLe H hIJ).op

theorem TauCeti.CommHopfAlgCat.quotientSpecMapOfLe_def {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {I J : HopfIdeal R ↑H} (hIJ : I ≤ J) : quotientSpecMapOfLe H hIJ = (AlgebraicGeometry.hopfSpec (CommRingCat.of R)).map (quotientMapOfLe H hIJ).op

quotientSpecMapOfLe is the image under hopfSpec of the opposite quotient-to-quotient morphism.

instance TauCeti.CommHopfAlgCat.isClosedImmersion_quotientSpecMapOfLe {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {I J : HopfIdeal R ↑H} (hIJ : I ≤ J) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (quotientSpecMapOfLe H hIJ).hom.hom)

The scheme morphism underlying quotientSpecMapOfLe is a closed immersion. In particular, a larger Hopf ideal defines a closed subgroup scheme of the subgroup defined by a smaller one.

@[simp]

theorem TauCeti.CommHopfAlgCat.quotientSpecMapOfLe_comp_quotientSpecι {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {I J : HopfIdeal R ↑H} (hIJ : I ≤ J) : CategoryTheory.CategoryStruct.comp (quotientSpecMapOfLe H hIJ) (quotientSpecι H I) = quotientSpecι H J

The inclusion associated to I ≤ J, followed by the inclusion into the ambient group scheme, is the inclusion associated to J.

@[simp]

theorem TauCeti.CommHopfAlgCat.quotientSpecMapOfLe_refl {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) : quotientSpecMapOfLe H ⋯ = CategoryTheory.CategoryStruct.id (quotientSpec H I)

The group-scheme inclusion induced by the reflexive inclusion I ≤ I is the identity.

@[simp]

theorem TauCeti.CommHopfAlgCat.quotientSpecMapOfLe_comp {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {I J K : HopfIdeal R ↑H} (hIJ : I ≤ J) (hJK : J ≤ K) : CategoryTheory.CategoryStruct.comp (quotientSpecMapOfLe H hJK) (quotientSpecMapOfLe H hIJ) = quotientSpecMapOfLe H ⋯

Closed subgroup morphisms compose contravariantly along inclusions I ≤ J ≤ K.

instance TauCeti.FiniteTypeCommHopfAlgCat.locallyOfFiniteType_quotientSpec {R : Type u} [CommRing R] (H : FiniteTypeCommHopfAlgCat R) (I : HopfIdeal R ↑H.obj) : AlgebraicGeometry.LocallyOfFiniteType (CommHopfAlgCat.quotientSpec H.obj I).X.hom

If H is a finite-type commutative Hopf algebra, then the group scheme represented by H ⧸ I is locally of finite type over Spec R. No finite-generation hypothesis on I is needed.