Quasi-finite flat commutative group schemes and their fppf cohomology

Mazur's pre-admissible group schemes over Spec ℤ are flat, quasi-finite, separated, and of finite presentation; they are only required to become finite after removing the level prime. This file packages the common structural part without prematurely adding a level, a power that kills the group, an open-base finiteness witness, or an admissible filtration.

Here quasi-finite is represented by Mathlib's LocallyQuasiFinite together with QuasiCompact, and finite presentation by LocallyOfFinitePresentation together with the same quasi-compactness condition. Morphisms act functorially on represented points and fppf H¹. Finite-flat group schemes and their morphisms embed in this category and provide compiled compatibility consumers for both the coefficient and map-level ambient APIs.

No extension-by-zero construction or claim about the four elementary admissible factors is made in this file.

def AlgebraicGeometry.quasiFiniteFlatCommGroupSchemeProperty (S : Scheme) : CategoryTheory.ObjectProperty (CommGroupScheme S)

The structural property of a flat, quasi-finite, separated commutative group scheme of finite presentation over S.

Equations

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

@[reducible, inline]

abbrev AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme (S : Scheme) : Type (u + 1)

Flat, quasi-finite, separated commutative group schemes of finite presentation over S. This is the ambient category in which Mazur's integral pre-admissible groups live.

Equations

• AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme S = (AlgebraicGeometry.quasiFiniteFlatCommGroupSchemeProperty S).FullSubcategory

@[reducible, inline]

abbrev AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.toCommGroupScheme {S : Scheme} (G : QuasiFiniteFlatCommGroupScheme S) : CommGroupScheme S

The underlying ambient commutative group scheme.

Equations

• G.toCommGroupScheme = G.obj

@[reducible, inline]

abbrev AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.scheme {S : Scheme} (G : QuasiFiniteFlatCommGroupScheme S) : Scheme

The underlying scheme.

Equations

• G.scheme = G.obj.X.left

@[reducible, inline]

abbrev AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.structureMap {S : Scheme} (G : QuasiFiniteFlatCommGroupScheme S) : G.scheme ⟶ S

The flat, quasi-finite, separated, finite-presentation structure morphism.

Equations

• G.structureMap = G.obj.X.hom

instance AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.instFlatStructureMap {S : Scheme} (G : QuasiFiniteFlatCommGroupScheme S) : Flat G.structureMap

instance AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.instLocallyQuasiFiniteStructureMap {S : Scheme} (G : QuasiFiniteFlatCommGroupScheme S) : LocallyQuasiFinite G.structureMap

instance AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.instQuasiCompactStructureMap {S : Scheme} (G : QuasiFiniteFlatCommGroupScheme S) : QuasiCompact G.structureMap

instance AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.instIsSeparatedStructureMap {S : Scheme} (G : QuasiFiniteFlatCommGroupScheme S) : IsSeparated G.structureMap

instance AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.instLocallyOfFinitePresentationStructureMap {S : Scheme} (G : QuasiFiniteFlatCommGroupScheme S) : LocallyOfFinitePresentation G.structureMap

@[reducible, inline]

abbrev AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.FppfHOne {S : Scheme} (G : QuasiFiniteFlatCommGroupScheme S) : Type (max (v + 1) (u + 1))

Global fppf H¹ of a quasi-finite flat commutative group scheme, through the ambient represented-point wrapper.

Equations

• G.FppfHOne = G.obj.FppfHOne

@[instance_reducible]

noncomputable instance AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.fppfHOneCommGroup {S : Scheme} (G : QuasiFiniteFlatCommGroupScheme S) : CommGroup G.FppfHOne

Equations

• G.fppfHOneCommGroup = G.obj.fppfHOneCommGroup

noncomputable def AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.mapPoint {S : Scheme} {G H : QuasiFiniteFlatCommGroupScheme S} (f : G ⟶ H) (T : CategoryTheory.Over S) : G.obj.Point T →* H.obj.Point T

A morphism of quasi-finite flat commutative group schemes acts on test-scheme points through its underlying ambient group-scheme morphism.

Equations

• AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.mapPoint f T = AlgebraicGeometry.CommGroupScheme.mapPoint f.hom T

@[simp]

theorem AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.mapPoint_apply {S : Scheme} {G H : QuasiFiniteFlatCommGroupScheme S} (f : G ⟶ H) (T : CategoryTheory.Over S) (x : G.obj.Point T) : (mapPoint f T) x = CategoryTheory.CategoryStruct.comp x f.hom.hom.hom.hom

noncomputable def AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.fppfHOneMap {S : Scheme} {G H : QuasiFiniteFlatCommGroupScheme S} (f : G ⟶ H) : G.FppfHOne →* H.FppfHOne

A quasi-finite flat group-scheme morphism induces the canonical map on global fppf H¹.

Equations

• AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.fppfHOneMap f = AlgebraicGeometry.CommGroupScheme.fppfHOneMap f.hom

@[simp]

theorem AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.fppfHOneMap_id {S : Scheme} (G : QuasiFiniteFlatCommGroupScheme S) : fppfHOneMap (CategoryTheory.CategoryStruct.id G) = MonoidHom.id G.FppfHOne

theorem AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.fppfHOneMap_comp {S : Scheme} {G H K : QuasiFiniteFlatCommGroupScheme S} (f : G ⟶ H) (g : H ⟶ K) : fppfHOneMap (CategoryTheory.CategoryStruct.comp f g) = (fppfHOneMap g).comp (fppfHOneMap f)

def AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.ofFiniteFlat {S : Scheme} (G : FiniteFlatCommGroupScheme S) [LocallyOfFinitePresentation G.obj.X.hom] : QuasiFiniteFlatCommGroupScheme S

A finite-flat commutative group scheme whose structure map is locally of finite presentation satisfies the broader quasi-finite, separated, finite-presentation property. The hypothesis is explicit because the legacy finite-flat wrapper does not store finite-presentation data.

Equations

• AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.ofFiniteFlat G = { obj := G.obj, property := ⋯ }

noncomputable def AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.fppfHOneMulEquivOfFiniteFlat {S : Scheme} (G : FiniteFlatCommGroupScheme S) [LocallyOfFinitePresentation G.obj.X.hom] : (ofFiniteFlat G).FppfHOne ≃* G.FppfHOne

The new quasi-finite wrapper is definitionally compatible with the existing finite-flat global fppf H¹; this is the first downstream consumer of the broader interface.

Equations

• AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.fppfHOneMulEquivOfFiniteFlat G = MulEquiv.refl (AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.ofFiniteFlat G).FppfHOne

noncomputable def AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.ofFiniteFlatMap {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) [LocallyOfFinitePresentation G.obj.X.hom] [LocallyOfFinitePresentation H.obj.X.hom] : ofFiniteFlat G ⟶ ofFiniteFlat H

A finite-flat morphism gives the same morphism after both endpoints are regarded as quasi-finite flat group schemes.

Equations

• AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.ofFiniteFlatMap f = CategoryTheory.ObjectProperty.homMk f.hom

theorem AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.fppfHOneMap_ofFiniteFlat_eq {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) [LocallyOfFinitePresentation G.obj.X.hom] [LocallyOfFinitePresentation H.obj.X.hom] : fppfHOneMap (ofFiniteFlatMap f) = FiniteFlatCommGroupScheme.fppfHOneMap f

The quasi-finite and finite-flat maps on fppf H¹ agree under the definitional compatibility equivalences. This is a morphism-level downstream consumer, needed before transporting exact quotient sequences to Mazur's four integral elementary factors.