Modularity of a curve

Find a qualifying form whose coefficients match the curve’s arithmetic data.

Start with a concrete example

Two people describe the same object in different ways. One records 2, −1, 4; the other records 2, −1, 4. Select a position to compare the records.

Move the number or condition

Position 1: both records contain 2. A few matches are not the full theorem.

How this example differs from the definition

This invented three-number record illustrates comparison only. Modularity needs an actual qualifying form and the full required correspondence, not agreement at three sample positions.

A small check: try the idea

Compare the numbers in the question with the diagram you are moving. You can try again.

In our toy records, does agreement at three positions prove the full modularity theorem?

Read the answer and reasoning

No; the actual object and full required correspondence still matter. Select each record position. These invented data illustrate comparison, not the existence of a qualifying form or the full theorem.

Build the idea in three steps

The curve yields arithmetic numbers at suitable primes. A form yields coefficients at those same primes.
Modularity asks for a qualifying normalized form whose coefficients exactly match the curve’s numbers where the definition requires it.
The level also has to exist and be positive. Finding this partner is a theorem, not a consequence of drawing two matching instruments.

A small example

The duet is the exact equality qCoeff f p = apOfModel W p at the specified good primes.

Lean definition · original excerpt

FLT · aa2d8b3 · Def_FLTPrelim_Modularity.lean

93def IsModularModelOfLevel (W : WeierstrassCurve ℤ) (N : ℕ) : Prop :=94  ∃ f : CuspForm (CongruenceSubgroup.Gamma0 N) 2, f.IsNormalizedEigenform ∧95    ∀ p : ℕ, p.Prime → W.IsGoodPrimeFor p → ¬ p ∣ N →96      ModularFormClass.qCoeff f p = (W.apOfModel p : ℂ)97 98def IsModularModel (W : WeierstrassCurve ℤ) : Prop :=99  ∃ N : ℕ, 0 < N ∧ W.IsModularModelOfLevel N100 101def IsModular (E : WeierstrassCurve ℚ) : Prop :=102  ∃ W : WeierstrassCurve ℤ, W.IsIntegralModelOf E ∧ W.IsModularModel

How to read this Lean

∃ f supplies a form; ∧ bundles its conditions; ∀ p specifies the primes; the final = is the matching condition. The next definition supplies a positive level N.

Original source ↗ · L93–102 Open the complete saved source

Where this idea is used

8. The secret duet 9. Two doors to the concert 10. A three-note audition 11. Borrow a better passport 12. The workshops agree 13. Pip’s impossible quilt 14. The shrinking reservation

Modularity of a curve

Start with a concrete example

A small check: try the idea

Build the idea in three steps

A small example

Lean definition · original excerpt

How to read this Lean

Where this idea is used

Mika’s help desk

One thing at a time

In simpler words

A small clue