funlean.
Step 57 / 64

University

Conductor and level lowering

Track problematic primes and use proved conditions to restrict the level.

Start with a concrete example

A product 2×3×5 records three prime labels, while 2²×3 also records a repeated label. A conductor records arithmetic information at primes, with exponents. It is not permission to erase any label we dislike.

A small check: try the idea

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

May the proof remove any prime label from a conductor just because it is inconvenient?

Read the answer and reasoning

No; the theorem’s local conditions must be justified. A label records arithmetic information. Removing it requires the relevant proved conditions; changing a tag by hand is not a theorem.

Build the idea in three steps

  1. A curve can behave differently at different primes. Its conductor records bad-reduction information, including multiplicities.
  2. For semistable curves those contributions are constrained. Here the definition requires every prime dividing Δ to divide the selected modular level.
  3. Level lowering needs further proved local conditions to remove prime factors; it does not let us delete arbitrary factors.

A small example

The luggage tags represent relevant primes. Checking a tag before removing it represents supplying the theorem’s local hypotheses.

Lean definition · original excerpt

FLT · aa2d8b3 · Def_FLTPrelim_ModularRep.lean

def IsModularModelOfConductorLevel (W : WeierstrassCurve ℤ) : Prop :=  ∃ N : ℕ, 0 < N ∧ W.IsModularModelOfLevel N ∧    ∀ ℓ : ℕ, ℓ.Prime → (ℓ : ℤ) ∣ W.Δ → ℓ ∣ N

How to read this Lean

This defines a conductor-level condition on a modular model, not the full conductor invariant. The last line requires each prime dividing Δ to divide the level.

Original source ↗ · L85–87Open the complete saved source

Where this idea is used

14. The shrinking reservation16. The room with no room
I’m lost · Help

Mika’s help desk

Conductor and level lowering

One thing at a time

Read the three explanation steps first. The Lean source is there for a closer look afterwards; you do not have to read it first.

In simpler words

Track problematic primes and use proved conditions to restrict the level.

Earlier ideas are listed under “Start with these ideas” on this page.

A small clue

The luggage tags represent relevant primes. Checking a tag before removing it represents supplying the theorem’s local hypotheses.

Close this panel to return to the exact place you were reading. These are prepared hints for this page.

Start with the first small story →