Affine finite-flat commutative group schemes

This file gives the affine coordinate-algebra side of finite-flat commutative group schemes. An affine commutative group scheme over Spec R is encoded contravariantly by a commutative, cocommutative Hopf R-algebra. The crucial bridge is not merely an equality of underlying sets: pointMulEquiv identifies morphisms Spec B ⟶ Spec A over Spec R with the convolution group of R-algebra maps A →ₐ[R] B.

The theorem AffineFiniteFreeCommGroupScheme.point_pow_order_eq_one transports the integrated AINTLIB theorem deligne_point_pow_eq_one across this geometric equivalence. The constant-rank finite-locally-free version is then obtained by localization at every maximal ideal and descent.

Scalar extension is functorial on the Hopf presentation, compatible with convolution-valued affine points, compatible with local rank, and compatible with geometric pullback as an isomorphism of internal commutative group objects.

def AlgebraicGeometry.cocommutativeHopfProperty (R : Type u) [CommRing R] : CategoryTheory.ObjectProperty (CommHopfAlgCat R)

Cocommutative objects in the category of commutative Hopf algebras over R.

Equations

• AlgebraicGeometry.cocommutativeHopfProperty R A = Coalgebra.IsCocomm R ↑A

@[reducible, inline]

abbrev AlgebraicGeometry.AffineCommGroupScheme (R : Type u) [CommRing R] : Type (u + 1)

Affine commutative group schemes over Spec R, encoded contravariantly by their commutative, cocommutative coordinate Hopf algebras.

Equations

• AlgebraicGeometry.AffineCommGroupScheme R = (AlgebraicGeometry.cocommutativeHopfProperty R).FullSubcategoryᵒᵖ

@[reducible, inline]

abbrev AlgebraicGeometry.AffineCommGroupScheme.coordinates {R : Type u} [CommRing R] (G : AffineCommGroupScheme R) : CommHopfAlgCat R

The coordinate Hopf algebra of an affine commutative group scheme.

Equations

• G.coordinates = (Opposite.unop G).obj

instance AlgebraicGeometry.AffineCommGroupScheme.instIsCocommXCoordinates {R : Type u} [CommRing R] (G : AffineCommGroupScheme R) : Coalgebra.IsCocomm R ↑G.coordinates

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.AffineCommGroupScheme.relativeSpecFunctor (R : Type u) [CommRing R] : CategoryTheory.Functor (CommAlgCat R)ᵒᵖ (CategoryTheory.Over (Spec (CommRingCat.of R)))

Relative affine spectrum, from commutative R-algebras to schemes over Spec R.

Equations

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

instance AlgebraicGeometry.AffineCommGroupScheme.instPreservesFiniteProductsOppositeCommAlgCatOverSchemeSpecOfRelativeSpecFunctor {R : Type u} [CommRing R] : CategoryTheory.Limits.PreservesFiniteProducts (relativeSpecFunctor R)

noncomputable def AlgebraicGeometry.AffineCommGroupScheme.relativeSpecFullyFaithful {R : Type u} [CommRing R] : (relativeSpecFunctor R).FullyFaithful

Relative affine spectrum is fully faithful.

Equations

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

@[instance_reducible]

noncomputable instance AlgebraicGeometry.AffineCommGroupScheme.instBraidedOppositeCommAlgCatOverSchemeSpecOfRelativeSpecFunctor {R : Type u} [CommRing R] : (relativeSpecFunctor R).Braided

Equations

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

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.AffineCommGroupScheme.coordinateCommGroup {R : Type u} [CommRing R] (A : CommHopfAlgCat R) [Coalgebra.IsCocomm R ↑A] : CategoryTheory.CommGrp (CommAlgCat R)ᵒᵖ

A commutative, cocommutative Hopf algebra as a commutative group object in the opposite category of commutative algebras. Its multiplication on points is convolution.

Equations

• AlgebraicGeometry.AffineCommGroupScheme.coordinateCommGroup A = { X := Opposite.op (CommAlgCat.of R ↑A), grp := CommAlgCat.grpObjOpOf, comm := ⋯ }

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.AffineCommGroupScheme.scheme {R : Type u} [CommRing R] (G : AffineCommGroupScheme R) : Scheme

The underlying affine scheme.

Equations

• G.scheme = AlgebraicGeometry.Spec (CommRingCat.of ↑G.coordinates)

noncomputable def AlgebraicGeometry.AffineCommGroupScheme.structureMap {R : Type u} [CommRing R] (G : AffineCommGroupScheme R) : G.scheme ⟶ Spec (CommRingCat.of R)

The structure morphism to Spec R.

Equations

• G.structureMap = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R ↑G.coordinates))

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.AffineCommGroupScheme.toCommGroupScheme {R : Type u} [CommRing R] (G : AffineCommGroupScheme R) : CommGroupScheme (Spec (CommRingCat.of R))

The geometric commutative group scheme constructed from the coordinate Hopf algebra.

Equations

• G.toCommGroupScheme = (AlgebraicGeometry.AffineCommGroupScheme.relativeSpecFunctor R).mapCommGrp.obj (AlgebraicGeometry.AffineCommGroupScheme.coordinateCommGroup G.coordinates)

@[simp]

theorem AlgebraicGeometry.AffineCommGroupScheme.toCommGroupScheme_X_left {R : Type u} [CommRing R] (G : AffineCommGroupScheme R) : G.toCommGroupScheme.X.left = G.scheme

@[simp]

theorem AlgebraicGeometry.AffineCommGroupScheme.toCommGroupScheme_X_hom {R : Type u} [CommRing R] (G : AffineCommGroupScheme R) : G.toCommGroupScheme.X.hom = G.structureMap

@[reducible, inline]

abbrev AlgebraicGeometry.AffineCommGroupScheme.coordinateMap {R : Type u} [CommRing R] {G H : AffineCommGroupScheme R} (f : G ⟶ H) : ↑H.coordinates →ₐc[R] ↑G.coordinates

The contravariant coordinate map associated to a morphism of affine group schemes.

Equations

• AlgebraicGeometry.AffineCommGroupScheme.coordinateMap f = CommHopfAlgCat.Hom.hom f.unop.hom

noncomputable def AlgebraicGeometry.AffineCommGroupScheme.schemeMap {R : Type u} [CommRing R] {G H : AffineCommGroupScheme R} (f : G ⟶ H) : G.scheme ⟶ H.scheme

The underlying morphism of affine schemes.

Equations

• AlgebraicGeometry.AffineCommGroupScheme.schemeMap f = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (↑(AlgebraicGeometry.AffineCommGroupScheme.coordinateMap f)).toRingHom)

@[simp]

theorem AlgebraicGeometry.AffineCommGroupScheme.schemeMap_id {R : Type u} [CommRing R] (G : AffineCommGroupScheme R) : schemeMap (CategoryTheory.CategoryStruct.id G) = CategoryTheory.CategoryStruct.id G.scheme

@[simp]

theorem AlgebraicGeometry.AffineCommGroupScheme.schemeMap_comp {R : Type u} [CommRing R] {G H K : AffineCommGroupScheme R} (f : G ⟶ H) (g : H ⟶ K) : schemeMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (schemeMap f) (schemeMap g)

@[simp]

theorem AlgebraicGeometry.AffineCommGroupScheme.schemeMap_comp_structureMap {R : Type u} [CommRing R] {G H : AffineCommGroupScheme R} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (schemeMap f) H.structureMap = G.structureMap

@[simp]

theorem AlgebraicGeometry.AffineCommGroupScheme.schemeMap_comp_structureMap_assoc {R : Type u} [CommRing R] {G H : AffineCommGroupScheme R} (f : G ⟶ H) {Z : Scheme} (h : Spec (CommRingCat.of R) ⟶ Z) : CategoryTheory.CategoryStruct.comp (schemeMap f) (CategoryTheory.CategoryStruct.comp H.structureMap h) = CategoryTheory.CategoryStruct.comp G.structureMap h

noncomputable def AlgebraicGeometry.AffineCommGroupScheme.coordinateCommGroupFunctor (R : Type u) [CommRing R] : CategoryTheory.Functor (AffineCommGroupScheme R) (CategoryTheory.CommGrp (CommAlgCat R)ᵒᵖ)

Contravariant Hopf morphisms as morphisms of commutative group objects in opposite commutative algebras.

Equations

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

noncomputable def AlgebraicGeometry.AffineCommGroupScheme.realizationFunctor (R : Type u) [CommRing R] : CategoryTheory.Functor (AffineCommGroupScheme R) (CommGroupScheme (Spec (CommRingCat.of R)))

Geometric realization of affine commutative group schemes, functorial in Hopf morphisms.

Equations

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

@[simp]

theorem AlgebraicGeometry.AffineCommGroupScheme.realizationFunctor_obj {R : Type u} [CommRing R] (G : AffineCommGroupScheme R) : (realizationFunctor R).obj G = G.toCommGroupScheme

@[simp]

theorem AlgebraicGeometry.AffineCommGroupScheme.realizationFunctor_map_left {R : Type u} [CommRing R] {G H : AffineCommGroupScheme R} (f : G ⟶ H) : CategoryTheory.Over.Hom.left ((realizationFunctor R).map f).hom.hom.hom = schemeMap f

def AlgebraicGeometry.AffineCommGroupScheme.isoOfCoordinateBialgEquiv {R : Type u} [CommRing R] {G H : AffineCommGroupScheme R} (e : ↑G.coordinates ≃ₐc[R] ↑H.coordinates) : G ≅ H

A bialgebra equivalence of coordinate Hopf algebras induces an isomorphism of affine commutative group schemes. The apparent reversal is handled by the opposite category in the Hopf-algebra dictionary.

Equations

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

@[simp]

theorem AlgebraicGeometry.AffineCommGroupScheme.coordinateMap_isoOfCoordinateBialgEquiv_hom {R : Type u} [CommRing R] {G H : AffineCommGroupScheme R} (e : ↑G.coordinates ≃ₐc[R] ↑H.coordinates) : coordinateMap (isoOfCoordinateBialgEquiv e).hom = ↑e.symm

@[simp]

theorem AlgebraicGeometry.AffineCommGroupScheme.coordinateMap_isoOfCoordinateBialgEquiv_inv {R : Type u} [CommRing R] {G H : AffineCommGroupScheme R} (e : ↑G.coordinates ≃ₐc[R] ↑H.coordinates) : coordinateMap (isoOfCoordinateBialgEquiv e).inv = ↑e

noncomputable def AlgebraicGeometry.AffineCommGroupScheme.baseChangeFunctor {R : Type u} [CommRing R] {K : Type u} [CommRing K] [Algebra R K] : CategoryTheory.Functor (AffineCommGroupScheme R) (AffineCommGroupScheme K)

Scalar extension of affine commutative group schemes, functorial in Hopf morphisms.

Equations

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

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.AffineCommGroupScheme.baseChange {R : Type u} [CommRing R] {K : Type u} [CommRing K] [Algebra R K] (G : AffineCommGroupScheme R) : AffineCommGroupScheme K

Scalar extension of one affine commutative group scheme.

Equations

• G.baseChange = AlgebraicGeometry.AffineCommGroupScheme.baseChangeFunctor.obj G

@[simp]

theorem AlgebraicGeometry.AffineCommGroupScheme.baseChange_coordinates {R : Type u} [CommRing R] {K : Type u} [CommRing K] [Algebra R K] (G : AffineCommGroupScheme R) : ↑G.baseChange.coordinates = TensorProduct R K ↑G.coordinates

@[simp]

theorem AlgebraicGeometry.AffineCommGroupScheme.baseChange_coordinateMap {R : Type u} [CommRing R] {K : Type u} [CommRing K] [Algebra R K] {G H : AffineCommGroupScheme R} (f : G ⟶ H) : coordinateMap (baseChangeFunctor.map f) = CommHopfAlgCat.Hom.hom (TauCeti.CommHopfAlgCat.baseChangeMap f.unop.hom)

noncomputable def AlgebraicGeometry.AffineCommGroupScheme.baseChangeSchemeIso {k K : Type u} [CommRing k] [CommRing K] [Algebra k K] (G : AffineCommGroupScheme k) : CategoryTheory.Limits.pullback G.structureMap (Spec.map (CommRingCat.ofHom (algebraMap k K))) ≅ G.baseChange.scheme

The affine spectrum of scalar-extended Hopf coordinates is canonically the geometric pullback of the original affine spectrum.

Equations

• G.baseChangeSchemeIso = AlgebraicGeometry.AffineCommGroupScheme.baseChangeUnderlyingSchemeIso✝ G.coordinates

noncomputable def AlgebraicGeometry.AffineCommGroupScheme.realizationBaseChangeIso {k K : Type u} [CommRing k] [CommRing K] [Algebra k K] (G : AffineCommGroupScheme k) : (CategoryTheory.Over.pullback (Spec.map (CommRingCat.ofHom (algebraMap k K)))).mapCommGrp.obj G.toCommGroupScheme ≅ G.baseChange.toCommGroupScheme

Scalar extension on affine Hopf coordinates agrees with geometric base change as an isomorphism of internal commutative group schemes, not just as an isomorphism of schemes.

Equations

• G.realizationBaseChangeIso = AlgebraicGeometry.AffineCommGroupScheme.baseChangeCommGroupIso✝ G.coordinates

theorem AlgebraicGeometry.AffineCommGroupScheme.realizationBaseChangeIso_naturality {k K : Type u} [CommRing k] [CommRing K] [Algebra k K] {G H : AffineCommGroupScheme k} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.pullback (Spec.map (CommRingCat.ofHom (algebraMap k K)))).mapCommGrp.map ((realizationFunctor k).map f)) H.realizationBaseChangeIso.hom = CategoryTheory.CategoryStruct.comp G.realizationBaseChangeIso.hom ((realizationFunctor K).map (baseChangeFunctor.map f))

Geometric realization commutes naturally with scalar extension on affine Hopf presentations.

noncomputable def AlgebraicGeometry.AffineCommGroupScheme.testObject {R : Type u} [CommRing R] (B : Type u) [CommRing B] [Algebra R B] : CategoryTheory.Over (Spec (CommRingCat.of R))

Spec B as an object over Spec R.

Equations

• AlgebraicGeometry.AffineCommGroupScheme.testObject B = CategoryTheory.Over.mk (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R B)))

noncomputable def AlgebraicGeometry.AffineCommGroupScheme.testObjectMap {R : Type u} [CommRing R] {A B : Type u} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) : testObject B ⟶ testObject A

An algebra map induces the corresponding contravariant morphism of affine test objects.

Equations

• AlgebraicGeometry.AffineCommGroupScheme.testObjectMap f = CategoryTheory.Over.homMk (AlgebraicGeometry.Spec.map (CommRingCat.ofHom f.toRingHom)) ⋯

noncomputable def AlgebraicGeometry.AffineCommGroupScheme.baseIsoSelfTestObject (R : Type u) [CommRing R] : CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id (Spec (CommRingCat.of R))) ≅ testObject R

The identity object over Spec R is canonically the affine self-test object. Keeping this at the affine interface avoids rebuilding the same comparison in each global-section calculation.

Equations

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

@[reducible, inline]

abbrev AlgebraicGeometry.AffineCommGroupScheme.Point {R : Type u} [CommRing R] (G : AffineCommGroupScheme R) (B : Type u) [CommRing B] [Algebra R B] : Type u

The affine test-scheme points of G, expressed geometrically as morphisms over Spec R.

Equations

• G.Point B = (AlgebraicGeometry.AffineCommGroupScheme.testObject B ⟶ G.toCommGroupScheme.X)

@[instance_reducible]

noncomputable instance AlgebraicGeometry.AffineCommGroupScheme.pointCommGroup {R : Type u} [CommRing R] (G : AffineCommGroupScheme R) (B : Type u) [CommRing B] [Algebra R B] : CommGroup (G.Point B)

Affine points carry the canonical group law induced by the constructed internal group scheme. This globally exposes the same instance that is otherwise available only in the CategoryTheory.MonObj scope.

Equations

• G.pointCommGroup B = CategoryTheory.Hom.commGroup

noncomputable def AlgebraicGeometry.AffineCommGroupScheme.pointToAlgHom {R : Type u} [CommRing R] (G : AffineCommGroupScheme R) (B : Type u) [CommRing B] [Algebra R B] (x : G.Point B) : ↑G.coordinates →ₐ[R] B

Recover the coordinate R-algebra map from a geometric affine point.

Equations

• G.pointToAlgHom B x = { toRingHom := CommRingCat.Hom.hom (AlgebraicGeometry.Spec.preimage (CategoryTheory.Over.Hom.left x)), commutes' := ⋯ }

theorem AlgebraicGeometry.AffineCommGroupScheme.pointToAlgHom_testObjectMap {R : Type u} [CommRing R] {A B : Type u} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (G : AffineCommGroupScheme R) (f : A →ₐ[R] B) (x : G.Point A) : G.pointToAlgHom B (CategoryTheory.CategoryStruct.comp (testObjectMap f) x) = f.comp (G.pointToAlgHom A x)

Reading coordinates commutes with restriction along a morphism of affine test objects.

noncomputable def AlgebraicGeometry.AffineCommGroupScheme.pointOfAlgHom {R : Type u} [CommRing R] (G : AffineCommGroupScheme R) (B : Type u) [CommRing B] [Algebra R B] (f : ↑G.coordinates →ₐ[R] B) : G.Point B

Turn a coordinate R-algebra map into a morphism of affine schemes over Spec R.

Equations

• G.pointOfAlgHom B f = id (CategoryTheory.Over.homMk (AlgebraicGeometry.Spec.map (CommRingCat.ofHom f.toRingHom)) ⋯)

noncomputable def AlgebraicGeometry.AffineCommGroupScheme.pointEquiv {R : Type u} [CommRing R] (G : AffineCommGroupScheme R) (B : Type u) [CommRing B] [Algebra R B] : G.Point B ≃ WithConv (↑G.coordinates →ₐ[R] B)

Geometric affine points are exactly coordinate-algebra maps.

Equations

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

noncomputable def AlgebraicGeometry.AffineCommGroupScheme.coordinatePointEquiv {R : Type u} [CommRing R] (A : CommHopfAlgCat R) [Coalgebra.IsCocomm R ↑A] (B : Type u) [CommRing B] [Algebra R B] : (Opposite.op (CommAlgCat.of R B) ⟶ (coordinateCommGroup A).X) ≃ WithConv (↑A →ₐ[R] B)

Algebra maps out of a Hopf algebra are the points of its opposite-algebra group object.

Equations

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

noncomputable def AlgebraicGeometry.AffineCommGroupScheme.coordinatePointMulEquiv {R : Type u} [CommRing R] (A : CommHopfAlgCat R) [Coalgebra.IsCocomm R ↑A] (B : Type u) [CommRing B] [Algebra R B] : (Opposite.op (CommAlgCat.of R B) ⟶ (coordinateCommGroup A).X) ≃* WithConv (↑A →ₐ[R] B)

The preceding point equivalence respects the actual internal group law and convolution.

Equations

• AlgebraicGeometry.AffineCommGroupScheme.coordinatePointMulEquiv A B = { toEquiv := AlgebraicGeometry.AffineCommGroupScheme.coordinatePointEquiv A B, map_mul' := ⋯ }

noncomputable def AlgebraicGeometry.AffineCommGroupScheme.relativeSpecPointMulEquiv {R : Type u} [CommRing R] (A : CommHopfAlgCat R) [Coalgebra.IsCocomm R ↑A] (B : Type u) [CommRing B] [Algebra R B] : (Opposite.op (CommAlgCat.of R B) ⟶ (coordinateCommGroup A).X) ≃* (testObject B ⟶ ((relativeSpecFunctor R).mapCommGrp.obj (coordinateCommGroup A)).X)

Full faithfulness of relative spectrum respects multiplication on group-valued hom-sets.

Equations

• AlgebraicGeometry.AffineCommGroupScheme.relativeSpecPointMulEquiv A B = { toEquiv := AlgebraicGeometry.AffineCommGroupScheme.relativeSpecFullyFaithful.homEquiv, map_mul' := ⋯ }

noncomputable def AlgebraicGeometry.AffineCommGroupScheme.pointMulEquiv {R : Type u} [CommRing R] (G : AffineCommGroupScheme R) (B : Type u) [CommRing B] [Algebra R B] : G.Point B ≃* WithConv (↑G.coordinates →ₐ[R] B)

The affine point equivalence respects the geometric group law and convolution.

Equations

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

@[simp]

theorem AlgebraicGeometry.AffineCommGroupScheme.pointMulEquiv_apply {R : Type u} [CommRing R] (G : AffineCommGroupScheme R) (B : Type u) [CommRing B] [Algebra R B] (x : G.Point B) : (G.pointMulEquiv B) x = WithConv.toConv (G.pointToAlgHom B x)

noncomputable def AlgebraicGeometry.AffineCommGroupScheme.baseChangePointMulEquiv {R : Type u} [CommRing R] {K : Type u} [CommRing K] [Algebra R K] (G : AffineCommGroupScheme R) (B : Type u) [CommRing B] [Algebra K B] [Algebra R B] [IsScalarTower R K B] : G.baseChange.Point B ≃* G.Point B

Points of a scalar-extended affine group scheme agree, as a group, with the original points after restricting scalars on the value algebra.

Equations

• G.baseChangePointMulEquiv B = (G.baseChange.pointMulEquiv B).trans (TauCeti.AlgHom.baseChangePointsMulEquiv.symm.trans (G.pointMulEquiv B).symm)

@[simp]

theorem AlgebraicGeometry.AffineCommGroupScheme.pointMulEquiv_baseChangePointMulEquiv {R : Type u} [CommRing R] {K : Type u} [CommRing K] [Algebra R K] (G : AffineCommGroupScheme R) (B : Type u) [CommRing B] [Algebra K B] [Algebra R B] [IsScalarTower R K B] (x : G.baseChange.Point B) : (G.pointMulEquiv B) ((G.baseChangePointMulEquiv B) x) = TauCeti.AlgHom.baseChangePointsMulEquiv.symm ((G.baseChange.pointMulEquiv B) x)

def AlgebraicGeometry.affineFiniteFreeProperty (R : Type u) [CommRing R] : CategoryTheory.ObjectProperty (AffineCommGroupScheme R)

The property that the coordinate algebra is finite free over the base.

Equations

• AlgebraicGeometry.affineFiniteFreeProperty R G = (Module.Free R ↑G.coordinates ∧ Module.Finite R ↑G.coordinates)

@[reducible, inline]

abbrev AlgebraicGeometry.AffineFiniteFreeCommGroupScheme (R : Type u) [CommRing R] : Type (u + 1)

Affine commutative group schemes with finite-free coordinate algebra.

Equations

• AlgebraicGeometry.AffineFiniteFreeCommGroupScheme R = (AlgebraicGeometry.affineFiniteFreeProperty R).FullSubcategory

@[reducible, inline]

abbrev AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.toAffineCommGroupScheme {R : Type u} [CommRing R] (G : AffineFiniteFreeCommGroupScheme R) : AffineCommGroupScheme R

Equations

• G.toAffineCommGroupScheme = G.obj

@[reducible, inline]

abbrev AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.coordinates {R : Type u} [CommRing R] (G : AffineFiniteFreeCommGroupScheme R) : CommHopfAlgCat R

Equations

• G.coordinates = G.obj.coordinates

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.scheme {R : Type u} [CommRing R] (G : AffineFiniteFreeCommGroupScheme R) : Scheme

Equations

• G.scheme = G.obj.scheme

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.structureMap {R : Type u} [CommRing R] (G : AffineFiniteFreeCommGroupScheme R) : G.obj.scheme ⟶ Spec (CommRingCat.of R)

Equations

• G.structureMap = G.obj.structureMap

@[reducible, inline]

abbrev AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.Point {R : Type u} [CommRing R] (G : AffineFiniteFreeCommGroupScheme R) (B : Type u) [CommRing B] [Algebra R B] : Type u

Equations

• G.Point B = G.obj.Point B

instance AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.instFreeXCoordinates {R : Type u} [CommRing R] (G : AffineFiniteFreeCommGroupScheme R) : Module.Free R ↑G.coordinates

instance AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.instFiniteXCoordinates {R : Type u} [CommRing R] (G : AffineFiniteFreeCommGroupScheme R) : Module.Finite R ↑G.coordinates

instance AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.instIsFiniteStructureMap {R : Type u} [CommRing R] (G : AffineFiniteFreeCommGroupScheme R) : IsFinite G.structureMap

instance AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.instFlatStructureMap {R : Type u} [CommRing R] (G : AffineFiniteFreeCommGroupScheme R) : Flat G.structureMap

noncomputable def AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.realize {R : Type u} [CommRing R] (G : AffineFiniteFreeCommGroupScheme R) : FiniteFlatCommGroupScheme (Spec (CommRingCat.of R))

The finite-flat geometric group scheme realized from finite-free Hopf coordinates.

Equations

• G.realize = { obj := G.obj.toCommGroupScheme, property := ⋯ }

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.realizePointMulEquiv {R : Type u} [CommRing R] (G : AffineFiniteFreeCommGroupScheme R) (B : Type u) [CommRing B] [Algebra R B] : G.realize.Point (AffineCommGroupScheme.testObject B) ≃* WithConv (↑G.coordinates →ₐ[R] B)

The affine convolution equivalence with the geometric realization type exposed.

Equations

• G.realizePointMulEquiv B = G.obj.pointMulEquiv B

@[simp]

theorem AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.realizePointMulEquiv_apply {R : Type u} [CommRing R] (G : AffineFiniteFreeCommGroupScheme R) (B : Type u) [CommRing B] [Algebra R B] (x : G.realize.Point (AffineCommGroupScheme.testObject B)) : (G.realizePointMulEquiv B) x = WithConv.toConv (G.obj.pointToAlgHom B x)

noncomputable def AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.realizeMap {R : Type u} [CommRing R] {G H : AffineFiniteFreeCommGroupScheme R} (f : G ⟶ H) : G.realize ⟶ H.realize

Functoriality of geometric realization on morphisms of finite-free affine group schemes.

Equations

• AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.realizeMap f = CategoryTheory.ObjectProperty.homMk ((AlgebraicGeometry.AffineCommGroupScheme.realizationFunctor R).map f.hom)

noncomputable def AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.realizationFunctor (R : Type u) [CommRing R] : CategoryTheory.Functor (AffineFiniteFreeCommGroupScheme R) (FiniteFlatCommGroupScheme (Spec (CommRingCat.of R)))

Geometric realization is a functor from finite-free affine Hopf presentations to finite-flat commutative group schemes. This packages realizeMap together with its identity and composition laws, so downstream constructions can use the categorical API directly.

Equations

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

@[simp]

theorem AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.realizationFunctor_obj {R : Type u} [CommRing R] (G : AffineFiniteFreeCommGroupScheme R) : (realizationFunctor R).obj G = G.realize

@[simp]

theorem AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.realizationFunctor_map {R : Type u} [CommRing R] {G H : AffineFiniteFreeCommGroupScheme R} (f : G ⟶ H) : (realizationFunctor R).map f = realizeMap f

def AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.isoOfCoordinateBialgEquiv {R : Type u} [CommRing R] {G H : AffineFiniteFreeCommGroupScheme R} (e : ↑G.coordinates ≃ₐc[R] ↑H.coordinates) : G ≅ H

A coordinate Hopf-algebra equivalence induces an isomorphism of finite-free affine group schemes.

Equations

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

@[simp]

theorem AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.coordinateMap_isoOfCoordinateBialgEquiv_hom {R : Type u} [CommRing R] {G H : AffineFiniteFreeCommGroupScheme R} (e : ↑G.coordinates ≃ₐc[R] ↑H.coordinates) : AffineCommGroupScheme.coordinateMap (isoOfCoordinateBialgEquiv e).hom.hom = ↑e.symm

@[simp]

theorem AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.coordinateMap_isoOfCoordinateBialgEquiv_inv {R : Type u} [CommRing R] {G H : AffineFiniteFreeCommGroupScheme R} (e : ↑G.coordinates ≃ₐc[R] ↑H.coordinates) : AffineCommGroupScheme.coordinateMap (isoOfCoordinateBialgEquiv e).inv.hom = ↑e

@[simp]

theorem AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.realizeMap_id {R : Type u} [CommRing R] (G : AffineFiniteFreeCommGroupScheme R) : realizeMap (CategoryTheory.CategoryStruct.id G) = CategoryTheory.CategoryStruct.id G.realize

@[simp]

theorem AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.realizeMap_comp {R : Type u} [CommRing R] {G H K : AffineFiniteFreeCommGroupScheme R} (f : G ⟶ H) (g : H ⟶ K) : realizeMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (realizeMap f) (realizeMap g)

theorem AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.pointToAlgHom_map_realizeMap {R : Type u} [CommRing R] {G H : AffineFiniteFreeCommGroupScheme R} (f : G ⟶ H) (B : Type u) [CommRing B] [Algebra R B] (x : G.realize.Point (AffineCommGroupScheme.testObject B)) : H.obj.pointToAlgHom B ((FiniteFlatCommGroupScheme.mapPoint (realizeMap f) (AffineCommGroupScheme.testObject B)) x) = (G.obj.pointToAlgHom B x).comp ↑(AffineCommGroupScheme.coordinateMap f.hom)

Mapping a geometric affine point is contravariant composition with the coordinate map.

@[simp]

theorem AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.realize_scheme {R : Type u} [CommRing R] (G : AffineFiniteFreeCommGroupScheme R) : G.realize.scheme = G.scheme

@[simp]

theorem AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.realize_structureMap {R : Type u} [CommRing R] (G : AffineFiniteFreeCommGroupScheme R) : G.realize.structureMap = G.structureMap

noncomputable def AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.baseChangeFunctor {R : Type u} [CommRing R] {K : Type u} [CommRing K] [Algebra R K] : CategoryTheory.Functor (AffineFiniteFreeCommGroupScheme R) (AffineFiniteFreeCommGroupScheme K)

Scalar extension preserves finite-free affine commutative group schemes.

Equations

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

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.baseChange {R : Type u} [CommRing R] {K : Type u} [CommRing K] [Algebra R K] (G : AffineFiniteFreeCommGroupScheme R) : AffineFiniteFreeCommGroupScheme K

Scalar extension of one finite-free affine commutative group scheme.

Equations

• G.baseChange = AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.baseChangeFunctor.obj G

noncomputable def AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.realizeBaseChangeIso {R : Type u} [CommRing R] {K : Type u} [CommRing K] [Algebra R K] (G : AffineFiniteFreeCommGroupScheme R) : (FiniteFlatCommGroupScheme.baseChange (Spec.map (CommRingCat.ofHom (algebraMap R K)))).obj G.realize ≅ G.baseChange.realize

Coordinate scalar extension of a finite-free affine realization agrees with geometric base change in the category of finite-flat commutative group schemes.

Equations

• G.realizeBaseChangeIso = (AlgebraicGeometry.finiteFlatCommGroupSchemeProperty (AlgebraicGeometry.Spec (CommRingCat.of K))).isoMk G.obj.realizationBaseChangeIso

theorem AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.realizeBaseChangeIso_naturality {R : Type u} [CommRing R] {K : Type u} [CommRing K] [Algebra R K] {G H : AffineFiniteFreeCommGroupScheme R} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp ((FiniteFlatCommGroupScheme.baseChange (Spec.map (CommRingCat.ofHom (algebraMap R K)))).map (realizeMap f)) H.realizeBaseChangeIso.hom = CategoryTheory.CategoryStruct.comp G.realizeBaseChangeIso.hom (realizeMap (baseChangeFunctor.map f))

The realization/base-change comparison is natural in morphisms of finite-free affine commutative group schemes. This is the morphism-level bridge needed to transport exact finite-flat filtrations, rather than merely identifying their individual terms.

noncomputable def AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.order {R : Type u} [CommRing R] (G : AffineFiniteFreeCommGroupScheme R) : ℕ

The order of an affine finite-free group scheme is the rank of its coordinate algebra.

Equations

• G.order = Module.finrank R ↑G.coordinates

theorem AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.baseChange_order {R : Type u} [CommRing R] {K : Type u} [CommRing K] [Algebra R K] [StrongRankCondition R] [StrongRankCondition K] (G : AffineFiniteFreeCommGroupScheme R) : G.baseChange.order = G.order

Finite-free order is invariant under scalar extension.

theorem AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.orderAt_eq_order {R : Type u} [CommRing R] (G : AffineFiniteFreeCommGroupScheme R) (x : ↥(Spec (CommRingCat.of R))) : Scheme.Hom.finrank G.structureMap x = G.order

The geometric rank function agrees everywhere with the finite-free coordinate rank.

theorem AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.point_pow_order_eq_one {R : Type u} [CommRing R] (G : AffineFiniteFreeCommGroupScheme R) (B : Type u) [CommRing B] [Algebra R B] (x : G.Point B) : x ^ G.order = 1

Deligne's order theorem in geometric affine-point form: every Spec B-point over Spec R is killed by the rank of the finite-free coordinate algebra.

theorem AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.realize_point_pow_order_eq_one {R : Type u} [CommRing R] (G : AffineFiniteFreeCommGroupScheme R) (B : Type u) [CommRing B] [Algebra R B] (x : G.realize.Point (AffineCommGroupScheme.testObject B)) : x ^ G.order = 1

Deligne's theorem for points of the constructed geometric realization.

theorem AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.realize_hasConstantOrder {R : Type u} [CommRing R] (G : AffineFiniteFreeCommGroupScheme R) : G.realize.HasConstantOrder G.order

The constructed realization has constant geometric order equal to the coordinate rank.

theorem AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.realize_point_pow_orderAt_eq_one {R : Type u} [CommRing R] (G : AffineFiniteFreeCommGroupScheme R) (B : Type u) [CommRing B] [Algebra R B] (x : G.realize.Point (AffineCommGroupScheme.testObject B)) (s : ↥(Spec (CommRingCat.of R))) : x ^ G.realize.orderAt s = 1

Pointwise geometric-rank form of Deligne's theorem for the constructed realization.

def AlgebraicGeometry.affineFiniteFlatProperty (R : Type u) [CommRing R] : CategoryTheory.ObjectProperty (AffineCommGroupScheme R)

The property that the coordinate algebra is finite and flat over the base.

Equations

• AlgebraicGeometry.affineFiniteFlatProperty R G = (Module.Finite R ↑G.coordinates ∧ Module.Flat R ↑G.coordinates)

@[reducible, inline]

abbrev AlgebraicGeometry.AffineFiniteFlatCommGroupScheme (R : Type u) [CommRing R] : Type (u + 1)

Affine commutative group schemes with finite-flat coordinate algebra. Unlike the finite-free subcategory, these objects do not carry a globally chosen numerical order.

Equations

• AlgebraicGeometry.AffineFiniteFlatCommGroupScheme R = (AlgebraicGeometry.affineFiniteFlatProperty R).FullSubcategory

@[reducible, inline]

abbrev AlgebraicGeometry.AffineFiniteFlatCommGroupScheme.toAffineCommGroupScheme {R : Type u} [CommRing R] (G : AffineFiniteFlatCommGroupScheme R) : AffineCommGroupScheme R

Equations

• G.toAffineCommGroupScheme = G.obj

@[reducible, inline]

abbrev AlgebraicGeometry.AffineFiniteFlatCommGroupScheme.coordinates {R : Type u} [CommRing R] (G : AffineFiniteFlatCommGroupScheme R) : CommHopfAlgCat R

Equations

• G.coordinates = G.obj.coordinates

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.AffineFiniteFlatCommGroupScheme.scheme {R : Type u} [CommRing R] (G : AffineFiniteFlatCommGroupScheme R) : Scheme

Equations

• G.scheme = G.obj.scheme

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.AffineFiniteFlatCommGroupScheme.structureMap {R : Type u} [CommRing R] (G : AffineFiniteFlatCommGroupScheme R) : G.obj.scheme ⟶ Spec (CommRingCat.of R)

Equations

• G.structureMap = G.obj.structureMap

@[reducible, inline]

abbrev AlgebraicGeometry.AffineFiniteFlatCommGroupScheme.Point {R : Type u} [CommRing R] (G : AffineFiniteFlatCommGroupScheme R) (B : Type u) [CommRing B] [Algebra R B] : Type u

Equations

• G.Point B = G.obj.Point B

instance AlgebraicGeometry.AffineFiniteFlatCommGroupScheme.instFiniteXCoordinates {R : Type u} [CommRing R] (G : AffineFiniteFlatCommGroupScheme R) : Module.Finite R ↑G.coordinates

instance AlgebraicGeometry.AffineFiniteFlatCommGroupScheme.instFlatXCoordinates {R : Type u} [CommRing R] (G : AffineFiniteFlatCommGroupScheme R) : Module.Flat R ↑G.coordinates

instance AlgebraicGeometry.AffineFiniteFlatCommGroupScheme.instIsFiniteStructureMap {R : Type u} [CommRing R] (G : AffineFiniteFlatCommGroupScheme R) : IsFinite G.structureMap

instance AlgebraicGeometry.AffineFiniteFlatCommGroupScheme.instFlatStructureMap {R : Type u} [CommRing R] (G : AffineFiniteFlatCommGroupScheme R) : Flat G.structureMap

noncomputable def AlgebraicGeometry.AffineFiniteFlatCommGroupScheme.realize {R : Type u} [CommRing R] (G : AffineFiniteFlatCommGroupScheme R) : FiniteFlatCommGroupScheme (Spec (CommRingCat.of R))

The finite-flat geometric group scheme realized from finite-flat Hopf coordinates.

Equations

• G.realize = { obj := G.obj.toCommGroupScheme, property := ⋯ }

@[simp]

theorem AlgebraicGeometry.AffineFiniteFlatCommGroupScheme.realize_scheme {R : Type u} [CommRing R] (G : AffineFiniteFlatCommGroupScheme R) : G.realize.scheme = G.scheme

@[simp]

theorem AlgebraicGeometry.AffineFiniteFlatCommGroupScheme.realize_structureMap {R : Type u} [CommRing R] (G : AffineFiniteFlatCommGroupScheme R) : G.realize.structureMap = G.structureMap

noncomputable def AlgebraicGeometry.AffineFiniteFlatCommGroupScheme.baseChangeFunctor {R : Type u} [CommRing R] {K : Type u} [CommRing K] [Algebra R K] : CategoryTheory.Functor (AffineFiniteFlatCommGroupScheme R) (AffineFiniteFlatCommGroupScheme K)

Scalar extension preserves finite-flat affine commutative group schemes.

Equations

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

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.AffineFiniteFlatCommGroupScheme.baseChange {R : Type u} [CommRing R] {K : Type u} [CommRing K] [Algebra R K] (G : AffineFiniteFlatCommGroupScheme R) : AffineFiniteFlatCommGroupScheme K

Scalar extension of one finite-flat affine commutative group scheme.

Equations

• G.baseChange = AlgebraicGeometry.AffineFiniteFlatCommGroupScheme.baseChangeFunctor.obj G

noncomputable def AlgebraicGeometry.AffineFiniteFlatCommGroupScheme.realizeBaseChangeIso {R : Type u} [CommRing R] {K : Type u} [CommRing K] [Algebra R K] (G : AffineFiniteFlatCommGroupScheme R) : (FiniteFlatCommGroupScheme.baseChange (Spec.map (CommRingCat.ofHom (algebraMap R K)))).obj G.realize ≅ G.baseChange.realize

Coordinate scalar extension of a finite-flat affine realization agrees with geometric base change in the category of finite-flat commutative group schemes.

Equations

• G.realizeBaseChangeIso = (AlgebraicGeometry.finiteFlatCommGroupSchemeProperty (AlgebraicGeometry.Spec (CommRingCat.of K))).isoMk G.obj.realizationBaseChangeIso

theorem AlgebraicGeometry.AffineFiniteFlatCommGroupScheme.baseChange_structureMap_finrank {R : Type u} [CommRing R] {K : Type u} [CommRing K] [Algebra R K] (G : AffineFiniteFlatCommGroupScheme R) (s : ↥(Spec (CommRingCat.of K))) : Scheme.Hom.finrank G.baseChange.structureMap s = Scheme.Hom.finrank G.structureMap ((Spec.map (CommRingCat.ofHom (algebraMap R K))) s)

The local rank of finite-flat coordinates is compatible with scalar extension.

theorem AlgebraicGeometry.AffineFiniteFlatCommGroupScheme.baseChange_realize_hasConstantOrder {R : Type u} [CommRing R] {K : Type u} [CommRing K] [Algebra R K] (G : AffineFiniteFlatCommGroupScheme R) (n : ℕ) (hG : G.realize.HasConstantOrder n) : G.baseChange.realize.HasConstantOrder n

Constant geometric order of a finite-flat affine realization survives arbitrary scalar extension, including over disconnected bases.

theorem AlgebraicGeometry.AffineFiniteFlatCommGroupScheme.algPoint_pow_eq_one_of_constantRank {R : Type u} [CommRing R] {A B : Type u} [CommRing A] [CommRing B] [HopfAlgebra R A] [Coalgebra.IsCocomm R A] [Module.Finite R A] [Module.Flat R A] [Algebra R B] (n : ℕ) (hA : ∀ (s : PrimeSpectrum R), Module.rankAtStalk A s = n) (f : A →ₐ[R] B) : WithConv.toConv f ^ n = 1

Algebraic localization and descent for Deligne's order theorem. Finite flatness is used to make the coordinate algebra free after localizing at a maximal ideal; the constant-rank hypothesis supplies one exponent on all components of the base.

theorem AlgebraicGeometry.AffineFiniteFlatCommGroupScheme.point_pow_eq_one_of_constantRank {R : Type u} [CommRing R] (G : AffineFiniteFlatCommGroupScheme R) (n : ℕ) (hG : ∀ (s : ↥(Spec (CommRingCat.of R))), Scheme.Hom.finrank G.structureMap s = n) (B : Type u) [CommRing B] [Algebra R B] (x : G.Point B) : x ^ n = 1

Every affine point of a finite-flat affine group scheme of constant rank n is killed by n. This is the global finite-locally-free geometric form of Deligne's theorem.

theorem AlgebraicGeometry.AffineFiniteFlatCommGroupScheme.realize_point_pow_eq_one_of_hasConstantOrder {R : Type u} [CommRing R] (G : AffineFiniteFlatCommGroupScheme R) (n : ℕ) (hG : G.realize.HasConstantOrder n) (B : Type u) [CommRing B] [Algebra R B] (x : G.realize.Point (AffineCommGroupScheme.testObject B)) : x ^ n = 1

Strong geometric form for the constructed finite-flat realization: a constant-order certificate on the geometric structure morphism kills every affine test point by that order.

theorem AlgebraicGeometry.AffineFiniteFlatCommGroupScheme.point_pow_finrank_eq_one_of_isLocalRing {R : Type u} [CommRing R] (G : AffineFiniteFlatCommGroupScheme R) [IsLocalRing R] (B : Type u) [CommRing B] [Algebra R B] (x : G.Point B) : x ^ Module.finrank R ↑G.coordinates = 1

Over a local base, finite flat coordinates are free, so Deligne's theorem gives the honest finite-flat geometric point statement.

structure AlgebraicGeometry.FiniteFlatCommGroupScheme.AffineFiniteFreePresentation {R : Type u} [CommRing R] (G : FiniteFlatCommGroupScheme (Spec (CommRingCat.of R))) : Type (u + 1)

A certificate that a geometric finite-flat commutative group scheme over Spec R is presented by a finite-free commutative, cocommutative coordinate Hopf algebra. Constructed realizations have a canonical such certificate; the structure also records presentations of pre-existing geometric objects.

• hopf : AffineFiniteFreeCommGroupScheme R

  The finite-free coordinate Hopf presentation.

• schemeIso : G.scheme ≅ self.hopf.scheme

  Identification of the underlying geometric scheme with the spectrum of the coordinates.

• schemeIso_hom_structureMap : CategoryTheory.CategoryStruct.comp self.schemeIso.hom self.hopf.structureMap = G.structureMap

  The scheme identification lies over Spec R.

• pointMulEquiv (B : Type u) [CommRing B] [Algebra R B] : G.Point (AffineCommGroupScheme.testObject B) ≃* self.hopf.Point B

  Compatibility of geometric group-valued points with convolution points.

• pointMulEquiv_left (B : Type u) [CommRing B] [Algebra R B] (x : G.Point (AffineCommGroupScheme.testObject B)) : CategoryTheory.Over.Hom.left ((self.pointMulEquiv B) x) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left x) self.schemeIso.hom

  The point equivalence is induced by the displayed scheme isomorphism, rather than an unrelated abstract equivalence of groups.

• order_eq : G.HasConstantOrder self.hopf.order

  The geometric rank agrees with the coordinate-algebra rank on the whole affine base.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.AffineFiniteFreePresentation.point_pow_order_eq_one {R : Type u} [CommRing R] {G : FiniteFlatCommGroupScheme (Spec (CommRingCat.of R))} (P : G.AffineFiniteFreePresentation) (B : Type u) [CommRing B] [Algebra R B] (x : G.Point (AffineCommGroupScheme.testObject B)) : x ^ P.hopf.order = 1

Deligne's theorem transported all the way to a point of a geometric finite-flat commutative group scheme carrying an explicit affine finite-free Hopf presentation.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.AffineFiniteFreePresentation.point_pow_orderAt_eq_one {R : Type u} [CommRing R] {G : FiniteFlatCommGroupScheme (Spec (CommRingCat.of R))} (P : G.AffineFiniteFreePresentation) (B : Type u) [CommRing B] [Algebra R B] (x : G.Point (AffineCommGroupScheme.testObject B)) (s : ↥(Spec (CommRingCat.of R))) : x ^ G.orderAt s = 1

Pointwise-rank form of the geometric order theorem. This formulation remains meaningful on the geometric side and records explicitly where constant order enters.

noncomputable def AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.presentation {R : Type u} [CommRing R] (G : AffineFiniteFreeCommGroupScheme R) : G.realize.AffineFiniteFreePresentation

The canonical finite-free Hopf presentation of the constructed geometric realization.

Equations

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

theorem AlgebraicGeometry.AffineFiniteFreeCommGroupScheme.exists_geometric_realization {R : Type u} [CommRing R] (G : AffineFiniteFreeCommGroupScheme R) : ∃ (H : FiniteFlatCommGroupScheme (Spec (CommRingCat.of R))) (P : H.AffineFiniteFreePresentation), P.hopf = G

Every finite-free commutative, cocommutative Hopf algebra has its canonical geometric finite-flat realization. This permanent theorem is the destination of the checked Challenge bridge.