Fppf quotient presentations for ambient commutative group schemes

An elliptic curve quotient by a finite subgroup is not a finite group scheme, so the existing finite-flat and quasi-finite quotient records cannot express it. This file gives the ambient version. A FppfQuotientPresentation i consists of an actual commutative group scheme, an fppf-surjective homomorphism to it, and an isomorphism identifying the supplied inclusion i with the scheme-theoretic kernel.

This is a certificate for a quotient that has already been constructed. It is not a theorem constructing G/K, and it does not separately assert a categorical coequalizer. An fppf cover with the displayed geometric kernel presents the corresponding quotient of fppf sheaves.

The point API deliberately keeps the arithmetic obstruction visible. On every test scheme X there is an injection

G(X) / K(X) ⟶ Q(X).

No surjectivity is asserted. Over the base, the image is exactly the zero fibre of the genuine connecting homomorphism Q(S) ⟶ H¹_fppf(S, K). Thus this file cannot be used to identify Q(S) with G(S) / K(S) while a nontrivial H¹ obstruction remains.

structure AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation {S : Scheme} {K G : CommGroupScheme S} (i : K ⟶ G) : Type (u + 1)

An actual ambient fppf quotient projection with a specified geometric kernel.

The parameter i : K ⟶ G is retained in the type so the kernel identification is with the caller's chosen subgroup scheme and inclusion, not merely with an unnamed isomorphic object.

• quotient : CommGroupScheme S

  The supplied quotient group scheme.

• project : G ⟶ self.quotient

  The supplied quotient homomorphism.

• project_flat : Flat (underlyingHom self.project)

  Flatness of the quotient projection.

• project_surjective : Surjective (underlyingHom self.project)

  Surjectivity of the quotient projection on underlying topological spaces.

• project_lfp : LocallyOfFinitePresentation (underlyingHom self.project)

  Local finite presentation of the quotient projection.

• kernelIso : K ≅ kernel self.project

  Identification of the supplied subgroup with the geometric kernel.

• kernelIso_hom_kernelInclusion : CategoryTheory.CategoryStruct.comp self.kernelIso.hom (kernelInclusion self.project) = i

  The kernel identification carries the canonical inclusion to the supplied inclusion.

@[reducible, inline]

abbrev AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.kernelPresentation {S : Scheme} {K G : CommGroupScheme S} {i : K ⟶ G} (D : FppfQuotientPresentation i) : KernelPresentation D.project

The quotient presentation as the ambient geometric-kernel record used by the existing fppf connecting construction.

Equations

• D.kernelPresentation = { kernel := K, inclusion := i, kernelIso := D.kernelIso, kernelIso_hom_kernelInclusion := ⋯ }

theorem AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.project_is_fppf {S : Scheme} {K G : CommGroupScheme S} {i : K ⟶ G} (D : FppfQuotientPresentation i) : Flat (underlyingHom D.project) ∧ Surjective (underlyingHom D.project) ∧ LocallyOfFinitePresentation (underlyingHom D.project)

The three geometric properties making the supplied projection an fppf cover.

theorem AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.project_point_eq_one_iff {S : Scheme} {K G : CommGroupScheme S} {i : K ⟶ G} (D : FppfQuotientPresentation i) (X : CategoryTheory.Over S) (x : G.Point X) : (mapPoint D.project X) x = 1 ↔ x ∈ Set.range ⇑(mapPoint i X)

The chosen subgroup is exactly the pointwise kernel on every test scheme.

noncomputable def AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.baseChange {S T : Scheme} {K G : CommGroupScheme S} {i : K ⟶ G} (D : FppfQuotientPresentation i) (t : T ⟶ S) : FppfQuotientPresentation ((CategoryTheory.Over.pullback t).mapCommGrp.map i)

Pull an ambient fppf quotient presentation back along an arbitrary base morphism. Both the specified kernel object and its inclusion are the literal pullbacks of the original data.

Equations

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

@[simp]

theorem AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.baseChange_quotient {S T : Scheme} {K G : CommGroupScheme S} {i : K ⟶ G} (D : FppfQuotientPresentation i) (t : T ⟶ S) : (D.baseChange t).quotient = (CategoryTheory.Over.pullback t).mapCommGrp.obj D.quotient

@[simp]

theorem AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.baseChange_project {S T : Scheme} {K G : CommGroupScheme S} {i : K ⟶ G} (D : FppfQuotientPresentation i) (t : T ⟶ S) : (D.baseChange t).project = (CategoryTheory.Over.pullback t).mapCommGrp.map D.project

@[simp]

theorem AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.baseChange_kernelPresentation_kernel {S T : Scheme} {K G : CommGroupScheme S} {i : K ⟶ G} (D : FppfQuotientPresentation i) (t : T ⟶ S) : (D.baseChange t).kernelPresentation.kernel = (CategoryTheory.Over.pullback t).mapCommGrp.obj K

@[simp]

theorem AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.baseChange_kernelPresentation_inclusion {S T : Scheme} {K G : CommGroupScheme S} {i : K ⟶ G} (D : FppfQuotientPresentation i) (t : T ⟶ S) : (D.baseChange t).kernelPresentation.inclusion = (CategoryTheory.Over.pullback t).mapCommGrp.map i

noncomputable def AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.pointKernelRange {S : Scheme} {K G : CommGroupScheme S} {i : K ⟶ G} (_D : FppfQuotientPresentation i) (X : CategoryTheory.Over S) : Subgroup (G.Point X)

The image of the specified kernel on X-valued points.

Equations

• _D.pointKernelRange X = (AlgebraicGeometry.CommGroupScheme.mapPoint i X).range

@[reducible, inline]

abbrev AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.PointQuotient {S : Scheme} {K G : CommGroupScheme S} {i : K ⟶ G} (D : FppfQuotientPresentation i) (X : CategoryTheory.Over S) : Type u

The quotient of source points by points coming from the specified geometric kernel.

Equations

• D.PointQuotient X = (G.Point X ⧸ D.pointKernelRange X)

noncomputable def AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.pointQuotientMap {S : Scheme} {K G : CommGroupScheme S} {i : K ⟶ G} (D : FppfQuotientPresentation i) (X : CategoryTheory.Over S) : D.PointQuotient X →* D.quotient.Point X

The quotient projection on represented points, induced by the actual group-scheme projection.

Equations

• D.pointQuotientMap X = QuotientGroup.lift (D.pointKernelRange X) (AlgebraicGeometry.CommGroupScheme.mapPoint D.project X) ⋯

@[simp]

theorem AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.pointQuotientMap_mk {S : Scheme} {K G : CommGroupScheme S} {i : K ⟶ G} (D : FppfQuotientPresentation i) (X : CategoryTheory.Over S) (x : G.Point X) : (D.pointQuotientMap X) ((QuotientGroup.mk' (D.pointKernelRange X)) x) = (mapPoint D.project X) x

theorem AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.pointKernelRange_eq_project_ker {S : Scheme} {K G : CommGroupScheme S} {i : K ⟶ G} (D : FppfQuotientPresentation i) (X : CategoryTheory.Over S) : D.pointKernelRange X = (mapPoint D.project X).ker

Scheme-theoretic kernel exactness says that the specified point image is precisely the kernel of the quotient projection on every test scheme.

theorem AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.pointQuotientMap_injective {S : Scheme} {K G : CommGroupScheme S} {i : K ⟶ G} (D : FppfQuotientPresentation i) (X : CategoryTheory.Over S) : Function.Injective ⇑(D.pointQuotientMap X)

The point quotient maps injectively into the points of the quotient scheme on every test scheme. Surjectivity is deliberately absent.

theorem AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.pointKernelRange_map_pointMulEquivOfOverIso {S : Scheme} {K G : CommGroupScheme S} {i : K ⟶ G} (D : FppfQuotientPresentation i) {X Y : CategoryTheory.Over S} (e : X ≅ Y) : Subgroup.map (G.pointMulEquivOfOverIso e).toMonoidHom (D.pointKernelRange X) = D.pointKernelRange Y

Changing the test scheme by an isomorphism carries the specified point-kernel image to the specified point-kernel image.

noncomputable def AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.pointQuotientMulEquivOfOverIso {S : Scheme} {K G : CommGroupScheme S} {i : K ⟶ G} (D : FppfQuotientPresentation i) {X Y : CategoryTheory.Over S} (e : X ≅ Y) : D.PointQuotient X ≃* D.PointQuotient Y

Point quotients are invariant under an isomorphism of test schemes.

Equations

• D.pointQuotientMulEquivOfOverIso e = QuotientGroup.congr (D.pointKernelRange X) (D.pointKernelRange Y) (G.pointMulEquivOfOverIso e) ⋯

theorem AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.pointQuotientMap_pointQuotientMulEquivOfOverIso {S : Scheme} {K G : CommGroupScheme S} {i : K ⟶ G} (D : FppfQuotientPresentation i) {X Y : CategoryTheory.Over S} (e : X ≅ Y) (x : D.PointQuotient X) : (D.pointQuotientMap Y) ((D.pointQuotientMulEquivOfOverIso e) x) = (D.quotient.pointMulEquivOfOverIso e) ((D.pointQuotientMap X) x)

The point-quotient injection commutes with changing the test scheme by an isomorphism.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.projectCover {S : Scheme} {K G : CommGroupScheme S} {i : K ⟶ G} (D : FppfQuotientPresentation i) : Scheme.Cover Scheme.fppfPrecoverage D.quotient.X.left

The quotient projection itself, regarded as a singleton fppf cover of its target.

Equations

• D.projectCover = AlgebraicGeometry.Scheme.Hom.cover (AlgebraicGeometry.CommGroupScheme.underlyingHom D.project) ⋯

noncomputable def AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.locallyLiftable {S : Scheme} {K G : CommGroupScheme S} {i : K ⟶ G} (D : FppfQuotientPresentation i) : D.kernelPresentation.LocallyLiftable

Pulling the actual quotient cover back along a target section gives local source lifts.

Equations

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

noncomputable def AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.boundaryHom {S : Scheme} {K G : CommGroupScheme S} {i : K ⟶ G} (D : FppfQuotientPresentation i) : D.quotient.BasePoint →* K.FppfHOne

The genuine fppf connecting homomorphism attached to the supplied quotient projection.

Equations

• D.boundaryHom = D.locallyLiftable.boundaryHom

@[simp]

theorem AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.boundaryHom_project {S : Scheme} {K G : CommGroupScheme S} {i : K ⟶ G} (D : FppfQuotientPresentation i) (x : G.BasePoint) : D.boundaryHom ((mapPoint D.project (baseObject S)) x) = 1

theorem AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.boundaryHom_eq_one_iff_exists_pointQuotient {S : Scheme} {K G : CommGroupScheme S} {i : K ⟶ G} (D : FppfQuotientPresentation i) (q : D.quotient.BasePoint) : D.boundaryHom q = 1 ↔ ∃ (x : D.PointQuotient (baseObject S)), (D.pointQuotientMap (baseObject S)) x = q

A quotient-scheme base point has zero connecting class exactly when it is represented by a class in the point quotient. This is the explicit H¹ obstruction to surjectivity.

theorem AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.exact_pointQuotientMap_boundaryHom {S : Scheme} {K G : CommGroupScheme S} {i : K ⟶ G} (D : FppfQuotientPresentation i) : Function.MulExact ⇑(D.pointQuotientMap (baseObject S)) ⇑D.boundaryHom

The point quotient embeds as exactly the zero-boundary fibre in the low-degree fppf cohomology sequence.

noncomputable def AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.boundaryHomOfOverIso {S : Scheme} {K G : CommGroupScheme S} {i : K ⟶ G} (D : FppfQuotientPresentation i) {X : CategoryTheory.Over S} (e : baseObject S ≅ X) : D.quotient.Point X →* K.FppfHOne

Transport the fppf boundary homomorphism from base sections to points on an isomorphic test scheme. This changes only the presentation of the represented points; it does not assert point surjectivity.

Equations

• D.boundaryHomOfOverIso e = D.boundaryHom.comp (D.quotient.pointMulEquivOfOverIso e).symm.toMonoidHom

theorem AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.exact_pointQuotientMap_boundaryHomOfOverIso {S : Scheme} {K G : CommGroupScheme S} {i : K ⟶ G} (D : FppfQuotientPresentation i) {X : CategoryTheory.Over S} (e : baseObject S ≅ X) : Function.MulExact ⇑(D.pointQuotientMap X) ⇑(D.boundaryHomOfOverIso e)

After transport along an isomorphism of test schemes, the same point quotient embeds as exactly the zero-boundary fibre.