Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_QExpansionDiff.lean

definition module

The operator , -expansions of differentials, trace of differentials

Three pieces of vocabulary, all introduced as data together with the predicates that characterise them.

For a field L, ModularCurve.thetaL is the L-linear endomorphism of the Laurent series field L((q)) sending f to q\cdot f', where f' is Mathlib's formal derivative of a Laurent series and q denotes the Hahn-series monomial single (1 : ℤ) (1 : L); thetaL_apply records this defining formula. Thus thetaL is the operator \theta = q\,d/dq.

In a context of fields K, F, L with F and L algebras over K, ModularCurve.IsQExpansionDiffAlong σ φ is a predicate on a K-algebra map \sigma : F \to L((q)) and a K-linear map \varphi : \Omega_{F/K} \to L((q)), asserting the conjunction of two conditions: \varphi(\mathrm{d}x) = \theta(\sigma x) for every x \in F, where \mathrm{d} is the universal derivation KaehlerDifferential.D K F, and \varphi(f \cdot \omega) = \sigma(f)\,\varphi(\omega) for all f \in F and \omega \in \Omega_{F/K}, i.e. \varphi is \sigma-semilinear over F. Informally, \varphi(\omega) is the Laurent series h with \omega = h\,dq/q along \sigma. Then ModularCurve.qExpansionDiffAlong σ is defined to be some \varphi with this property when one exists, and the zero map otherwise; neither existence nor uniqueness is asserted here, so the map is characterised only through the predicate.

For a tower of fields K \to F \to F', AlgebraicCurve.IsTraceDiff K F F' t is the predicate on an F-linear map t : \Omega_{F'/K} \to \Omega_{F/K} that t(y \cdot \iota(\omega)) = \mathrm{Tr}_{F'/F}(y)\cdot\omega for all y \in F' and \omega \in \Omega_{F/K}, where \iota is KaehlerDifferential.map K K F F'. Again AlgebraicCurve.traceDiff is defined to be such a t if one exists and the zero map otherwise.

Relation to Mathlib

Built on Mathlib's Laurent series with their formal derivative, Mathlib's Kähler differentials Ω[F⁄K] with the universal derivation and the base-change map KaehlerDifferential.map, and Algebra.trace. The operator \theta, the notion of a q-expansion of a differential along an embedding into L((q)), and the trace (push-forward) map on differentials in a tower are the project's own notions.

Where it is used

This module supplies vocabulary used throughout the tree: the q-expansion map attaches to a differential on a modular curve, via an embedding of its function field into L((q)) at a cusp, the Laurent series of the associated weight-two form, and traceDiff is the push-forward of differentials along a covering of curves, expressed through the field trace.

References

  1. F. Diamond and J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005
  2. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Princeton University Press, 1971

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

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib.RingTheory.LaurentSeries ↗
import Mathlib.RingTheory.Kaehler.Basic ↗

set_option autoImplicit false

noncomputable section

open HahnSeries

namespace ModularCurve

section Theta

variable (L : Type*) [Field L]

def thetaL : LaurentSeries L →ₗ[L] LaurentSeries L where
  toFun f := single (1 : ℤ) (1 : L) * LaurentSeries.derivative L f
  map_add' f g := by rw [map_add, mul_add]
  map_smul' c f := by
    rw [map_smul, RingHom.id_apply, ← single_zero_mul_eq_smul, ← single_zero_mul_eq_smul,
      mul_left_comm]

variable {L} in

theorem thetaL_apply (f : LaurentSeries L) :
    thetaL L f = single (1 : ℤ) (1 : L) * LaurentSeries.derivative L f :=
  rfl

end Theta

section QExpansionDiff

variable {K F L : Type*} [Field K] [Field F] [Algebra K F] [Field L] [Algebra K L]

def IsQExpansionDiffAlong (σ : F →ₐ[K] LaurentSeries L) (φ : Ω[F⁄K] →ₗ[K] LaurentSeries L) :
    Prop :=
  (∀ x : F, φ (KaehlerDifferential.D K F x) = thetaL L (σ x)) ∧
    ∀ (f : F) (ω : Ω[F⁄K]), φ (f • ω) = σ f * φ ω

open scoped Classical in

def qExpansionDiffAlong (σ : F →ₐ[K] LaurentSeries L) : Ω[F⁄K] →ₗ[K] LaurentSeries L :=
  if h : ∃ φ : Ω[F⁄K] →ₗ[K] LaurentSeries L, IsQExpansionDiffAlong σ φ then h.choose else 0

end QExpansionDiff

end ModularCurve

namespace AlgebraicCurve

section TraceDiff

variable (K F F' : Type*) [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
  [Algebra F F'] [IsScalarTower K F F']

def IsTraceDiff (t : Ω[F'⁄K] →ₗ[F] Ω[F⁄K]) : Prop :=
  ∀ (y : F') (ω : Ω[F⁄K]),
    t (y • KaehlerDifferential.map K K F F' ω) = Algebra.trace F F' y • ω

open scoped Classical in

def traceDiff : Ω[F'⁄K] →ₗ[F] Ω[F⁄K] :=
  if h : ∃ t : Ω[F'⁄K] →ₗ[F] Ω[F⁄K], IsTraceDiff K F F' t then h.choose else 0

end TraceDiff

end AlgebraicCurve

end

Statements phrased using this module (111)