4. 04 — Prime-level infrastructure
Néron models over discrete valuation rings. Construct the smooth separated model of an abelian variety, recover its generic fibre, and expose the Néron mapping property.
Status: blocked.
Canonical deliverables — these names are authoritative for this node:
-
structure(proposed):AlgebraicGeometry.NeronModelPackage a smooth separated model over a discrete valuation ring together with its generic fibre. -
theorem(proposed):AlgebraicGeometry.NeronModel.genericFiberEquivIdentify the generic fibre of a Neron model with the original smooth group variety. -
theorem(proposed):AlgebraicGeometry.NeronModel.mappingPropertyState the Neron mapping property as a unique extension theorem for smooth test schemes.
Identity components and component groups. Construct the open identity component of a Néron model and the finite component group of its special fibre.
Status: blocked.
Canonical deliverables — these names are authoritative for this node:
-
definition(proposed):AlgebraicGeometry.NeronModel.identityComponentDefine the open identity component of the special fibre of a Neron model. -
definition(proposed):AlgebraicGeometry.NeronModel.componentGroupDefine the finite component group of the special fibre. -
theorem(proposed):AlgebraicGeometry.NeronModel.specializationExactExpose the exact sequence relating integral points, the identity component, and the component group.
Torsion specialization through Néron models. Prime-to-residue-characteristic torsion specializes injectively into the identity component plus component group, in exactly the form consumed by Mazur's argument.
Status: blocked.
Canonical deliverables — these names are authoritative for this node:
-
theorem(proposed):AlgebraicGeometry.NeronModel.primeToResidueTorsion_injectiveProve injectivity of specialization on torsion prime to the residue characteristic. -
theorem(proposed):AlgebraicGeometry.NeronModel.torsion_componentGroupRelate torsion points outside the identity component to the special-fibre component group.
Finite-flat commutative group schemes. Build the category, kernels,
quotients, and base change, tested on constant groups, \mu_p, and
multiplication kernels.
Status: planned.
Canonical deliverables — these names are authoritative for this node:
-
structure(proposed):AlgebraicGeometry.FiniteFlatCommGroupSchemePackage finite flat commutative group schemes over an arithmetic base. -
definition(proposed):AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelConstruct kernels of morphisms in the finite-flat group-scheme category. -
definition(proposed):AlgebraicGeometry.FiniteFlatCommGroupScheme.quotientConstruct quotients by finite-flat closed subgroup schemes. -
theorem(proposed):AlgebraicGeometry.FiniteFlatCommGroupScheme.baseChangeProve compatibility of kernels and quotients with the required base changes.
Connected–étale sequence. Every finite-flat commutative group scheme in the required local setting has a functorial connected–étale exact sequence, compatible with base change.
Status: blocked.
Canonical deliverables — these names are authoritative for this node:
-
definition(proposed):AlgebraicGeometry.FiniteFlatCommGroupScheme.connectedComponentDefine the connected identity component of a finite-flat commutative group scheme. -
definition(proposed):AlgebraicGeometry.FiniteFlatCommGroupScheme.etaleQuotientDefine the maximal etale quotient in the connected-etale sequence. -
theorem(proposed):AlgebraicGeometry.FiniteFlatCommGroupScheme.connectedEtale_exactProve exactness, functoriality, and base-change compatibility of the connected-etale sequence.
Oort–Tate classification and Raynaud uniqueness. Classify finite-flat group schemes of prime order and prove the uniqueness statements controlling extensions of generic-fibre subgroup schemes.
Status: blocked.
Canonical deliverables — these names are authoritative for this node:
-
theorem(proposed):AlgebraicGeometry.OortTate.classificationClassify finite-flat commutative group schemes of prime order over the required arithmetic bases. -
theorem(proposed):AlgebraicGeometry.Raynaud.primeOrder_uniquenessProve the uniqueness theorem for finite-flat prime-order models used in the semistability argument.
The \Gamma_0 modular-curve moduli problem. Define elliptic curves with
cyclic finite-flat subgroups and their isomorphisms, families, and base change.
Status: planned.
Canonical deliverables — these names are authoritative for this node:
-
structure(proposed):ModularCurve.GammaZeroStructurePackage an elliptic curve together with a cyclic finite-flat subgroup of order N. -
definition(proposed):ModularCurve.XZeroModuliDefine the Gamma-zero moduli functor with its isomorphisms and base-change action.
Integral compactified X_0(N). Construct the compactification used by
Mazur and prove its generic-fibre and reduction interfaces.
Status: blocked.
Canonical deliverables — these names are authoritative for this node:
-
structure(proposed):ModularCurve.IntegralXZeroPackage the proper integral compactification of the Gamma-zero moduli problem. -
theorem(proposed):ModularCurve.IntegralXZero.genericFiberIdentify the generic fibre with the characteristic-zero modular curveX_0(N). -
theorem(proposed):ModularCurve.IntegralXZero.reductionCompatibilityExpose the reduction and specialization interfaces consumed by Mazur's argument.
Cusps and the rational cusp divisor. Construct the rational cusps, their specializations, and the degree-zero difference of the zero and infinity cusps.
Status: blocked.
Canonical deliverables — these names are authoritative for this node:
-
definition(proposed):ModularCurve.XZero.cuspDefine the rational cusp sections on the integral modular curve. -
definition(proposed):ModularCurve.XZero.cuspDifferenceDefine the degree-zero divisor class given by the difference of the two rational cusps. -
theorem(proposed):ModularCurve.XZero.cusp_specializationProve the cusp sections and their divisor class specialize compatibly at the required primes.
The modular Jacobian J_0(N). Instantiate the shared Jacobian and
Abel–Jacobi APIs on X_0(N), compatibly with the integral model.
Status: blocked.
Canonical deliverables — these names are authoritative for this node:
-
structure(proposed):ModularCurve.ModularJacobianInstantiate the shared Jacobian construction on the modular curveX_0(N). -
definition(proposed):ModularCurve.ModularJacobian.abelJacobiDefine the Abel-Jacobi map fromX_0(N)using a chosen rational cusp. -
theorem(proposed):ModularCurve.ModularJacobian.integralCompatibilityProve compatibility of the modular Jacobian and Abel-Jacobi map with the integral model.
Hecke correspondences on J_0(N). Construct the correspondences and their
endomorphism action, including base-change and composition laws.
Status: blocked.
Canonical deliverables — these names are authoritative for this node:
-
structure(proposed):ModularCurve.HeckeCorrespondencePackage the two finite maps defining a Hecke correspondence onX_0(N). -
definition(proposed):ModularCurve.ModularJacobian.heckeOperatorConstruct the induced Hecke endomorphism of the modular Jacobian. -
theorem(proposed):ModularCurve.ModularJacobian.hecke_compProve the required composition, base-change, and isogeny compatibility laws.
The Eisenstein ideal and Hecke quotient. Define the Eisenstein ideal and prove the finite-quotient and local-principality interfaces used by the arithmetic quotient.
Status: blocked.
Canonical deliverables — these names are authoritative for this node:
-
definition(proposed):ModularCurve.EisensteinIdealDefine the ideal in the Hecke algebra generated by the Eisenstein relations. -
definition(proposed):ModularCurve.EisensteinHeckeQuotientDefine the finite Hecke-algebra quotient cut out by the Eisenstein ideal. -
theorem(proposed):ModularCurve.EisensteinIdeal.locallyPrincipalProve the local-principality input required to control the associated quotient ofJ_0(N).
Arithmetic of the Eisenstein quotient. Construct the quotient and prove that its rational Mordell–Weil group is finite, the cusp difference has the expected exact order, and its image is nonzero.
Status: blocked.
Canonical deliverables — these names are authoritative for this node:
-
structure(proposed):ModularCurve.EisensteinQuotientConstruct the abelian-variety quotient ofJ_0(N)determined by the Eisenstein ideal. -
theorem(proposed):ModularCurve.EisensteinQuotient.mordellWeil_finiteProve finiteness of the rational Mordell-Weil group of the Eisenstein quotient. -
theorem(proposed):ModularCurve.EisensteinQuotient.cuspDifference_orderCompute the exact order of the rational cusp-difference class in the quotient. -
theorem(proposed):ModularCurve.EisensteinQuotient.cuspDifference_ne_zeroProve that the cusp-difference image is nonzero in the cases used by specialization.
Cyclotomic unramified character extensions. Develop the class-field and
cyclotomic input excluding the inverse-cyclotomic everywhere-unramified
extension over \mathbb{Q}(\zeta_p).
Status: planned.
Canonical deliverables — these names are authoritative for this node:
-
definition(proposed):NumberTheory.CyclotomicCharacter.inverseExtensionPackage the inverse-cyclotomic character extension over the p-th cyclotomic field. -
theorem(proposed):NumberTheory.CyclotomicCharacter.unramifiedAtFinitePlacesGive the local criterion showing that the relevant extension is unramified at every finite place. -
theorem(proposed):NumberTheory.CyclotomicCharacter.noEverywhereUnramifiedExclude an everywhere-unramified inverse-cyclotomic extension using the required class-field input.