Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AlgebraicCurve_IsCurveOver.lean

definition module

The curve axioms `IsCurveOver` for a function field

Throughout, K and F are fields with F a K-algebra. A place of F/K (the structure Place K F of the divisor-class module) is a valuation subring A \subseteq F containing the image of K, with A \neq F and with A a principal ideal ring, so that A is a discrete valuation ring; its residue field \kappa(v) is a K-algebra, v.\mathrm{deg} is \dim_K \kappa(v), and \mathrm{ord}_v is the associated normalised valuation on F. The class HasPrincipalDivisors K F asserts that for every f \in F^{\times} there is a finitely supported function D : \mathrm{Place}\,K\,F \to \mathbb{Z} with D(v) = \mathrm{ord}_v(f) for every place v and with \deg D = \sum_v D(v)\,v.\mathrm{deg} = 0; that is, the divisor of f exists as a divisor and has degree zero.

The class defined here, IsCurveOver K F, extends HasPrincipalDivisors K F by two further fields: every place v of F/K has residue field finite over K, and the module of Kähler differentials \Omega_{F/K} is free of rank one over F. The accessors record these as separately usable facts: the underlying principal-divisors structure, finiteness of each residue field (also registered as the Place.FiniteResidue property at every place), freeness of \Omega_{F/K}, \dim_F \Omega_{F/K} = 1, and hence nontriviality of \Omega_{F/K}. Finally, if K is algebraically closed and \kappa(v) is finite over K, then K \to \kappa(v) is integral and therefore bijective, so v.\mathrm{deg} = 1; consequently, over an algebraically closed K every place of a curve F/K has degree one, stated both pointwise and as a universally quantified statement.

Relation to Mathlib

Mathlib has no axiomatisation of the function field of a curve of this shape; Place, HasPrincipalDivisors and IsCurveOver are the project's own, built on Mathlib's valuation subrings, discrete valuation rings and Kähler differentials Ω[F⁄K].

Where it is used

This package is the hypothesis discharged wherever a function field is treated as the function field of a curve: it supplies degree-zero divisors and the group \mathrm{Pic}^0, the finiteness of residue fields needed for the degree map, and the rank-one differential module underlying canonical-divisor and Riemann–Roch arguments. These are used in the study of modular curves and of the special fibre of X_0(N), where the base field is algebraically closed and all places have degree one.

References

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

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

Imports

Imported by

Declarations

Source

import Definitions.Def_AlgebraicCurve_DivisorClassGroup
import Mathlib.RingTheory.Kaehler.Basic ↗
import Mathlib.FieldTheory.IsAlgClosed.Basic ↗

set_option autoImplicit false

noncomputable section

open KaehlerDifferential

namespace AlgebraicCurve

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

class IsCurveOver : Prop extends HasPrincipalDivisors K F where

  finiteResidue : ∀ v : Place K F, Module.Finite K v.ResidueField

  kaehler_free_rank_one : Module.Free F Ω[F⁄K] ∧ Module.finrank F Ω[F⁄K] = 1

namespace IsCurveOver

variable {K F}

theorem hasPrincipalDivisors [h : IsCurveOver K F] : HasPrincipalDivisors K F :=
  h.toHasPrincipalDivisors

theorem finite_residueField [IsCurveOver K F] (v : Place K F) :
    Module.Finite K v.ResidueField :=
  IsCurveOver.finiteResidue v

instance instFiniteResidue [IsCurveOver K F] (v : Place K F) : v.FiniteResidue :=
  ⟨IsCurveOver.finiteResidue v⟩

instance instFreeKaehler [h : IsCurveOver K F] : Module.Free F Ω[F⁄K] :=
  h.kaehler_free_rank_one.1

theorem finrank_kaehler [h : IsCurveOver K F] : Module.finrank F Ω[F⁄K] = 1 :=
  h.kaehler_free_rank_one.2

instance instNontrivialKaehler [IsCurveOver K F] : Nontrivial Ω[F⁄K] :=
  Module.nontrivial_of_finrank_eq_succ (n := 0) finrank_kaehler

end IsCurveOver

namespace Place

variable {K F}

theorem deg_eq_one_of_isAlgClosed_of_finite [IsAlgClosed K] (v : Place K F)
    [Module.Finite K v.ResidueField] : v.deg = 1 := by
  have : Algebra.IsIntegral K v.ResidueField := Algebra.IsIntegral.of_finite K v.ResidueField
  have hbij : Function.Bijective (algebraMap K v.ResidueField) :=
    IsAlgClosed.algebraMap_bijective_of_isIntegral
  show Module.finrank K v.ResidueField = 1
  rw [← Module.finrank_self K]
  exact ((AlgEquiv.ofBijective (Algebra.ofId K v.ResidueField) hbij).toLinearEquiv.finrank_eq).symm

end Place

namespace IsCurveOver

variable {K F}

theorem deg_eq_one_of_isAlgClosed [IsAlgClosed K] [IsCurveOver K F] (v : Place K F) :
    v.deg = 1 :=
  haveI : Module.Finite K v.ResidueField := IsCurveOver.finiteResidue v
  v.deg_eq_one_of_isAlgClosed_of_finite

theorem forall_deg_eq_one_of_isAlgClosed [IsAlgClosed K] [IsCurveOver K F] :
    ∀ w : Place K F, w.deg = 1 :=
  deg_eq_one_of_isAlgClosed

end IsCurveOver

end AlgebraicCurve

Statements phrased using this module (1,013)

… and 863 more statements (search for the module name to find them).