Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_SpecializeModuli.lean

definition module

Places of the -line and specialisation of moduli divisors

Throughout, K is a field and \mathrm{jqModC}\ K \in K((q)) is the q-expansion of j with coefficients in K; the level-N field modularFunctionFieldC K N is the intermediate field of K((q)) generated by j(q) and j(q^N), so at N=1 it is K\langle j(q)\rangle. Since j(q) is transcendental over K, ratFuncEquivCharLOneC is the K-algebra isomorphism K(t) \cong modularFunctionFieldC K 1 sending t to j(q). Here Place K F is the project's notion of a place: a valuation subring of F that contains the image of K, is not all of F, and is a principal ideal ring; its degree is the K-dimension of the residue field, divisors are finitely supported \mathbb{Z}-combinations of places, and charLJacobian K N is the group \mathrm{Pic}^0 of degree-zero divisors modulo principal divisors of modularFunctionFieldC K N.

Transport of valuation subrings along the above isomorphism gives a bijection charLGeomPlaceEquiv between places of K(t) and of the level-one modular function field, and charLGeomPlaceOfPoint K a is the image under it of the place of K(t) attached to the prime (X-a). It is injective in a and of degree 1. Extending by Finsupp.mapDomain, charLGeomModuliDictionary K is the injective additive map from K \to_0 \mathbb{Z} to divisors, \sum n_i (a_i) \mapsto \sum n_i\,[j = a_i].

For an arbitrary map of underlying sets r : K \to k between fields, specializePlace r a is [j = r(a)] as a place over k, and specializeModuli r is the additive map \sum n_i (a_i) \mapsto \sum n_i\,[j = r(a_i)], equivalently Finsupp.mapDomain along specializePlace r. Accompanying lemmas compute it on singletons, bound its support, show it is the dictionary itself when r = \mathrm{id}, and show that all places involved have degree 1, whence the degree of the image equals the degree over K and degree-zero divisors are sent to degree-zero divisors. Three further lemmas record equivariance: precomposing the index map with \sigma : K \to K amounts to replacing r by r \circ \sigma; if r \circ \sigma = r the divisor is unchanged; and if r \circ \sigma = \tau \circ r for \tau : k \to k the result is the k-dictionary applied to the pushforward of D along r then \tau.

Relation to Mathlib

The rational function field, IntermediateField.adjoin, RatFunc.algEquivOfTranscendental and Finsupp.mapDomain are Mathlib's; the notions of place, divisor, degree and \mathrm{Pic}^0 of a function field used here are the project's own, defined via valuation subrings containing the base field.

Where it is used

These maps are the carrier of the specialisation of divisors on the j-line from characteristic 0 to characteristic \ell: the intended instance is K = \overline{\mathbb{Q}}, k = \overline{\mathbb{F}}_\ell and r the reduction map at a place above \ell. The degree and equivariance lemmas are what later modules use to descend specialisation to the degree-zero divisor class group and to compare the actions of inertia and Frobenius on both sides.

References

  1. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154
  2. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Publications of the Mathematical Society of Japan 11, Princeton University Press, 1971
  3. H. Stichtenoth, Algebraic Function Fields and Codes, 2nd edition, Graduate Texts in Mathematics 254, Springer, 2009

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

Imports

Theorems imported by this definition module

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_JqCoeff
import Definitions.Def_AlgebraicCurve_RatFuncPlaces
import Theorems.Thm_ModularCurve_transcendental_jqModC

set_option autoImplicit false

noncomputable section

open AlgebraicCurve

namespace ModularCurve

section Transcendence

variable (K : Type*) [Field K]

def ratFuncEquivCharLOneC : RatFunc K ≃ₐ[K] (modularFunctionFieldC K 1) :=
  (RatFunc.algEquivOfTranscendental (jqModC K) (transcendental_jqModC K)).trans
    (IntermediateField.equivOfEq (modularFunctionFieldC_one K).symm)

end Transcendence

section Jacobian

variable (K : Type*) [Field K]

abbrev charLJacobian (N : ℕ) [NeZero N] : Type _ :=
  Pic0 K (modularFunctionFieldC K N)

def charLGeomPlaceEquiv :
    Place K (RatFunc K) ≃ Place K (modularFunctionFieldC K 1) :=
  Place.congrEquiv (ratFuncEquivCharLOneC K).toRingEquiv
    (fun a => (ratFuncEquivCharLOneC K).commutes a)

def charLGeomPlaceOfPoint (a : K) : Place K (modularFunctionFieldC K 1) :=
  charLGeomPlaceEquiv K (RationalFunctionField.placeOfPoint K a)

theorem charLGeomPlaceOfPoint_injective : Function.Injective (charLGeomPlaceOfPoint K) :=
  fun _ _ h => RationalFunctionField.placeOfPoint_injective K
    ((charLGeomPlaceEquiv K).injective h)

theorem deg_charLGeomPlaceOfPoint (a : K) : (charLGeomPlaceOfPoint K a).deg = 1 :=
  (Place.deg_congrRingEquiv (ratFuncEquivCharLOneC K).toRingEquiv
    (fun a => (ratFuncEquivCharLOneC K).commutes a)
    (RationalFunctionField.placeOfPoint K a)).trans
    (RationalFunctionField.deg_placeOfPoint K a)

def charLGeomModuliDictionary :
    (K →₀ ℤ) →+ Divisor K (modularFunctionFieldC K 1) :=
  Finsupp.mapDomain.addMonoidHom (charLGeomPlaceOfPoint K)

theorem charLGeomModuliDictionary_injective :
    Function.Injective (charLGeomModuliDictionary K) :=
  Finsupp.mapDomain_injective (charLGeomPlaceOfPoint_injective K)

@[simp]
theorem charLGeomModuliDictionary_single (a : K) (n : ℤ) :
    charLGeomModuliDictionary K (Finsupp.single a n)
      = Finsupp.single (charLGeomPlaceOfPoint K a) n := by
  simp only [charLGeomModuliDictionary, Finsupp.mapDomain.addMonoidHom_apply,
    Finsupp.mapDomain_single]

end Jacobian

section Map

variable {K k : Type*} [Field K] [Field k]

def specializePlace (r : K → k) (a : K) : Place k (modularFunctionFieldC k 1) :=
  charLGeomPlaceOfPoint k (r a)

omit [Field K] in
@[simp]
theorem specializePlace_def (r : K → k) (a : K) :
    specializePlace r a = charLGeomPlaceOfPoint k (r a) := rfl

omit [Field K] in

theorem deg_specializePlace (r : K → k) (a : K) : (specializePlace r a).deg = 1 :=
  deg_charLGeomPlaceOfPoint k (r a)

omit [Field K] in

theorem specializePlace_eq_of_eq (r : K → k) {a b : K} (h : r a = r b) :
    specializePlace r a = specializePlace r b := by
  simp only [specializePlace, h]

omit [Field K] in

theorem specializePlace_inj_iff (r : K → k) {a b : K} :
    specializePlace r a = specializePlace r b ↔ r a = r b :=
  ⟨fun h => charLGeomPlaceOfPoint_injective k h, specializePlace_eq_of_eq r⟩

def specializeModuli (r : K → k) :
    (K →₀ ℤ) →+ Divisor k (modularFunctionFieldC k 1) :=
  (charLGeomModuliDictionary k).comp (Finsupp.mapDomain.addMonoidHom r)

omit [Field K] in
@[simp]
theorem specializeModuli_single (r : K → k) (a : K) (n : ℤ) :
    specializeModuli r (Finsupp.single a n)
      = Finsupp.single (specializePlace r a) n := by
  simp only [specializeModuli, AddMonoidHom.coe_comp, Function.comp_apply,
    Finsupp.mapDomain.addMonoidHom_apply, Finsupp.mapDomain_single,
    charLGeomModuliDictionary_single, specializePlace_def]

omit [Field K] in

theorem specializeModuli_eq_mapDomain (r : K → k) (D : K →₀ ℤ) :
    specializeModuli r D = Finsupp.mapDomain (specializePlace r) D := by
  simp only [specializeModuli, AddMonoidHom.coe_comp, Function.comp_apply,
    Finsupp.mapDomain.addMonoidHom_apply, charLGeomModuliDictionary,
    Finsupp.mapDomain.addMonoidHom_apply]
  rw [← Finsupp.mapDomain_comp]
  rfl

theorem specializeModuli_id (D : K →₀ ℤ) :
    specializeModuli (id : K → K) D = charLGeomModuliDictionary K D := by
  simp only [specializeModuli, AddMonoidHom.coe_comp, Function.comp_apply,
    Finsupp.mapDomain.addMonoidHom_apply, Finsupp.mapDomain_id]

omit [Field K] in
open scoped Classical in

theorem support_specializeModuli_subset (r : K → k) (D : K →₀ ℤ) :
    (specializeModuli r D).support ⊆ D.support.image (specializePlace r) := by
  rw [specializeModuli_eq_mapDomain]
  exact Finsupp.mapDomain_support

end Map

section Degree

variable {K k : Type*} [Field K] [Field k]

omit [Field K] in

theorem degree_specializeModuli_single (r : K → k) (a : K) (n : ℤ) :
    Divisor.degree (specializeModuli r (Finsupp.single a n)) = n := by
  rw [specializeModuli_single, Divisor.degree_single, deg_specializePlace, Nat.cast_one,
    mul_one]

theorem degree_specializeModuli_eq_degree (r : K → k) (D : K →₀ ℤ) :
    Divisor.degree (specializeModuli r D)
      = Divisor.degree (charLGeomModuliDictionary K D) := by
  have h : (Divisor.degree.comp (specializeModuli r) : (K →₀ ℤ) →+ ℤ)
      = Divisor.degree.comp (charLGeomModuliDictionary K) := by
    refine Finsupp.addHom_ext fun a n => ?_
    simp only [AddMonoidHom.coe_comp, Function.comp_apply, specializeModuli_single,
      charLGeomModuliDictionary_single, Divisor.degree_single, deg_specializePlace,
      deg_charLGeomPlaceOfPoint]
  exact DFunLike.congr_fun h D

theorem specializeModuli_mem_degZero (r : K → k) {D : K →₀ ℤ}
    (hD : Divisor.degree (charLGeomModuliDictionary K D) = 0) :
    Divisor.degree (specializeModuli r D) = 0 := by
  rw [degree_specializeModuli_eq_degree, hD]

end Degree

section Galois

variable {K k : Type*} [Field K] [Field k]

omit [Field K] in

theorem specializeModuli_mapDomain (r : K → k) (σ : K → K) (D : K →₀ ℤ) :
    specializeModuli r (Finsupp.mapDomain σ D) = specializeModuli (r ∘ σ) D := by
  rw [specializeModuli_eq_mapDomain, specializeModuli_eq_mapDomain,
    ← Finsupp.mapDomain_comp]
  rfl

omit [Field K] in

theorem specializeModuli_inertia_invariant (r : K → k) (σ : K → K)
    (hσ : ∀ a, r (σ a) = r a) (D : K →₀ ℤ) :
    specializeModuli r (Finsupp.mapDomain σ D) = specializeModuli r D := by
  rw [specializeModuli_mapDomain, show (r ∘ σ) = r from funext hσ]

omit [Field K] in

theorem specializeModuli_intertwines (r : K → k) (σ : K → K) (τ : k → k)
    (h : ∀ a, r (σ a) = τ (r a)) (D : K →₀ ℤ) :
    specializeModuli r (Finsupp.mapDomain σ D)
      = charLGeomModuliDictionary k
          (Finsupp.mapDomain τ (Finsupp.mapDomain r D)) := by
  rw [specializeModuli_mapDomain, show (r ∘ σ) = (τ ∘ r) from funext h,
    ← Finsupp.mapDomain_comp]
  rfl

omit [Field K] in

theorem specializePlace_intertwines (r : K → k) (σ : K → K) (τ : k → k)
    (h : ∀ a, r (σ a) = τ (r a)) (a : K) :
    specializePlace r (σ a) = charLGeomPlaceOfPoint k (τ (r a)) := by
  simp only [specializePlace, h]

end Galois

end ModularCurve

end

Statements phrased using this module (40)