lemmaroutineinferred_dep

Modular Jacobian contains A as isogeny factor

Shows JJ is isogenous to A×D0A\times D_0 over L′L'
lets the height of A be bounded through J
Lemma·hei:modular-factor·§4.9 The modular factor and the final height bound

Statement (paper)

There is an abelian variety D0/L′D_0/L' such that J∼L′A×D0. J\sim_{L'}A\times D_0.

In plain English

There is an abelian variety D0D_0 over L′L' such that the modular Jacobian JJ is L′L'-isogenous to A×D0A\times D_0, so AA is an isogeny factor of JJ over L′L'.

Why it's here

Since r2r_2 comes from a newform ff of level NN, the abelian variety AA is identified with a piece of JJ, and D0D_0 is the complementary factor. This lets the height of AA be bounded through the height and dimension of JJ, which are polynomially controlled in NN, 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.

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

  • info
    inferred_dep
    critique: 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".