Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AlgebraicCurve_RegularDifferentials.lean

definition module

Everywhere-regular Kähler differentials of a function field

Throughout, K and F are fields with F a K-algebra, and a place of F/K is an element of the project's structure Place K F: a valuation subring \mathcal O_v \subseteq F containing the image of K, different from F itself, and whose ideals are principal (so \mathcal O_v is a discrete valuation ring, with associated order function v.\mathrm{ord} : F \to \mathbb Z normalised so that an irreducible element has order 1). For such a v, v.dCoord is the Kähler differential d\pi \in \Omega[F\!\mid\!K] of a chosen irreducible element \pi of \mathcal O_v.

The module defines AlgebraicCurve.regularDifferentials K F, a K-submodule of \Omega[F\!\mid\!K], whose elements are those \omega such that for every place v of F/K there is f \in \mathcal O_v with \omega = f \cdot v.\mathrm{dCoord}. Thus \omega is required to be an \mathcal O_v-multiple of the differential of a uniformizer at each place simultaneously; when v.dCoord generates \Omega[F\!\mid\!K] as an F-module, this is the condition \mathrm{ord}_v \omega \ge 0. That this set is a K-submodule uses only that \mathcal O_v is a subring containing \mathrm{im}(K \to F). The companion lemma AlgebraicCurve.mem_regularDifferentials_iff records the membership criterion in exactly this form.

The module also proves AlgebraicCurve.Place.exists_ord_eq_one_and_dCoord_eq: for each place v there is \pi \in F with v.\mathrm{ord}\,\pi = 1 and v.\mathrm{dCoord} = d\pi. This exposes, without reference to the internal choice made in defining dCoord, that dCoord is the differential of some element of order exactly one at v.

No statement is made here about the dimension of regularDifferentials K F, about Hecke operators, or about q-expansions.

Relation to Mathlib

Built on Mathlib's KaehlerDifferential module \Omega[F\!\mid\!K] and on Mathlib's theory of valuation subrings and discrete valuation rings, but the notion of a place of F/K and this submodule of everywhere-regular differentials are the project's own, defined in its own AlgebraicCurve namespace.

Where it is used

For F the function field of a curve over K, this submodule is the space of global regular differentials, which for modular curves is the space attached to weight-two cusp forms and the cotangent space of the Jacobian; it sits alongside the project's divisor, degree and Picard-group constructions for such function fields, which underlie the treatment of Jacobians of modular curves.

References

  1. H. Stichtenoth, Algebraic Function Fields and Codes, Springer, 1993
  2. R. Hartshorne, Algebraic Geometry, Graduate Texts in Mathematics 52, Springer, 1977, Ch. II.8 and IV.1

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_CanonicalDivisor

set_option autoImplicit false

noncomputable section

open KaehlerDifferential

namespace AlgebraicCurve

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

namespace Place

variable {K F}

theorem exists_ord_eq_one_and_dCoord_eq (v : Place K F) :
    ∃ π : F, v.ord π = 1 ∧ v.dCoord = D K F π := by
  refine ⟨((IsDiscreteValuationRing.exists_irreducible v.toValuationSubring).choose : F), ?_, rfl⟩
  exact v.ord_coe_irreducible
    (IsDiscreteValuationRing.exists_irreducible v.toValuationSubring).choose_spec

end Place

def regularDifferentials : Submodule K Ω[F⁄K] where
  carrier := {ω | ∀ v : Place K F, ∃ f ∈ v.toValuationSubring, ω = f • v.dCoord}
  zero_mem' v := ⟨0, v.toValuationSubring.zero_mem, by rw [zero_smul]⟩
  add_mem' {ω η} hω hη v := by
    obtain ⟨f, hf, rfl⟩ := hω v
    obtain ⟨g, hg, hη'⟩ := hη v
    exact ⟨f + g, v.toValuationSubring.add_mem _ _ hf hg, by rw [hη', add_smul]⟩
  smul_mem' c {ω} hω v := by
    obtain ⟨f, hf, rfl⟩ := hω v
    refine ⟨algebraMap K F c * f, v.toValuationSubring.mul_mem _ _ (v.algebraMap_mem' c) hf, ?_⟩
    rw [mul_smul, algebraMap_smul]

variable {K F} in
theorem mem_regularDifferentials_iff {ω : Ω[F⁄K]} :
    ω ∈ regularDifferentials K F ↔
      ∀ v : Place K F, ∃ f ∈ v.toValuationSubring, ω = f • v.dCoord :=
  Iff.rfl

end AlgebraicCurve

end

Statements phrased using this module (129)