Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_PrimeNormIndex_AdmissibleExpAt.lean

definition module

Admissible exponents and admissible moduli at a prime degree

Over a number field K and a field L carrying a K-algebra structure, this module introduces a one-prime variant of the admissibility conditions on a modulus used in the Artin-reciprocity part of the project.

For a natural number \ell and a finite place v of K (an element of the height-one spectrum of \mathcal{O}_K, i.e. a nonzero prime ideal v.\mathrm{asIdeal}), admissibleExpAt K ℓ v is the natural number 2\,e_v(\ell)+1, where e_v(\ell) denotes Ideal.ramificationIdx' of v.\mathrm{asIdeal} over the ideal (\ell) of \mathbb{Z} generated by the image of \ell. In particular the exponent is 1 at every place not lying above \ell.

The predicate IsAdmissibleModulusAt K L ℓ 𝔣 on an ideal \mathfrak{f}\subseteq\mathcal{O}_K asserts two things: \mathfrak{f}\neq 0, and for every finite place v of K whose chosen prime primeAbove K L v of \mathcal{O}_L has nontrivial inertia subgroup inside L\simeq_{\mathrm{alg}[K]}L, the power v.\mathrm{asIdeal}^{\,2e_v(\ell)+1} divides \mathfrak{f}.

The remaining declarations compare this with the degree-24 exponent \mathrm{admissibleExp}_K(v)=4\,e_v(2)+2\,e_v(3)+1 and the predicate IsAdmissibleModulus of the imported Artin module: admissibleExpAt_two_le and admissibleExpAt_three_le give 2e_v(2)+1\le \mathrm{admissibleExp}_K(v) and 2e_v(3)+1\le\mathrm{admissibleExp}_K(v) at every v, and isAdmissibleModulusAt_two, isAdmissibleModulusAt_three deduce that any modulus admissible in the degree-24 sense is admissible at \ell=2 and at \ell=3. Finally IsAdmissibleModulusAt.of_dvd records that admissibility at \ell propagates upwards: if \mathfrak{f} is admissible at \ell and \mathfrak{f}\mid\mathfrak{f}' with \mathfrak{f}'\neq 0, then \mathfrak{f}' is admissible at \ell.

Relation to Mathlib

Mathlib has no notion of an admissible modulus for an extension; both the exponent and the predicate are the project's own, stated in terms of Mathlib's height-one spectrum of \mathcal{O}_K, the ramification index Ideal.ramificationIdx' and the inertia subgroup of a prime.

Where it is used

These divisibility conditions at the ramified places are the shape of modulus under which the ray-class Artin symbol of the imported LanglandsTunnell.P2.Artin development is used: an exponent 2e_v(\ell)+1 at v makes local units congruent to 1 modulo v^{2e_v(\ell)+1} into \ell-th powers, hence local norms from an abelian layer of degree \ell. They serve the abelian class field theory input to the Langlands–Tunnell step used for the modularity of the mod-3 representation attached to a Frey curve.

References

  1. J.-P. Serre, Local Fields, Graduate Texts in Mathematics 67, Springer, 1979
  2. E. Artin and J. Tate, Class Field Theory, Benjamin, 1968

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_PrimeNormIndex_AdmissibleExpAt.lean

Imports

Imported by

Declarations

Source

import Definitions.Def_LanglandsTunnell_ArtinCoreCTM

set_option autoImplicit false

noncomputable section

open IsDedekindDomain
open LanglandsTunnell.P2.Artin

namespace NumberField.PrimeNormIndex

variable (K L : Type*) [Field K] [NumberField K] [Field L] [Algebra K L]

def admissibleExpAt (ℓ : ℕ) (v : HeightOneSpectrum (𝓞 K)) : ℕ :=
  2 * Ideal.ramificationIdx' (Ideal.span {(ℓ : ℤ)}) v.asIdeal + 1

def IsAdmissibleModulusAt (ℓ : ℕ) (𝔣 : Ideal (𝓞 K)) : Prop :=
  𝔣 ≠ ⊥ ∧ ∀ v : HeightOneSpectrum (𝓞 K),
    (primeAbove K L v).inertia (L ≃ₐ[K] L) ≠ ⊥ → v.asIdeal ^ admissibleExpAt K ℓ v ∣ 𝔣

omit [NumberField K] in

theorem admissibleExpAt_two_le (v : HeightOneSpectrum (𝓞 K)) :
    admissibleExpAt K 2 v ≤ admissibleExp K v := by
  unfold admissibleExpAt admissibleExp
  rw [show ((2 : ℕ) : ℤ) = (2 : ℤ) by norm_num]
  omega

omit [NumberField K] in

theorem admissibleExpAt_three_le (v : HeightOneSpectrum (𝓞 K)) :
    admissibleExpAt K 3 v ≤ admissibleExp K v := by
  unfold admissibleExpAt admissibleExp
  rw [show ((3 : ℕ) : ℤ) = (3 : ℤ) by norm_num]
  omega

theorem isAdmissibleModulusAt_two {𝔣 : Ideal (𝓞 K)} (h : IsAdmissibleModulus K L 𝔣) :
    IsAdmissibleModulusAt K L 2 𝔣 :=
  ⟨h.1, fun v hv => dvd_trans (pow_dvd_pow _ (admissibleExpAt_two_le K v)) (h.2 v hv)⟩

theorem isAdmissibleModulusAt_three {𝔣 : Ideal (𝓞 K)} (h : IsAdmissibleModulus K L 𝔣) :
    IsAdmissibleModulusAt K L 3 𝔣 :=
  ⟨h.1, fun v hv => dvd_trans (pow_dvd_pow _ (admissibleExpAt_three_le K v)) (h.2 v hv)⟩

theorem IsAdmissibleModulusAt.of_dvd {ℓ : ℕ} {𝔣 𝔣' : Ideal (𝓞 K)}
    (h : IsAdmissibleModulusAt K L ℓ 𝔣) (hd : 𝔣 ∣ 𝔣') (h0 : 𝔣' ≠ ⊥) :
    IsAdmissibleModulusAt K L ℓ 𝔣' :=
  ⟨h0, fun v hv => (h.2 v hv).trans hd⟩

end NumberField.PrimeNormIndex

end

Statements phrased using this module (3)