claimroutineinferred_dep

Theta-null height matches Pazuki theta height

Shows theta-null height equals Pazuki theta height up to CrC_r
links theta-null map to Pazuki's height
Claim·§4.4 Comparison of base height and Faltings height·inside lemBase height bounded by Faltings height

Statement (paper)

Fix an even level rr and put k=r2k=r^2. Then there is a constant CrC_r, depending on rr but not on the fiber A=AyA=\mathcal A_y or its field of definition, such that the projective height of the theta-null map at yy (the point with coordinates θ[a,b](τ,0)\theta[a,b](\tau,0), a,b∈(r−1Z2)/Z2a,b\in(r^{-1}\Z^2)/\Z^2, equivalently θ[e/k,0](kτ,0)\theta[e/k,0](k\tau,0), e mod ke \bmod k) differs from Pazuki's theta height of AA by at most CrC_r.

In plain English

For even level rr and k=r2k=r^2, the projective height of the theta-null point (θ[a,b](τ,0))a,b(\theta[a,b](\tau,0))_{a,b}, equivalently (θ[e/k,0](kτ,0))e mod k(\theta[e/k,0](k\tau,0))_{e \bmod k}, differs from Pazuki's theta height of the fiber A=AyA=\mathcal A_y by at most a constant CrC_r independent of AA and its field of definition.

Why it's here

This identifies the height of the theta-null map, which is defined via the algebraic theta data from the previous claim, with Pazuki's theta height up to a bounded error. It is what lets the later claims bound the base height of π(y)\pi(y) in terms of the Faltings height, since Pazuki's theta height is comparable to the Faltings height of AA.
Classified routine:
This comparison follows from the standard relations among theta-null coordinates (the Riemann/isogeny theta relations between θ[a,b](τ,0)\theta[a,b](\tau,0) and θ[e/k,0](kτ,0)\theta[e/k,0](k\tau,0)) together with Pazuki's definition of the theta height. It amounts to bookkeeping that identifies two projective embeddings up to a bounded height difference.

Uses

claimTheta-null data after finite covers

Used by

claimBase height bounded by theta height

Sources

PaperOpen
Section
§4.4 Comparison of base height and Faltings height
Page
—
Label
—
Line
sections/04-height.tex:405
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Theta-null map height equals Pazuki theta height up to constant" rests on claim-hei-base-height-1