Residual modularity

Match arithmetic data after passing to a residue setting.

Start with a concrete example

Imagine two records that show 8 and 5. They differ, but both leave 2 when divided by 3. Move the first number: when do the remainders match?

Move the number or condition

Left remainder 2; right remainder 2. They match.

How this example differs from the definition

These two integers illustrate one comparison only. Actual residual modularity requires a qualifying form and the specified arithmetic correspondence; one matching pair is not enough.

A small check: try the idea

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

8 and 5 both leave 2 after division by 3. What can we conclude from this small example?

Read the answer and reasoning

Their remainders agree, although the full values differ. Compare 8 ÷ 3 and 5 ÷ 3 in the diagram. Matching remainders forgets part of the original information; this pair alone is not a proof of residual modularity.

Build the idea in three steps

You already have two arithmetic data sources: a curve and a form.
Now compare them after passing to a residue setting rather than demanding exact equality. For integers, same-remainder arithmetic is the entry example.
The definition uses algebraic integers: roots of polynomial equations with integer coefficients and leading coefficient one. Their addition and multiplication form a ring. An ideal collects values treated as zero in residue arithmetic and stays closed under addition and multiplication by ring elements. The chosen maximal ideal gives a residue system in which nonzero residues can be divided by. This extends the ordinary integer example.

A small example

In ordinary arithmetic, 7 − 2 is a multiple of 5. In the definition, the difference belongs to an ideal 𝔪 containing p.

Lean definition · original excerpt

FLT · aa2d8b3 · Def_FLTPrelim_ModularRep.lean

75def IsResiduallyModularOfLevel (W : WeierstrassCurve ℤ) (p M : ℕ) : Prop :=76  ∃ (f : CuspForm (CongruenceSubgroup.Gamma0 M) 2) (𝔪 : Ideal (integralClosure ℤ ℂ)),77    f.IsNormalizedEigenform ∧ 𝔪.IsMaximal ∧ (p : integralClosure ℤ ℂ) ∈ 𝔪 ∧78    ∀ ℓ : ℕ, ℓ.Prime → W.IsGoodPrimeFor ℓ → ¬ ℓ ∣ M → ℓ ≠ p →79      ∃ a : integralClosure ℤ ℂ, (a : ℂ) = ModularFormClass.qCoeff f ℓ ∧80        a - ((W.apOfModel ℓ : ℤ) : integralClosure ℤ ℂ) ∈ 𝔪81 82def IsResiduallyModular (W : WeierstrassCurve ℤ) (p : ℕ) : Prop :=83  ∃ M : ℕ, 0 < M ∧ W.IsResiduallyModularOfLevel p M

How to read this Lean

The witness 𝔪 is a maximal ideal containing p. The final difference ∈ 𝔪 expresses residual agreement. IsResiduallyModular then asks for a positive level.

Original source ↗ · L75–83 Open the complete saved source

Where this idea is used

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

Residual modularity

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