lemmaroutineinferred_dep
Modular Jacobian contains A as isogeny factor
Shows is isogenous to over
lets the height of A be bounded through J
Lemma·
hei:modular-factor·§4.9 The modular factor and the final height boundStatement (paper)
There is an abelian variety such that
In plain English
There is an abelian variety over such that the modular Jacobian is -isogenous to , so is an isogeny factor of over .
Why it's here
Since comes from a newform of level , the abelian variety is identified with a piece of , and is the complementary factor. This lets the height of be bounded through the height and dimension of , which are polynomially controlled in , in the later height-bound steps.
Classified routine:
Follows from the Eichler–Shimura construction: the newform f gives an abelian variety A_f that is an isogeny factor of J_0(N) (Shimura), combined with Faltings' isogeny theorem to identify A with A_f over L' once r_2 is known to be modular.
Uses
Used by
Sources
PaperOpen
- Section
- §4.9 The modular factor and the final height bound
- Page
- —
- Label
hei:modular-factor- Line
sections/04-height.tex:1170
Leannot aligned
Phase 2 aligns this node to a Lean declaration.
Friction
- infoinferred_depcritique: The proof of hei:modular-factor uses that r_2 is realized by the newform f of level N inside V_2(J_1(N)) (04-height.tex:1162-1180). That fact is established in the claim "r_2 is modular from a weight-two newform".