Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_LambdaNodeDescent.lean

definition module

The λ-function field, the λ-ring, and its integral closure

Everything here takes place inside the Laurent series field \overline{\mathbb Q}((q)), the ambient ring LaurentSeries (AlgebraicClosure ℚ). The two distinguished elements are lambdaModC (AlgebraicClosure ℚ), the image under coefficientwise reduction of the integral Laurent series lambdaInt given by the eta-product expression q\,\eta-product of weight-zero type (precisely, \mathrm{single}(1,1)\cdot(\mathrm{ofPowerSeries}\ \mathtt{etaProd})^{8} times the substitutions q\mapsto q^4 and q\mapsto q^2 of (\mathrm{ofPowerSeries}\ \mathtt{etaProd})^{16} and of \mathrm{ofPowerSeries}\ \mathtt{dedekindEtaUnitInv}), and lambdaNModC (AlgebraicClosure ℚ) N, obtained from it by the substitution q \mapsto q^{N} (the ring map qExpand on Laurent series).

For N \neq 0 and an intermediate field K of \overline{\mathbb Q}/\mathbb Q, lambdaFieldOver N K is the subfield of \overline{\mathbb Q}((q)) generated by the constant series with coefficients in K together with these two elements; informally K(\lambda(q),\lambda(q^{N})). For a valuation subring A \subseteq \overline{\mathbb Q}, lambdaRing A K is the subring generated by the constant series with coefficients in coeffSubring A K = A \cap K together with \lambda(q) alone; informally (A\cap K)[\lambda(q)]. Finally lambdaIntegralClosure N A K is the subring whose underlying set consists of those x lying in lambdaFieldOver N K which are integral over lambdaRing A K, i.e. the integral closure of (A\cap K)[\lambda(q)] inside K(\lambda(q),\lambda(q^{N})); the subring axioms are the standard closure properties of integral elements. Three further lemmas record the defining equivalence for membership in lambdaIntegralClosure and the memberships \lambda(q),\lambda(q^{N}) \in lambdaFieldOver N K.

Relation to Mathlib

Mathlib's integralClosure produces the integral closure of a commutative ring in an algebra over it; lambdaIntegralClosure instead carves out, as a Subring of the Laurent series field, the elements of a prescribed Subfield that are integral over a prescribed Subring.

Where it is used

These rings are the level-two (\lambda-) analogues of the j-line objects fieldOver, jRing and jIntegralClosure: the integral closure serves as a normal model of the level-two modular curve over the cut-down coefficient ring A \cap K, through which local behaviour at a node of the plane model is analysed and then passed to the limit over the intermediate fields K.

References

  1. F. Diamond and J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005
  2. O. Zariski and P. Samuel, Commutative Algebra II, Van Nostrand, 1960

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_LambdaNodeLocalized
import Definitions.Def_ModularCurve_NodeDescent

set_option autoImplicit false

namespace ModularCurve
namespace LambdaNodeLocalized
noncomputable section

open NodeLocalized

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

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

def lambdaIntegralClosure (N : ℕ) [NeZero N] (A : ValuationSubring (AlgebraicClosure ℚ))
    (K : IntermediateField ℚ (AlgebraicClosure ℚ)) :
    Subring (LaurentSeries (AlgebraicClosure ℚ)) where
  carrier := {x | x ∈ lambdaFieldOver N K ∧ IsIntegral (lambdaRing 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⟩

theorem mem_lambdaIntegralClosure (N : ℕ) [NeZero N] (A : ValuationSubring (AlgebraicClosure ℚ))
    (K : IntermediateField ℚ (AlgebraicClosure ℚ)) {x : LaurentSeries (AlgebraicClosure ℚ)} :
    x ∈ lambdaIntegralClosure N A K ↔ x ∈ lambdaFieldOver N K ∧ IsIntegral (lambdaRing A K) x :=
  Iff.rfl

theorem lambdaModC_mem_lambdaFieldOver (N : ℕ) [NeZero N] (K : IntermediateField ℚ (AlgebraicClosure ℚ)) :
    lambdaModC (AlgebraicClosure ℚ) ∈ lambdaFieldOver N K :=
  Subfield.subset_closure (Or.inr (Set.mem_insert _ _))

theorem lambdaNModC_mem_lambdaFieldOver (N : ℕ) [NeZero N] (K : IntermediateField ℚ (AlgebraicClosure ℚ)) :
    lambdaNModC (AlgebraicClosure ℚ) N ∈ lambdaFieldOver N K :=
  Subfield.subset_closure (Or.inr (Set.mem_insert_of_mem _ (Set.mem_singleton _)))

end
end LambdaNodeLocalized
end ModularCurve

Statements phrased using this module (18)