Mazur's rational torsion theorem

3. 03 — Shared algebraic geometry and isogenies🔗

Theorem3.1
Group: Reusable divisor, cohomology, Picard, Jacobian, Abel–Jacobi, and isogeny infrastructure, developed upstream where possible. Stage weight: 300 points. (12)
Group member previews
Preview
Theorem 3.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1XL∃∀N
EffortlargePriorityhighTagsupstreamopencompiledtau-ceti

Finite support of orders of rational functions. A nonzero rational function on a Noetherian integral scheme has nonzero order at only finitely many codimension-one points.

Status: open; scope: exact compiled Tau Ceti challenge contract. The target is TauCeti.AlgebraicGeometry.SchemeWeilDivisor.finite_support_orderAt, with challenge bridge MazurTauCetiChallenge.finite_support_orderAt; it instantiates Tau Ceti's existing OrderSystem.

Theorem3.2
Group: Reusable divisor, cohomology, Picard, Jacobian, Abel–Jacobi, and isogeny infrastructure, developed upstream where possible. Stage weight: 300 points. (12)
Group member previews
Preview
Theorem 3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1XL∃∀N
EffortlargePriorityhighTagsupstreamblockedstatement-onlytau-ceti

Degree-zero product formula. Every principal divisor on a proper smooth geometrically integral curve has residue-degree-weighted degree zero.

Status: blocked.

Canonical deliverables — these names are authoritative for this node:

  • theorem (proposed): TauCeti.AlgebraicGeometry.SchemeWeilDivisor.orderSystem_isWeightedDegreeZero State and prove the residue-degree-weighted product formula for every nonzero rational function on a proper smooth curve.

Theorem3.3
Group: Reusable divisor, cohomology, Picard, Jacobian, Abel–Jacobi, and isogeny infrastructure, developed upstream where possible. Stage weight: 300 points. (12)
Group member previews
Preview
Theorem 3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1XL∃∀N
EffortmediumPriorityhighTagsupstreamopencompiledtau-ceti

Dimension of a product of abelian varieties. Tau Ceti's abelian-variety dimension is additive under its product construction.

Status: open; scope: exact compiled Tau Ceti challenge contract. The target is TauCeti.AlgebraicGeometry.AbelianVariety.prod_dim, with challenge bridge MazurTauCetiChallenge.prod_dim.

Definition3.4
Group: Reusable divisor, cohomology, Picard, Jacobian, Abel–Jacobi, and isogeny infrastructure, developed upstream where possible. Stage weight: 300 points. (12)
Group member previews
Preview
Theorem 3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 3
Reverse dependency previews
Preview
Definition 3.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
XL∃∀N
EffortlargePriorityhighTagsupstreamblockednouns-missingtau-ceti

Divisor–line-bundle dictionary. Construct the Picard group of line bundles and identify divisor classes with line bundles on a smooth curve.

Status: blocked.

Canonical deliverables — these names are authoritative for this node:

  • structure (proposed): TauCeti.AlgebraicGeometry.PicardGroup Expose line bundles modulo isomorphism as the Picard group of a smooth proper curve.

  • theorem (proposed): TauCeti.AlgebraicGeometry.SchemeWeilDivisor.classEquivPicard Identify Weil divisors modulo principal divisors with the line-bundle Picard group.

Definition3.5
Group: Reusable divisor, cohomology, Picard, Jacobian, Abel–Jacobi, and isogeny infrastructure, developed upstream where possible. Stage weight: 300 points. (12)
Group member previews
Preview
Theorem 3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 3.6
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
XL∃∀N
EffortlargePriorityhighTagsupstreamblockednouns-missingtau-ceti

Coherent cohomology of proper curves. Build finite-dimensional coherent cohomology, affine acyclicity, and vanishing above degree one.

Status: blocked.

Canonical deliverables — these names are authoritative for this node:

  • definition (proposed): TauCeti.AlgebraicGeometry.CurveCohomology Define degree-zero and degree-one coherent cohomology for sheaves on proper curves.

  • theorem (proposed): TauCeti.AlgebraicGeometry.CurveCohomology.finiteDimensional Prove finite dimensionality, affine acyclicity, and vanishing above degree one in the required scope.

Theorem3.6
Group: Reusable divisor, cohomology, Picard, Jacobian, Abel–Jacobi, and isogeny infrastructure, developed upstream where possible. Stage weight: 300 points. (12)
Group member previews
Preview
Theorem 3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1XL∃∀N
EffortlargePriorityhighTagsupstreamblockednouns-missingtau-ceti

Riemann–Roch and Serre duality for curves. Define genus through H^1 and prove Riemann–Roch, Serre duality, and the degree of the dualizing sheaf.

Status: blocked.

Canonical deliverables — these names are authoritative for this node:

  • definition (proposed): TauCeti.AlgebraicGeometry.Curve.genus Define the genus of a proper smooth curve from the dimension of first coherent cohomology.

  • theorem (proposed): TauCeti.AlgebraicGeometry.Curve.riemannRoch Provide the Riemann-Roch formula for divisors or line bundles on a proper smooth curve.

  • theorem (proposed): TauCeti.AlgebraicGeometry.Curve.serreDuality Provide Serre duality and the resulting degree formula for the dualizing sheaf.

Definition3.7
Group: Reusable divisor, cohomology, Picard, Jacobian, Abel–Jacobi, and isogeny infrastructure, developed upstream where possible. Stage weight: 300 points. (12)
Group member previews
Preview
Theorem 3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 3
Reverse dependency previews
Preview
Definition 3.8
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
XL∃∀N
EffortlargePriorityhighTagsupstreamblockednouns-missingtau-ceti

Relative cohomology and base change. Provide proper-flat pushforward, cohomology-and-base-change, and semicontinuity in the form needed by Picard.

Status: blocked.

Canonical deliverables — these names are authoritative for this node:

  • definition (proposed): TauCeti.AlgebraicGeometry.RelativeCohomology Package derived pushforward data for coherent sheaves in a proper flat family of curves.

  • theorem (proposed): TauCeti.AlgebraicGeometry.RelativeCohomology.baseChange Prove the base-change comparison required by the relative Picard construction.

  • theorem (proposed): TauCeti.AlgebraicGeometry.RelativeCohomology.upperSemicontinuous Prove upper semicontinuity of fibrewise cohomology dimensions in the required setting.

Definition3.8
Group: Reusable divisor, cohomology, Picard, Jacobian, Abel–Jacobi, and isogeny infrastructure, developed upstream where possible. Stage weight: 300 points. (12)
Group member previews
Preview
Theorem 3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 3.4
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1XL∃∀N
EffortlargePriorityhighTagsupstreamblockednouns-missingtau-ceti

Relative effective divisors and symmetric powers. Represent degree-d effective divisors by \operatorname{Sym}^d X and construct relative Abel maps.

Status: blocked.

Canonical deliverables — these names are authoritative for this node:

  • structure (proposed): TauCeti.AlgebraicGeometry.RelativeEffectiveDivisor Represent flat families of effective divisors of a fixed relative degree.

  • definition (proposed): TauCeti.AlgebraicGeometry.SymmetricPower Construct the relative symmetric power that represents effective divisors of degree d.

  • definition (proposed): TauCeti.AlgebraicGeometry.relativeAbelMap Construct the relative Abel map from the symmetric power to the degree-d Picard functor.

Definition3.9
Group: Reusable divisor, cohomology, Picard, Jacobian, Abel–Jacobi, and isogeny infrastructure, developed upstream where possible. Stage weight: 300 points. (12)
Group member previews
Preview
Theorem 3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 3.4
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1XL∃∀N
EffortlargePriorityhighTagsupstreamblockednouns-missingtau-ceti

Rigidified relative Picard functor. Define the fppf Picard sheaf, its degree-zero subfunctor, rigidification, and Poincaré line bundle.

Status: blocked.

Canonical deliverables — these names are authoritative for this node:

  • definition (proposed): TauCeti.AlgebraicGeometry.RelativePicardFunctor Define the rigidified fppf sheaf of line bundles modulo pullbacks from the base.

  • definition (proposed): TauCeti.AlgebraicGeometry.RelativePicardFunctor.degreeZero Define the degree-zero subfunctor used to construct the relative Jacobian.

  • structure (proposed): TauCeti.AlgebraicGeometry.PoincareBundle Package the normalized universal line bundle on the curve times its Picard space.

Theorem3.10
Group: Reusable divisor, cohomology, Picard, Jacobian, Abel–Jacobi, and isogeny infrastructure, developed upstream where possible. Stage weight: 300 points. (12)
Group member previews
Preview
Theorem 3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Theorem 3.6
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1XL∃∀N
EffortlargePriorityhighTagsupstreamblockednouns-missingtau-ceti

Representability and properness of \mathrm{Pic}^0. Represent the degree-zero Picard functor and prove that its group scheme is proper and geometrically connected.

Status: blocked.

Canonical deliverables — these names are authoritative for this node:

  • structure (proposed): TauCeti.AlgebraicGeometry.PicardScheme Package a group scheme representing the degree-zero relative Picard functor.

  • theorem (proposed): TauCeti.AlgebraicGeometry.PicardScheme.representsDegreeZero Prove the representing equivalence between points of PicardScheme and the degree- zero Picard functor.

  • theorem (proposed): TauCeti.AlgebraicGeometry.PicardScheme.proper_geometricallyConnected Prove properness and geometric connectedness of the represented degree-zero component.

Definition3.11
Group: Reusable divisor, cohomology, Picard, Jacobian, Abel–Jacobi, and isogeny infrastructure, developed upstream where possible. Stage weight: 300 points. (12)
Group member previews
Preview
Theorem 3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Theorem 3.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 4
Reverse dependency previews
Preview
Theorem 3.12
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
XL∃∀N
EffortlargePriorityhighTagsupstreamblockednouns-missingtau-ceti

Jacobian variety and sanity checks. Bundle \mathrm{Pic}^0 as an abelian variety, prove that its dimension is the genus, and recover an elliptic curve from its pointed genus-one Jacobian.

Status: blocked.

Canonical deliverables — these names are authoritative for this node:

  • structure (proposed): TauCeti.AlgebraicGeometry.Jacobian Package the represented Picard degree-zero component as an abelian variety.

  • theorem (proposed): TauCeti.AlgebraicGeometry.Jacobian.dimension_eq_genus Identify the dimension of the Jacobian with the genus of the curve.

  • theorem (proposed): TauCeti.AlgebraicGeometry.Jacobian.ellipticCurveEquiv Prove the pointed genus-one sanity check identifying an elliptic curve with its Jacobian.

Theorem3.12
Group: Reusable divisor, cohomology, Picard, Jacobian, Abel–Jacobi, and isogeny infrastructure, developed upstream where possible. Stage weight: 300 points. (12)
Group member previews
Preview
Theorem 3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 3.7
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1XL∃∀N
EffortlargePriorityhighTagsupstreamblockednouns-missingtau-ceti

Abel–Jacobi universal property and base change. Construct the Abel–Jacobi morphism, prove its universal property and base-change compatibility, and show it is a closed immersion in positive genus.

Status: blocked.

Canonical deliverables — these names are authoritative for this node:

  • definition (proposed): TauCeti.AlgebraicGeometry.Jacobian.abelJacobi Construct the pointed Abel-Jacobi morphism from a curve to its Jacobian.

  • theorem (proposed): TauCeti.AlgebraicGeometry.Jacobian.abelJacobi_universal Prove the universal factorization property for pointed morphisms to abelian varieties.

  • theorem (proposed): TauCeti.AlgebraicGeometry.Jacobian.abelJacobi_baseChange Prove compatibility of the Abel-Jacobi construction with base change.

  • theorem (proposed): TauCeti.AlgebraicGeometry.Jacobian.abelJacobi_closedImmersion Prove that Abel-Jacobi is a closed immersion for curves of positive genus.

Definition3.13
Group: Reusable divisor, cohomology, Picard, Jacobian, Abel–Jacobi, and isogeny infrastructure, developed upstream where possible. Stage weight: 300 points. (12)
Group member previews
Preview
Theorem 3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 4
Reverse dependency previews
Preview
Definition 4.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
XL∃∀N
EffortlargePriorityhighTagsinfrastructureplannednouns-missingmathlib

Elliptic-curve isogenies, quotients, duals, and Weil pairing. Supply finite-subgroup quotients, dual isogenies, multiplication kernels, and the Weil pairing, all compatible with base change.

Status: planned.

Canonical deliverables — these names are authoritative for this node:

  • structure (proposed): EllipticCurve.Isogeny Package finite morphisms of elliptic curves with their group-homomorphism and degree data.

  • definition (proposed): EllipticCurve.quotientByFiniteSubgroup Construct the quotient elliptic curve and quotient isogeny for a finite subgroup scheme.

  • definition (proposed): EllipticCurve.Isogeny.dual Construct the dual isogeny and prove both composites are multiplication by the degree.

  • definition (proposed): EllipticCurve.weilPairing Define the Weil pairing on multiplication kernels with functoriality and nondegeneracy.