Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_JZeroNaiveHeight.lean

definition module

Naive height on the modular Jacobian via -coordinates

Fix N \ge 1 and work with \bar F = modularFunctionFieldBar N, the base change to \overline{\mathbb Q} of the field generated over \mathbb Q by the q-expansions j(q^d), d \mid N, inside Laurent series; write j \in \bar F for the coefficientwise image of the series jq. For a place v of \bar F over \overline{\mathbb Q}, jCoord N v is a choice (via Classical.epsilon, hence unspecified when none exists) of c \in \overline{\mathbb Q} with v.\mathrm{ord}(j - c) > 0, i.e. a value of j at v; jFactor N v is X - C(\mathrm{jCoord}\,N\,v) when v.\mathrm{ord}(j) \ge 0 and 1 otherwise, so that places at which j has a pole contribute trivially. For a divisor D, symPoly N D is the finitely supported product \prod_v (\mathrm{jFactor}\,N\,v)^{\max(D(v),0)}, and symVec N g' D is the vector in \overline{\mathbb Q}^{\,g'+1} whose k-th entry is the coefficient of X^{g'-k} (truncated subtraction in \mathbb N) of that polynomial.

Let K be an intermediate field of \overline{\mathbb Q}/\mathbb Q of finite degree, made a number field by numberField_of_finiteDimensional. Then divNaiveHeight N K g' D is Mathlib's logarithmic height Height.logHeight of symVec N g' D regarded as a tuple over K, when all its entries lie in K, and 0 otherwise. For a class c in the fixed-point subgroup JZero N ^+ K.fixingSubgroup of the degree-zero divisor class group, JZero.repHeights N K g' c is the set of reals divNaiveHeight N K g' D taken over pairs (D,E) with D effective, E of degree zero, E + g' \cdot (\mathrm{cuspInftyBar}\,N) = D, D invariant under the arithmetic Galois action of every \sigma fixing K pointwise, and [E] = c; JZero.naiveHeight is the infimum of that set. Accompanying lemmas evaluate jFactor in the two cases, compute symPoly on 0 and on a single place, and record that divNaiveHeight and hence naiveHeight are non-negative, that naiveHeight is at most the height of any admissible representative, and that it equals 0 when no representative exists.

Relation to Mathlib

The logarithmic height Height.logHeight over a number field is taken from Mathlib; places, divisors and the degree-zero class group Pic0 belong to the project's own curve library, and the height on classes of JZero defined here has no Mathlib counterpart. The notation α ^+ M for FixedPoints.addSubgroup M α is re-declared in the project's compatibility module.

Where it is used

These definitions provide the height function on Galois-invariant classes of the degree-zero divisor class group of the modular function field, the quantitative input for descent-type arguments on J_0(N)(K) in the modular-curve part of the development.

References

  1. M. Hindry and J. H. Silverman, Diophantine Geometry: An Introduction, Graduate Texts in Mathematics 201, Springer, 2000
  2. J.-P. Serre, Lectures on the Mordell–Weil Theorem, Aspects of Mathematics E15, Vieweg, 1989
  3. E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press, 2006

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

Imports

Imported by

Declarations

Source

import Definitions.Def_ModularCurve_AtkinLehner
import Mathlib.Algebra.Ring.Action.Submonoid ↗
import Mathlib.FieldTheory.Galois.Basic ↗
import Mathlib.NumberTheory.Height.NumberField ↗
import Definitions.Def_Compat_Mathlib430

noncomputable section

open AlgebraicCurve Polynomial

namespace ModularCurve

variable (N : ℕ) [NeZero N]

def jCoord (v : Place (AlgebraicClosure ℚ) (modularFunctionFieldBar N)) : AlgebraicClosure ℚ :=
  Classical.epsilon fun c : AlgebraicClosure ℚ =>
    0 < v.ord ((⟨coeffEmb (AlgebraicClosure ℚ) jq,
      coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) (jq_mem_full N)⟩ : modularFunctionFieldBar N)
      - algebraMap (AlgebraicClosure ℚ) (modularFunctionFieldBar N) c)

def jFactor (v : Place (AlgebraicClosure ℚ) (modularFunctionFieldBar N)) :
    Polynomial (AlgebraicClosure ℚ) :=
  if 0 ≤ v.ord (⟨coeffEmb (AlgebraicClosure ℚ) jq,
      coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) (jq_mem_full N)⟩ : modularFunctionFieldBar N)
  then X - C (jCoord N v) else 1

def symPoly (D : Divisor (AlgebraicClosure ℚ) (modularFunctionFieldBar N)) :
    Polynomial (AlgebraicClosure ℚ) :=
  D.prod fun v n => jFactor N v ^ n.toNat

def symVec (g' : ℕ) (D : Divisor (AlgebraicClosure ℚ) (modularFunctionFieldBar N)) :
    Fin (g' + 1) → AlgebraicClosure ℚ :=
  fun k => (symPoly N D).coeff (g' - k)

instance numberField_of_finiteDimensional (K : IntermediateField ℚ (AlgebraicClosure ℚ))
    [FiniteDimensional ℚ K] : NumberField K :=
  NumberField.mk

variable (K : IntermediateField ℚ (AlgebraicClosure ℚ)) [FiniteDimensional ℚ K]

open scoped Classical in

def divNaiveHeight (g' : ℕ) (D : Divisor (AlgebraicClosure ℚ) (modularFunctionFieldBar N)) : ℝ :=
  if h : ∀ k, symVec N g' D k ∈ K then Height.logHeight fun k => (⟨symVec N g' D k, h k⟩ : K) else 0

def JZero.repHeights (g' : ℕ) (c : ↥(JZero N ^+ ↥K.fixingSubgroup)) : Set ℝ :=
  {r | ∃ (D : Divisor (AlgebraicClosure ℚ) (modularFunctionFieldBar N))
      (E : Divisor.degZero (K := AlgebraicClosure ℚ) (F := ↥(modularFunctionFieldBar N))),
      (∀ v, 0 ≤ D v) ∧
      (E : Divisor (AlgebraicClosure ℚ) (modularFunctionFieldBar N))
          + (g' : ℤ) • Finsupp.single (cuspInftyBar N) 1 = D ∧
      (∀ σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ, σ ∈ K.fixingSubgroup →
          arithmeticGalois (modularFunctionFieldFull N) σ • D = D) ∧
      Pic0.mk E = (c : JZero N) ∧
      r = divNaiveHeight N K g' D}

def JZero.naiveHeight (g' : ℕ) (c : ↥(JZero N ^+ ↥K.fixingSubgroup)) : ℝ :=
  sInf (JZero.repHeights N K g' c)

variable {N K}

theorem jFactor_of_nonneg {v : Place (AlgebraicClosure ℚ) (modularFunctionFieldBar N)}
    (hv : 0 ≤ v.ord (⟨coeffEmb (AlgebraicClosure ℚ) jq,
      coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) (jq_mem_full N)⟩ : modularFunctionFieldBar N)) :
    jFactor N v = X - C (jCoord N v) :=
  if_pos hv

theorem jFactor_of_neg {v : Place (AlgebraicClosure ℚ) (modularFunctionFieldBar N)}
    (hv : v.ord (⟨coeffEmb (AlgebraicClosure ℚ) jq,
      coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) (jq_mem_full N)⟩ : modularFunctionFieldBar N) < 0) :
    jFactor N v = 1 :=
  if_neg (not_le.mpr hv)

@[simp]
theorem symPoly_zero : symPoly N 0 = 1 :=
  Finsupp.prod_zero_index

theorem symPoly_single (v : Place (AlgebraicClosure ℚ) (modularFunctionFieldBar N)) (n : ℤ) :
    symPoly N (Finsupp.single v n) = jFactor N v ^ n.toNat :=
  Finsupp.prod_single_index (by simp)

theorem divNaiveHeight_nonneg (g' : ℕ) (D : Divisor (AlgebraicClosure ℚ) (modularFunctionFieldBar N)) :
    0 ≤ divNaiveHeight N K g' D := by
  unfold divNaiveHeight
  split_ifs with h
  · exact Height.logHeight_nonneg _
  · exact le_rfl

theorem JZero.repHeights_nonneg {g' : ℕ} {c : ↥(JZero N ^+ ↥K.fixingSubgroup)} {r : ℝ}
    (hr : r ∈ JZero.repHeights N K g' c) : 0 ≤ r := by
  obtain ⟨D, E, -, -, -, -, rfl⟩ := hr
  exact divNaiveHeight_nonneg g' D

theorem JZero.naiveHeight_nonneg (g' : ℕ) (c : ↥(JZero N ^+ ↥K.fixingSubgroup)) :
    0 ≤ JZero.naiveHeight N K g' c :=
  Real.sInf_nonneg fun _ hr => JZero.repHeights_nonneg hr

theorem JZero.naiveHeight_le (g' : ℕ) (c : ↥(JZero N ^+ ↥K.fixingSubgroup))
    (D : Divisor (AlgebraicClosure ℚ) (modularFunctionFieldBar N))
    (E : Divisor.degZero (K := AlgebraicClosure ℚ) (F := ↥(modularFunctionFieldBar N)))
    (hD : ∀ v, 0 ≤ D v)
    (hE : (E : Divisor (AlgebraicClosure ℚ) (modularFunctionFieldBar N))
        + (g' : ℤ) • Finsupp.single (cuspInftyBar N) 1 = D)
    (hK : ∀ σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ, σ ∈ K.fixingSubgroup →
        arithmeticGalois (modularFunctionFieldFull N) σ • D = D)
    (hc : Pic0.mk E = (c : JZero N)) :
    JZero.naiveHeight N K g' c ≤ divNaiveHeight N K g' D :=
  csInf_le ⟨0, fun _ hr => JZero.repHeights_nonneg hr⟩ ⟨D, E, hD, hE, hK, hc, rfl⟩

theorem JZero.naiveHeight_eq_zero (g' : ℕ) (c : ↥(JZero N ^+ ↥K.fixingSubgroup))
    (h : JZero.repHeights N K g' c = ∅) : JZero.naiveHeight N K g' c = 0 := by
  rw [JZero.naiveHeight, h, Real.sInf_empty]

end ModularCurve

end

Statements phrased using this module (10)