Forms and representations together

One statement asks for curve data and form data to agree inside a residue world.

Start with a concrete example

13 and 18 differ by 5, so both leave 3 after division by 5. The modular-representation definition also compares arithmetic data after passing to a specified remainder setting; it is not equality of the original values.

A small check: try the idea

Think with the concrete example above. You can try again.

13 and 18 both leave 3 when divided by 5. Are the original integers equal?

Read the answer and reasoning

No. 18−13=5. Their difference is divisible by 5, which explains equal remainders without equality of the original numbers.

Build the idea in three steps

Two strands of the story can finally be compared: the curve attached to the Frey package, and the coefficients of a cusp form.
ModularRepOfLevel bundles one request: exhibit a normalized eigenform f, an integral model W of the Frey curve, and a maximal ideal 𝔪 containing p.
At each qualifying prime ℓ, the form’s coefficient and the curve’s arithmetic number must land in the same residue class modulo 𝔪. One Prop statement collects all of these demands.

A small example

13 and 18 have the same remainder 3 modulo 5, since their difference is 5. The formal definition compares arithmetic data modulo the chosen ideal 𝔪; that agreement need not be equality before reduction.

Lean definition · original excerpt

FLT · aa2d8b3 · Def_FLTPrelim_ModularRep.lean

62def ModularRepOfLevel (P : FreyPackage) (N : ℕ) : Prop :=63  ∃ (f : CuspForm (CongruenceSubgroup.Gamma0 N) 2) (W : WeierstrassCurve ℤ)64      (𝔪 : Ideal (integralClosure ℤ ℂ)),65    f.IsNormalizedEigenform ∧ W.IsIntegralModelOf P.freyCurve ∧66    𝔪.IsMaximal ∧ (P.p : integralClosure ℤ ℂ) ∈ 𝔪 ∧67    ∀ ℓ : ℕ, ℓ.Prime → W.IsGoodPrimeFor ℓ → ¬ ℓ ∣ N → ℓ ≠ P.p →68      ∃ a : integralClosure ℤ ℂ, (a : ℂ) = ModularFormClass.qCoeff f ℓ ∧69        a - ((W.apOfModel ℓ : ℤ) : integralClosure ℤ ℂ) ∈ 𝔪

How to read this Lean

∃ asks for the three witnesses f, W and 𝔪, and ∧ joins the conditions. The names IsNormalizedEigenform and IsIntegralModelOf point at their own prerequisite pages.

Original source ↗ · L62–69 Open the complete saved source

Where this idea is used

11. Borrow a better passport

Forms and representations together

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