Automorphic.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

5 declarations, 2 contain sorry, 0 declared as axioms

Automorphic Galois representations

For our proof of Fermat's Last Theorem, the following definition is the most convenient.

We say that a 2-dimensional $p$-adic or a mod $p$ Galois representation of the absolute Galois of a totally real field number field $F$ of even degree is automorphic if there exists a totally definite quaternion algebra $D/F$ unramified at all finite places, a finite set $S$ of finite places of $F$, and an automorphic form of level $U_1(S)$ (matrices congruent to $(a *;0 a)$ mod $v$ for all $v\in S$) and weight 2 for $D$ such that the Galois representation is associated to the form by the construction of Carayol, Taylor et al.

Notes

Several things here are specialized to our case. We demand that the quaternion algebra is unramified everywhere because this is the only case that we need. We stick to weight 2 because this is the only case that we need. The level is also more restrictive but again the only thing we need: the automorphic forms it catches are trivial at all infinite places and at all finite places are either Steinberg or principal series π(χ₁, χ₂) with χᵢ tame and χ₁χ₂ unramified.

Imports (6)

Imported by 1 file

FLT.lean

def GaloisRep.IsAutomorphicOfLevel Documented declaration: IsAutomorphicOfLevel line 67 source
Source documentation
A 2-dimensional Galois representation ρ of the absolute Galois group of a totally real field of even degree is said to be automorphic if it comes from a weight 2 trivial character square-free level automorphic form on a totally definite quaternion algebra of discriminant 1. More precisely, the level at each bad prime v has to be of the form (a *;0 a) mod v.
This is a far more restrictive definition of automorphic than is found in the literature, however it will suffice for the purpose of proving FLT.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, NumberField.IsTotallyReal, Nat, Fact, Nat.Prime, LT.lt, OfNat.ofNat, Module.finrank, CyclotomicField, CommRing, TopologicalSpace, Algebra, PadicInt, ContinuousSMul, AddCommGroup, Module, Module.Finite, Module.Free, Eq and 4 more
Proof uses: Exists, DivisionRing, IsQuaternionAlgebra, IsQuaternionAlgebra.NumberField.WithRigidification, AlgHom, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, TotallyDefiniteQuaternionAlgebra.U₁Data.mk, EmptyCollection.emptyCollection, MonoidHom, Units, IsLocalRing.ResidueField, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Not, Ideal, IsDedekindDomain.HeightOneSpectrum.asIdeal, And and 12 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def GaloisRep.IsAutomorphicOfLevel
    -- `F` is a totally real field
    {F : Type u} [Field F] [NumberField F] [IsTotallyReal F]
    (p : ℕ) [Fact p.Prime] (hp : 2 < Module.finrank F (CyclotomicField p F))
    {A : Type*} [CommRing A] [TopologicalSpace A] [Algebra ℤ_[p] A]
    [ContinuousSMul ℤ_[p] A]
    -- `V` is the rank 2 free `A`-module on which the Galois group will act
    {V : Type*} [AddCommGroup V] [Module A V] [Module.Finite A V]
      [Module.Free A V] (_hV : Module.finrank A V = 2)
    -- `ρ` is the Galois representation
    (ρ : GaloisRep F A V)
    -- `S` is the level of the modular form
…
```
Mentions: GaloisRep
instance (instance at line 96) sorry line 96 source
instance (instance at line 103) line 103 source
instance (instance at line 106) line 106 source
theorem cyclic_base_change Cyclic base change sorry line 127 source
Source documentation
Cyclic base change.
Let E/F be a finite solvable extension of totally real fields of even degree, let p>2 be a prime and let ρ : Gal(F-bar/F) -> GL_2(Q_p-bar) be a continuous representation, which is irreducible even when restricted to Gal(E-bar/E). Let S be a finite set of finite places of F, not dividing p.
Suppose furthermore
- ρ unramified outside S and p;
- ρ descends to ρ₀ : Gal(F-bar/F) -> GL_2(R) with R ⊆ ℚ_p-bar a subring finite free over ℤ_p, and ρ₀ is flat at all places of F dividing p;
- If v ∈ S then the restriction of ρ to Fᵥ has a rank one tame quotient;
- det(ρ) is the cyclotomic character.
Then ρ is automorphic of level U₁(S) iff ρ|G_E is automorphic of level U₁(S_E), where S_E is the pullback of S to E.
depends on sorry what this means
Statement uses: Field, NumberField, NumberField.IsTotallyReal, Even, Nat, Module.finrank, Rat, Algebra, IsGalois, Group.IsSolvable, AlgEquiv, Fact, Nat.Prime, LT.lt, OfNat.ofNat, CyclotomicField, AddCommGroup, Module, AlgebraicClosure, Padic and 55 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
202 instances, coercions and auxiliary constants left out.
```
theorem cyclic_base_change
    -- let F be a totally real number field of even degree
    {F : Type*} [Field F] [NumberField F] [IsTotallyReal F]
    (hF : Even (Module.finrank ℚ F))
    -- let E/F be a finite solvable extension
    {E : Type*} [Field E] [NumberField E] [IsTotallyReal E]
    [Algebra F E] [IsGalois F E] [Group.IsSolvable (E ≃ₐ[F] E)]
    -- let p be a prime
    (p : ℕ) [Fact p.Prime] (hp : 2 < Module.finrank F (CyclotomicField p F))
    (hpE : 2 < Module.finrank E (CyclotomicField p E))
    -- let ρ:Gal(F-bar/F)->GL_2(Q_p-bar) be a continuous representation
    {V : Type} [AddCommGroup V] [Module (ℚ_[p]ᵃˡᵍ) V]
…
```