Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_X0ModL.lean

definition module

j-expansions and modular function fields over an arbitrary field

Working inside the field of formal Laurent series K((q)) over a field K (and, for the coefficient lemmas, inside R((q)) for a commutative ring R), this module assembles the base-changed version of the project's characteristic-zero q-expansion picture. The series jqModC R of the imported definition module is q^{-1} times the image in R[[q]] of the integral power series jNum = E_4^3\cdot\prod_{n\ge 1}(1-q^n)^{-24}, and jqNModC R N is its image under q\mapsto q^N. The lemmas record that coefficientwise application of a ring homomorphism f\colon R\to S sends ofPowerSeries to ofPowerSeries of the mapped power series, sends jqModC R to jqModC S and jqNModC R N to jqNModC S N; that every coefficient of jqModC R is the image of the corresponding integer coefficient of jqModC ℤ; that jqModC R ^ n equals q^{-n} times the n-th power of the mapped jNum; that the coefficients in degrees < -1 vanish; and that jqModC R is non-zero when R is non-trivial. Over \mathbb{Q} these objects are the rational ones already defined: jqNModC ℚ N = jqN N.

Three definitions are made. First, qExpandAlgHomC K N upgrades the substitution ring homomorphism q\mapsto q^N on K((q)) to a K-algebra homomorphism, the constants \mathrm{single}\;0\;c being fixed. Second, divisorExpansionsC K N is the set of Laurent series \bar j_K(q^d) for the non-zero divisors d of N, and modularFunctionFieldFullC K N is the intermediate field of K((q))/K generated by this set; at K=\mathbb{Q} it is the field modularFunctionFieldFull N. The accompanying inclusions state that the two-generator field modularFunctionFieldC K N lies in it, that N \mid M gives modularFunctionFieldFullC K N ≤ modularFunctionFieldFullC K M, and that the image of modularFunctionFieldFullC K N under qExpandAlgHomC K ℓ lies in modularFunctionFieldFullC K (N * ℓ). Third, JZeroC K N is the group \mathrm{Pic}^0 of that field over K: degree-zero divisors supported on the places of modularFunctionFieldFullC K N (valuation subrings containing K, proper, with principal ideals; degree of a place the residue-field degree over K) modulo principal divisors. No identification with X_0(N) or its Jacobian is asserted here; only the carriers are built, for a field K of any characteristic.

Relation to Mathlib

Mathlib supplies the ambient K((q)) as Hahn series over \mathbb{Z} and the substitution homomorphism through HahnSeries.embDomain; the modular function field presented as a subfield of a Laurent series field, and the divisor class group attached to it, are the project's own notions.

Where it is used

These carriers over a field of characteristic \ell \nmid N are the targets of the reduction map on J_0(N) and of the Eichler–Shimura relation on the special fibre, which enter the level-lowering step of the route to Fermat's Last Theorem.

References

  1. J. Igusa, Kroneckerian model of fields of elliptic modular functions, American Journal of Mathematics 81 (1959), 561–577
  2. P. Deligne and M. Rapoport, Les schémas de modules de courbes elliptiques, in: Modular Functions of One Variable II, Lecture Notes in Mathematics 349, Springer, 1973, 143–316
  3. N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, Annals of Mathematics Studies 108, Princeton University Press, 1985

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_ModularCurve_X0ModL.lean

Imports

Theorems imported by this definition module

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_JqCoeff
import Definitions.Def_ModularCurve_LaurentCoeff
import Definitions.Def_AlgebraicCurve_DivisorClassGroup
import Theorems.Thm_ModularCurve_coeffMap_qExpand
import Theorems.Thm_ModularCurve_coeff_jqModC_pow_self
import Theorems.Thm_ModularCurve_coeff_jqModC_pow_of_lt
import Theorems.Thm_ModularCurve_coeff_jqModC_neg_one

set_option autoImplicit false

noncomputable section

open HahnSeries IntermediateField AlgebraicCurve

namespace ModularCurve

section CoeffMapSupply

variable {R S : Type*} [CommRing R] [CommRing S]

theorem coeffMap_ofPowerSeries (f : R →+* S) (p : PowerSeries R) :
    coeffMap f (HahnSeries.ofPowerSeries ℤ R p) = HahnSeries.ofPowerSeries ℤ S (p.map f) := by
  ext k
  rw [coeffMap_coeff]
  rcases le_or_gt 0 k with hk | hk
  · lift k to ℕ using hk
    rw [HahnSeries.ofPowerSeries_apply_coeff, HahnSeries.ofPowerSeries_apply_coeff,
      PowerSeries.coeff_map]
  · rw [ofPowerSeries_coeff_of_neg _ hk, ofPowerSeries_coeff_of_neg _ hk, map_zero]

end CoeffMapSupply

section JExpansion

variable (R : Type*) [CommRing R]

theorem jqNModC_rat (N : ℕ) [NeZero N] : jqNModC ℚ N = jqN N := rfl

variable {R} in

theorem coeffMap_jqModC {S : Type*} [CommRing S] (f : R →+* S) : coeffMap f (jqModC R) = jqModC S := by
  rw [jqModC, map_mul, coeffMap_single, map_one, coeffMap_ofPowerSeries,
    ← RingHom.comp_apply (PowerSeries.map f) (PowerSeries.map (Int.castRingHom R)),
    ← PowerSeries.map_comp, RingHom.ext_int (f.comp (Int.castRingHom R)) (Int.castRingHom S)]
  rfl

variable {R} in
theorem coeffMap_jqNModC {S : Type*} [CommRing S] (f : R →+* S) (N : ℕ) [NeZero N] :
    coeffMap f (jqNModC R N) = jqNModC S N := by
  rw [jqNModC, coeffMap_qExpand, coeffMap_jqModC, jqNModC]

variable {R} in

theorem coeff_jqModC_eq_intCast (k : ℤ) : (jqModC R).coeff k = (((jqModC ℤ).coeff k : ℤ) : R) := by
  conv_lhs => rw [← coeffMap_jqModC (Int.castRingHom R)]
  rfl

theorem jqModC_pow (n : ℕ) :
    jqModC R ^ n = HahnSeries.single (-(n : ℤ)) 1 *
      HahnSeries.ofPowerSeries ℤ R ((jNum.map (Int.castRingHom R)) ^ n) := by
  have h : n • (-1 : ℤ) = -(n : ℤ) := by simp
  rw [jqModC, mul_pow, HahnSeries.single_pow, one_pow, h, ← map_pow]

theorem coeff_jqModC_of_lt {k : ℤ} (hk : k < -1) : (jqModC R).coeff k = 0 := by
  simpa using coeff_jqModC_pow_of_lt R (b := 1) (m := k) (by simpa using hk)

theorem jqModC_ne_zero_of_nontrivial [Nontrivial R] : jqModC R ≠ 0 := fun h => by
  simpa [h] using coeff_jqModC_neg_one R

end JExpansion

section QExpandAlg

variable (K : Type*) [Field K] (N : ℕ) [NeZero N]

def qExpandAlgHomC : LaurentSeries K →ₐ[K] LaurentSeries K where
  __ := qExpand K N
  commutes' c := by
    show qExpand K N (algebraMap K (LaurentSeries K) c) = algebraMap K (LaurentSeries K) c
    rw [algebraMap_laurentSeries_eq_single, qExpand_single, mul_zero]

@[simp]
theorem qExpandAlgHomC_apply (f : LaurentSeries K) : qExpandAlgHomC K N f = qExpand K N f := rfl

end QExpandAlg

section FunctionField

variable (K : Type*) [Field K] (N : ℕ) [NeZero N]

def divisorExpansionsC : Set (LaurentSeries K) :=
  {x | ∃ (d : ℕ) (_ : NeZero d), d ∣ N ∧ x = qExpand K d (jqModC K)}

omit [NeZero N] in
theorem mem_divisorExpansionsC {d : ℕ} [NeZero d] (hd : d ∣ N) :
    qExpand K d (jqModC K) ∈ divisorExpansionsC K N :=
  ⟨d, ‹_›, hd, rfl⟩

def modularFunctionFieldFullC : IntermediateField K (LaurentSeries K) :=
  IntermediateField.adjoin K (divisorExpansionsC K N)

omit [NeZero N] in

theorem modularFunctionFieldFullC_rat : modularFunctionFieldFullC ℚ N = modularFunctionFieldFull N :=
  rfl

omit [NeZero N] in
theorem jqModCd_mem_full {d : ℕ} [NeZero d] (hd : d ∣ N) :
    qExpand K d (jqModC K) ∈ modularFunctionFieldFullC K N :=
  subset_adjoin K _ (mem_divisorExpansionsC K N hd)

omit [NeZero N] in
theorem jqModC_mem_full : jqModC K ∈ modularFunctionFieldFullC K N := by
  simpa [qExpand_one_apply] using jqModCd_mem_full K N (one_dvd N)

theorem modularFunctionFieldC_le_full : modularFunctionFieldC K N ≤ modularFunctionFieldFullC K N := by
  rw [modularFunctionFieldC, adjoin_le_iff]
  rintro x (rfl | rfl)
  · exact jqModC_mem_full K N
  · exact jqModCd_mem_full K N dvd_rfl

theorem full_degeneracyC_le {N M : ℕ} [NeZero N] [NeZero M] (h : N ∣ M) :
    modularFunctionFieldFullC K N ≤ modularFunctionFieldFullC K M := by
  rw [modularFunctionFieldFullC, adjoin_le_iff]
  rintro x ⟨d, hne, hdvd, rfl⟩
  haveI := hne
  exact jqModCd_mem_full K M (hdvd.trans h)

omit [NeZero N] in

theorem full_degeneracyC_map_le (ℓ : ℕ) [NeZero ℓ] :
    (modularFunctionFieldFullC K N).map (qExpandAlgHomC K ℓ) ≤ modularFunctionFieldFullC K (N * ℓ) := by
  rw [modularFunctionFieldFullC, adjoin_map, adjoin_le_iff]
  rintro x ⟨y, ⟨d, hne, hdvd, rfl⟩, rfl⟩
  haveI := hne
  haveI : NeZero (ℓ * d) := ⟨Nat.mul_ne_zero (NeZero.ne ℓ) (NeZero.ne d)⟩
  show qExpandAlgHomC K ℓ (qExpand K d (jqModC K)) ∈ _
  rw [qExpandAlgHomC_apply, qExpand_qExpand]
  exact jqModCd_mem_full K (N * ℓ) ((mul_dvd_mul_left ℓ hdvd).trans (dvd_of_eq (mul_comm ℓ N)))

end FunctionField

section Jacobian

variable (K : Type*) [Field K] (N : ℕ) [NeZero N]

abbrev JZeroC : Type _ := Pic0 K (modularFunctionFieldFullC K N)

example : AddCommGroup (JZeroC K N) := inferInstance

end Jacobian

end ModularCurve

end

Statements phrased using this module (132)