claimroutineinferred_dep

The 2-adic representation r_2 is modular

Shows r2r_2 is modular, from a weight-two newform of level NN
brings modularity into the height bound
Claim·§4.7 Two-dimensional representations and modularity·inside thmHeight bounded by radical of contact primes

Statement (paper)

The representation r2r_2 satisfies the hypotheses of [OddRegularFontaineMazurAtTwo, Theorem 1.1]: it is continuous, absolutely irreducible, odd, unramified outside finitely many primes, and de Rham at 22 with Hodge--Tate weights (cyclotomic exponents) 0,10,1. Consequently r2r_2 is realized by the arithmetic 22-adic representation of a normalized primitive weight-two newform ff, of some level NN, with Tate shift zero (after passing, if necessary, from geometric to arithmetic Frobenius).

In plain English

The two-dimensional 2-adic representation r2r_2 meets the hypotheses of the Fontaine–Mazur-at-2 modularity theorem for odd representations: it is continuous, absolutely irreducible, odd, unramified outside finitely many primes, and de Rham at 22 with Hodge–Tate weights 0,10,1. Hence r2r_2 comes from the arithmetic 2-adic representation of a normalized weight-two newform ff of some level NN, with Tate shift zero.

Why it's here

This is the step that brings modularity into the argument. The representation r2r_2 is a genuine Galois representation by the corrected Tate-module construction, and its ramification control comes from the bounded splitting field of the fiber. The newform ff it produces is then compared with r3r_3 in the compatibility lemma and used to build the modular factor D0D_0 of JJ.
Classified routine:
Checks the hypotheses of the cited Fontaine–Mazur-type modularity theorem for odd 2-adic representations (OddRegularFontaineMazurAtTwo, Thm 1.1) and applies it as a black box. Continuity and irreducibility come from the earlier Tate-module construction, and ramification control from the bounded splitting field.

Uses

claimCorrected Galois representation on Tate modulelemSign-splitting cochain with square-root characterlemBounded splitting field for rational fibers

Used by

lem3-adic and 2-adic representations are compatiblelemModular Jacobian contains A as isogeny factor

Sources

PaperOpen
Section
§4.7 Two-dimensional representations and modularity
Page
—
Label
—
Line
sections/04-height.tex:901
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "r_2 is modular from a weight-two newform" rests on claim-hei-height-5
  • info
    inferred_dep
    outline: "r_2 is modular from a weight-two newform" rests on hei:sign-splitting
  • info
    inferred_dep
    outline: "r_2 is modular from a weight-two newform" rests on hei:fiber-field