Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_IgusaFunctionField.lean

definition module

Igusa function field, Kummer generators, diamond data

Throughout, \kappa is a field, \Omega an extension field of \kappa (intended to be a field of Laurent series in q), K_0 an intermediate field of \Omega/\kappa and a \in \Omega. The field igusaFunctionField K₀ a is the intermediate field of \Omega/\kappa obtained by adjoining to \kappa the set K_0 \cup \{a\}; accompanying lemmas record that it contains K_0 and a, and that it equals the join K_0 \sqcup \kappa(a) inside the lattice of intermediate fields. The map incl is the \kappa-algebra inclusion of K_0 into this field, and qExpansion is its tautological embedding into \Omega, which composed with incl is the inclusion K_0 \subseteq \Omega.

IsKummerGenerator n K₀ a is a Prop-valued structure with exactly three fields: n > 0, a \neq 0, and a^n \in K_0; it asserts no irreducibility or degree statement. For a place w of K_I = igusaFunctionField K₀ a over \kappa in the project's sense (a valuation subring of K_I containing \kappa, proper, and a principal ideal ring, hence a discrete valuation ring), restrictToBase is its restriction along incl — formed from the hypothesis that incl is an integral ring homomorphism — and ramificationIndexOverBase w is the ramification index along incl, i.e. the least positive n of the form w(\mathrm{ord}) of the image of a nonzero element of K_0.

For a prime p with \operatorname{char} \kappa = p and k \in \mathbb{Z}, IgusaDiamondData p k K₀ a is a structure carrying as data a monoid homomorphism b \mapsto \langle b \rangle from (\mathbb{Z}/p)^\times to the group of \kappa-automorphisms of K_I, together with two axioms: each \langle b \rangle fixes every element of K_I lying in K_0, and \langle b \rangle a = b^k \cdot a, where b^k \in (\mathbb{Z}/p)^\times is mapped into \kappa by the canonical homomorphism \mathbb{Z}/p \to \kappa available in characteristic p. From such data, actDiff is the \kappa-linear endomorphism of the module of Kähler differentials \Omega_{K_I/\kappa} obtained by pulling back along \langle b \rangle, and act_incl restates that \langle b \rangle fixes the image of K_0. Existence of the action, the degree [K_I : K_0], and ramification behaviour are not addressed here.

Relation to Mathlib

IntermediateField.adjoin and the Kähler differential module \Omega_{\cdot/\cdot} are Mathlib's; places of a function field, their restriction and ramification index along a \kappa-algebra map, and pull-back on differentials are the project's own notions. Mathlib has no notion of Igusa cover or of diamond operators on one.

Where it is used

The intended reading is that K_0 is the function field of a modular curve over a field of characteristic p, a a root of an equation extracted from the Hasse invariant, so that K_I is the function field of the associated Igusa cover and qExpansion records q-expansions at a cusp where that root is rational. The diamond data provide the (\mathbb{Z}/p)^\times-action used in the analysis of the reduction modulo p of modular curves and of their Jacobians.

References

  1. J.-I. Igusa, Kroneckerian model of fields of elliptic modular functions, American Journal of Mathematics 81 (1959), 561–577
  2. 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_IgusaFunctionField.lean

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_AlgebraicCurve_Correspondence
import Definitions.Def_AlgebraicCurve_Differentials

set_option autoImplicit false

noncomputable section

namespace ModularCurve.IgusaCover

open AlgebraicCurve

variable {κ : Type*} [Field κ] {Ω : Type*} [Field Ω] [Algebra κ Ω]

def igusaFunctionField (K₀ : IntermediateField κ Ω) (a : Ω) : IntermediateField κ Ω :=
  IntermediateField.adjoin κ ((K₀ : Set Ω) ∪ {a})

variable (K₀ : IntermediateField κ Ω) (a : Ω)

theorem le_igusaFunctionField : K₀ ≤ igusaFunctionField K₀ a :=
  fun _ hx => IntermediateField.subset_adjoin κ _ (Or.inl hx)

theorem mem_igusaFunctionField : a ∈ igusaFunctionField K₀ a :=
  IntermediateField.subset_adjoin κ _ (Or.inr rfl)

theorem igusaFunctionField_eq_sup :
    igusaFunctionField K₀ a = K₀ ⊔ IntermediateField.adjoin κ {a} := by
  rw [igusaFunctionField, IntermediateField.adjoin_union, IntermediateField.adjoin_self]

def incl : K₀ →ₐ[κ] igusaFunctionField K₀ a :=
  IntermediateField.inclusion (le_igusaFunctionField K₀ a)

@[simp] theorem coe_incl (x : K₀) : ((incl K₀ a x : igusaFunctionField K₀ a) : Ω) = x := rfl

def qExpansion : igusaFunctionField K₀ a →ₐ[κ] Ω := (igusaFunctionField K₀ a).val

theorem qExpansion_incl (x : K₀) : qExpansion K₀ a (incl K₀ a x) = (x : Ω) := rfl

structure IsKummerGenerator (n : ℕ) (K₀ : IntermediateField κ Ω) (a : Ω) : Prop where

  pos : 0 < n
  ne_zero : a ≠ 0
  pow_mem : a ^ n ∈ K₀

def restrictToBase (hint : (incl K₀ a).toRingHom.IsIntegral) (w : Place κ (igusaFunctionField K₀ a)) : Place κ K₀ :=
  w.restrictAlong (incl K₀ a) hint

def ramificationIndexOverBase (w : Place κ (igusaFunctionField K₀ a)) : ℕ :=
  w.ramificationIndexAlong (incl K₀ a)

structure IgusaDiamondData (p : ℕ) [Fact p.Prime] [CharP κ p] (k : ℤ) (K₀ : IntermediateField κ Ω) (a : Ω) where

  act : (ZMod p)ˣ →* (igusaFunctionField K₀ a ≃ₐ[κ] igusaFunctionField K₀ a)

  act_apply_of_mem : ∀ (b : (ZMod p)ˣ) (x : igusaFunctionField K₀ a), (x : Ω) ∈ K₀ → act b x = x

  act_gen : ∀ b : (ZMod p)ˣ,
    ((act b ⟨a, mem_igusaFunctionField K₀ a⟩ : igusaFunctionField K₀ a) : Ω) =
      (ZMod.castHom (dvd_refl p) κ (((b ^ k : (ZMod p)ˣ) : ZMod p))) • a

namespace IgusaDiamondData

variable {K₀ a} {p : ℕ} [Fact p.Prime] [CharP κ p] {k : ℤ}

def actDiff (d : IgusaDiamondData p k K₀ a) (b : (ZMod p)ˣ) :
    Ω[igusaFunctionField K₀ a⁄κ] →ₗ[κ] Ω[igusaFunctionField K₀ a⁄κ] :=
  pullbackDiff (d.act b : igusaFunctionField K₀ a →ₐ[κ] igusaFunctionField K₀ a)

theorem act_incl (d : IgusaDiamondData p k K₀ a) (b : (ZMod p)ˣ) (x : K₀) : d.act b (incl K₀ a x) = incl K₀ a x :=
  d.act_apply_of_mem b _ x.2

end IgusaDiamondData

end ModularCurve.IgusaCover

end

Statements phrased using this module (3)