Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_NodeDescent.lean

definition module

Descent of the nodal -ring to a coefficient subfield

Throughout, A is a valuation subring of \overline{\mathbb Q}, K an intermediate field of \overline{\mathbb Q}/\mathbb Q, and N a positive natural number; the ambient ring of Laurent series is \overline{\mathbb Q}((q)), in which j(q) is the series jqModC =q^{-1}+\dots obtained from the integral q-expansion of j and j(q^N) is its image jqNModC under substitution q\mapsto q^N. Four objects are introduced. First, coeffSubring A K is the intersection A\cap K, formed as the meet of the subring underlying A and the subring underlying K; it is the coefficient ring on which reduction will act. Second, redRestrict restricts a ring homomorphism \mathrm{red}\colon A\to k into a field k along the inclusion A\cap K\hookrightarrow A, yielding A\cap K\to k. Third, fieldOver N K is the subfield of \overline{\mathbb Q}((q)) generated by the constant series with coefficients in K (the image of K under CharPReduction.constSeries, i.e. the range of the map sending c to the series c concentrated in degree 0) together with the two elements j(q) and j(q^N); it is the subfield closure of that set, a model for the function field K(j,j_N). Fourth, jRing A K is the subring generated by the constant series with coefficients in A\cap K together with j(q) alone, that is (A\cap K)[j]. Finally jIntegralClosure N A K is the subring of \overline{\mathbb Q}((q)) whose elements are those x lying in fieldOver N K and integral over jRing A K: the integral closure of (A\cap K)[j] inside K(j,j_N), packaged with its verifications of closure under the ring operations. Nothing is asserted beyond these definitions.

Relation to Mathlib

Built from Mathlib's ValuationSubring, IntermediateField, Subring.closure, Subfield.closure and IsIntegral; rather than Mathlib's integralClosure of an algebra, the integral closure is here cut out as an explicit subring of the Laurent series field by intersecting the integrality condition with membership in a prescribed subfield.

Where it is used

This is the coefficient-descent vocabulary accompanying the localisation modularLocalizedAtPoint of the modular ring at a point of the reduction of X_0(N): the ring localised at a point with coefficients in all of A is replaced by data over the smaller coefficient ring A\cap K, with the integral closure of (A\cap K)[j] in K(j,j_N) as the ring to which normality arguments are applied. It feeds the analysis of X_0(N) at a node used in the level-lowering part of the proof.

References

  1. P. Deligne and M. Rapoport, Les schémas de modules de courbes elliptiques, in: Modular Functions of One Variable II, Lecture Notes in Mathematics 349, Springer, 1973, 143–316
  2. S. Lang, Elliptic Functions, 2nd edition, Graduate Texts in Mathematics 112, Springer, 1987

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_NodeLocalized

set_option autoImplicit false

namespace ModularCurve
namespace NodeLocalized
noncomputable section

def coeffSubring (A : ValuationSubring (AlgebraicClosure ℚ)) (K : IntermediateField ℚ (AlgebraicClosure ℚ)) :
    Subring (AlgebraicClosure ℚ) :=
  A.toSubring ⊓ K.toSubalgebra.toSubring

def redRestrict {k : Type*} [Field k] {A : ValuationSubring (AlgebraicClosure ℚ)} (red : A →+* k)
    (K : IntermediateField ℚ (AlgebraicClosure ℚ)) : coeffSubring A K →+* k :=
  red.comp (Subring.inclusion inf_le_left)

def fieldOver (N : ℕ) [NeZero N] (K : IntermediateField ℚ (AlgebraicClosure ℚ)) : Subfield (LaurentSeries (AlgebraicClosure ℚ)) :=
  Subfield.closure (Set.range (CharPReduction.constSeries K.toSubalgebra.toSubring)
    ∪ {jqModC (AlgebraicClosure ℚ), jqNModC (AlgebraicClosure ℚ) N})

def jRing (A : ValuationSubring (AlgebraicClosure ℚ)) (K : IntermediateField ℚ (AlgebraicClosure ℚ)) :
    Subring (LaurentSeries (AlgebraicClosure ℚ)) :=
  Subring.closure (Set.range (CharPReduction.constSeries (coeffSubring A K)) ∪ {jqModC (AlgebraicClosure ℚ)})

def jIntegralClosure (N : ℕ) [NeZero N] (A : ValuationSubring (AlgebraicClosure ℚ)) (K : IntermediateField ℚ (AlgebraicClosure ℚ)) :
    Subring (LaurentSeries (AlgebraicClosure ℚ)) where
  carrier := {x | x ∈ fieldOver N K ∧ IsIntegral (jRing A K) x}
  zero_mem' := ⟨zero_mem _, isIntegral_zero⟩
  one_mem' := ⟨one_mem _, isIntegral_one⟩
  add_mem' := fun hx hy => ⟨add_mem hx.1 hy.1, hx.2.add hy.2⟩
  neg_mem' := fun hx => ⟨neg_mem hx.1, hx.2.neg⟩
  mul_mem' := fun hx hy => ⟨mul_mem hx.1 hy.1, hx.2.mul hy.2⟩

end
end NodeLocalized
end ModularCurve

Statements phrased using this module (103)