Affine group schemes of finite type

This file restricts the anti-equivalence between commutative Hopf algebras and affine group schemes to the finite-type objects. On the coordinate side, finite type means Algebra.FiniteType R H. On the scheme side, it means that the structural morphism G ⟶ Spec R is locally of finite type. Since the source and target are affine, this is the usual finite-type condition for an affine group scheme.

The key compatibility theorem is TauCeti.algebraFiniteType_iff_locallyOfFiniteType_hopfSpec: the coordinate algebra H is finitely generated over R exactly when the structural morphism of its Hopf spectrum is locally of finite type. Restricting the existing anti-equivalence along this equality gives

(FiniteTypeCommHopfAlgCat R)ᵒᵖ ≌ FiniteTypeAffineGroupSchemeCat (CommRingCat.of R).

Thus finite type remains a separate object property in both models, as required by the reductive-groups roadmap, while the dictionary records that the two predicates correspond.

Main declarations

• TauCeti.finiteTypeAffineGroupSchemeProperty: the locally-of-finite-type object property on affine group schemes over an affine base.
• TauCeti.FiniteTypeAffineGroupSchemeCat: the resulting full subcategory.
• TauCeti.algebraFiniteType_iff_locallyOfFiniteType_hopfSpec: compatibility of the algebraic and scheme-theoretic finite-type conditions.
• TauCeti.finiteTypeCommHopfAlgCatOpEquivFiniteTypeAffineGroupSchemeCat: the restricted anti-equivalence.
• TauCeti.finiteTypeCommHopfAlgCatOpEquivFiniteTypeAffineGroupSchemeCat.functorCompιIso: after both inclusions, the forward functor is Mathlib's AlgebraicGeometry.hopfSpec.
• TauCeti.finiteTypeCommHopfAlgCatOpEquivFiniteTypeAffineGroupSchemeCat.functorObjIso: the corresponding object-level isomorphism with the bundled Hopf spectrum.
• TauCeti.finiteType_objectProperty_iff_coordinate: transport of an isomorphism-invariant object property through the finite-type anti-equivalence.

References

The affine anti-equivalence is TauCeti.commHopfAlgCatOpEquivAffineGroupSchemeCat, assembled from Mathlib's AlgebraicGeometry.hopfSpec. The finite-type comparison uses Mathlib's AlgebraicGeometry.HasRingHomProperty.Spec_iff for locally finite-type morphisms and RingHom.finiteType_algebraMap. This is the finite-type predicate synchronization requested in Layer 0 of TauCetiRoadmap/ReductiveGroups/README.md.

def TauCeti.finiteTypeAffineGroupSchemeProperty (S : CommRingCat) : CategoryTheory.ObjectProperty (AffineGroupSchemeCat S)

The object property on affine group schemes over Spec S selecting those whose structural morphism is locally of finite type. Since both the group scheme and the base are affine, these are precisely the affine group schemes of finite type over S.

Equations

• TauCeti.finiteTypeAffineGroupSchemeProperty S G = AlgebraicGeometry.LocallyOfFiniteType G.obj.X.hom

@[simp]

theorem TauCeti.finiteTypeAffineGroupSchemeProperty_iff (S : CommRingCat) (G : AffineGroupSchemeCat S) : finiteTypeAffineGroupSchemeProperty S G ↔ AlgebraicGeometry.LocallyOfFiniteType G.obj.X.hom

Membership in the finite-type affine-group-scheme object property.

instance TauCeti.instIsClosedUnderIsomorphismsAffineGroupSchemeCatFiniteTypeAffineGroupSchemeProperty (S : CommRingCat) : (finiteTypeAffineGroupSchemeProperty S).IsClosedUnderIsomorphisms

Local finite type of the structural morphism is invariant under isomorphism of affine group schemes. This lets the predicate restrict equivalences to full subcategories.

@[reducible, inline]

abbrev TauCeti.FiniteTypeAffineGroupSchemeCat (S : CommRingCat) : Type (u + 1)

The category of affine group schemes of finite type over the affine base Spec S.

Finite type is kept as an object property rather than included in the definition of an affine group scheme.

Equations

• TauCeti.FiniteTypeAffineGroupSchemeCat S = (TauCeti.finiteTypeAffineGroupSchemeProperty S).FullSubcategory

instance TauCeti.instLocallyOfFiniteTypeHomSchemeXOverSpecObjGrpAffineGroupSchemePropertyAffineGroupSchemeCatFiniteTypeAffineGroupSchemeProperty {S : CommRingCat} (G : FiniteTypeAffineGroupSchemeCat S) : AlgebraicGeometry.LocallyOfFiniteType G.obj.obj.X.hom

An object of FiniteTypeAffineGroupSchemeCat S has a locally finite-type structural morphism by construction.

theorem TauCeti.algebraFiniteType_iff_locallyOfFiniteType_hopfSpec (R : Type u) [CommRing R] (H : CommHopfAlgCat R) : Algebra.FiniteType R ↑H ↔ AlgebraicGeometry.LocallyOfFiniteType ((AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H)).X.hom

A commutative Hopf algebra is finitely generated over its base exactly when the structural morphism of its Hopf spectrum is locally of finite type.

This is the predicate-level compatibility needed to restrict the affine Hopf/group-scheme anti-equivalence to finite-type objects.

theorem TauCeti.finiteTypeAffineGroupSchemeProperty_inverseImage (R : Type u) [CommRing R] : (finiteTypeAffineGroupSchemeProperty ↧R).inverseImage (commHopfAlgCatOpEquivAffineGroupSchemeCat ↧R).functor = (finiteTypeCommHopfAlgProperty R).op

Under the affine Hopf/group-scheme anti-equivalence, the inverse image of the finite-type scheme property is the finite-type coordinate-algebra property.

noncomputable def TauCeti.finiteTypeCommHopfAlgCatOpEquivFiniteTypeAffineGroupSchemeCat (R : Type u) [CommRing R] : (FiniteTypeCommHopfAlgCat R)ᵒᵖ ≌ FiniteTypeAffineGroupSchemeCat ↧R

Spec as an anti-equivalence from finite-type commutative R-Hopf algebras to affine group schemes of finite type over Spec R.

This is the restriction of commHopfAlgCatOpEquivAffineGroupSchemeCat along finiteTypeAffineGroupSchemeProperty_inverseImage.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.finiteTypeCommHopfAlgCatOpEquivFiniteTypeAffineGroupSchemeCat.functorCompιIso (R : Type u) [CommRing R] : (finiteTypeCommHopfAlgCatOpEquivFiniteTypeAffineGroupSchemeCat R).functor.comp ((finiteTypeAffineGroupSchemeProperty ↧R).ι.comp (affineGroupSchemeProperty ↧R).ι) ≅ (CategoryTheory.forget₂ (FiniteTypeCommHopfAlgCat R) (CommHopfAlgCat R)).op.comp (AlgebraicGeometry.hopfSpec ↧R)

The forward finite-type anti-equivalence, followed by the inclusions into affine group schemes and then all group schemes, is Mathlib's hopfSpec applied after forgetting the finite-type proof. This is the computation interface for the restricted equivalence.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.finiteTypeCommHopfAlgCatOpEquivFiniteTypeAffineGroupSchemeCat.functorObjIso (R : Type u) [CommRing R] (H : (FiniteTypeCommHopfAlgCat R)ᵒᵖ) : (finiteTypeCommHopfAlgCatOpEquivFiniteTypeAffineGroupSchemeCat R).functor.obj H ≅ { obj := { obj := (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op (Opposite.unop H).obj), property := ⋯ }, property := ⋯ }

The object produced by the finite-type Hopf/group-scheme anti-equivalence is the bundled finite-type Hopf spectrum.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.finiteType_objectProperty_iff_coordinate (R : Type u) [CommRing R] (P : CategoryTheory.ObjectProperty (AffineGroupSchemeCat ↧R)) [P.IsClosedUnderIsomorphisms] (Q : CategoryTheory.ObjectProperty (CommHopfAlgCat R)) (hPQ : P.inverseImage (commHopfAlgCatOpEquivAffineGroupSchemeCat ↧R).functor = Q.op) (G : FiniteTypeAffineGroupSchemeCat ↧R) : P G.obj ↔ Q (Opposite.unop ((finiteTypeCommHopfAlgCatOpEquivFiniteTypeAffineGroupSchemeCat R).inverse.obj G)).obj

An isomorphism-invariant property of affine group schemes can be tested on the coordinate Hopf algebra of a finite-type affine group scheme whenever the unrestricted anti-equivalence identifies it with a coordinate-side property.