Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_JZeroHeightForm.lean

definition module

Height form on divisors; divisor representatives in J_0(N)

The first half works with a function field F over \overline{\mathbb{Q}} in the project's AlgebraicCurve framework, where a Place is a valuation subring of F containing the image of the base field, proper and with principal ideals, and a Divisor is a finitely supported \mathbb{Z}-valued function on places. For a finite family x of algebraic numbers, absLogHeight is the logarithmic height of x, computed in the intermediate field \mathbb{Q}(\operatorname{range} x) of \overline{\mathbb{Q}}, divided by [\mathbb{Q}(\operatorname{range} x):\mathbb{Q}]; that this field is finite over \mathbb{Q} is finiteDimensional_adjoin_range. Given s : \mathrm{Fin}\,r \to F and a place v, pivotIndex selects (when r>0) an index minimising \operatorname{ord}_v(s_i), evalVec s v is the vector of residues v(s_i/s_{\mathrm{piv}}) under Place.evalAt, and chordVec s v w is the family of 2\times2 minors \,e_v(i)e_w(j)-e_v(j)e_w(i). Then pointHt s v is absLogHeight of evalVec s v, pairHt s v w = pointHt v + pointHt w - absLogHeight (chordVec v w), and baseHt s b v is pairHt s v b, set to 0 when v=b. For \gamma \in \mathbb{Z}, a base place b and a divisor D=\sum_v n_v v, heightFormAux is \Big(\gamma+\sum_v n_v-1\Big)\sum_v n_v\,\mathrm{baseHt}(v)-\tfrac12\sum_{v\neq w \in \operatorname{supp} D} n_v n_w\,\mathrm{pairHt}(v,w)-(2-2\gamma)\sum_v \tfrac{n_v(n_v-1)}{2}\,\mathrm{baseHt}(v), and heightForm applies this after erasing the coefficient at b. Hence the form is unchanged on adding any multiple of b (heightForm_add_single_base) and satisfies Q(2D)=4\,Q(D) (heightForm_two_smul).

The second half specialises to N with NeZero N. With g= genusFF of \overline{\mathbb{Q}}-function field modularFunctionFieldBar N, embDegree is 2g+1, embDivisor is (2g+1)\cdot\infty at the place cuspInftyBar N, and IsEmbBasis s says that s is linearly independent over \overline{\mathbb{Q}} and spans riemannRochSpace (embDivisor N), i.e. the space of functions with poles bounded by (2g+1)\infty. JZero.heightForm N s D is heightForm with \gamma=g and base place cuspInftyBar N, inheriting both identities. Finally, for a number field K \subset \overline{\mathbb{Q}} and a class c in the additive fixed points of JZero N under K.fixingSubgroup, JZero.IsRepOf N K n c D asserts the existence of a degree-zero divisor E with: D effective, E+n\cdot\infty=D, D invariant under the arithmeticGalois action of every \sigma fixing K, and \mathrm{Pic}^0-class of E equal to c. JZero.mem_repHeights_iff identifies repHeights with the set of divNaiveHeight values of such representatives; IsRepOf.nsmul gives m\cdotscaling (m n, m\bullet c, m\bullet D) and IsRepOf.add_single allows adding p\cdot\infty, raising n to n+p, under the hypothesis that the cusp place itself is fixed by the relevant Galois elements.

Relation to Mathlib

The normalised height absLogHeight is built from Mathlib's Height.logHeight for number fields by dividing by the degree of the field generated by the coordinates. Places, divisors, Pic0, riemannRochSpace and genusFF are the project's own function-field notions; Mathlib has no height form on divisors of a curve.

Where it is used

The form defined here is the quadratic-form companion of the naive height divNaiveHeight on effective divisors of X_0(N), and IsRepOf isolates exactly the Galois-stable effective representatives E + n\cdot\infty of a class of J_0(N) over which that naive height is minimised. Together they supply the height machinery used in the bounds on rational points and torsion of J_0(N) entering the modular-curve side of the argument.

References

  1. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154
  2. S. Lang, Fundamentals of Diophantine Geometry, Springer, 1983
  3. M. Hindry and J. H. Silverman, Diophantine Geometry: An Introduction, Graduate Texts in Mathematics 201, Springer, 2000

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

Imports

Imported by

Declarations

Source

import Definitions.Def_ModularCurve_JZeroNaiveHeight
import Definitions.Def_AlgebraicCurve_PlaceEvaluation
import Definitions.Def_AlgebraicCurve_Repartitions
import Definitions.Def_Compat_Mathlib430

noncomputable section

open AlgebraicCurve

namespace AlgebraicCurve

theorem finiteDimensional_adjoin_range {ι : Type} [Fintype ι] (x : ι → AlgebraicClosure ℚ) :
    FiniteDimensional ℚ (IntermediateField.adjoin ℚ (Set.range x)) :=
  IntermediateField.finiteDimensional_adjoin fun y _ =>
    ((AlgebraicClosure.isAlgebraic ℚ).isAlgebraic y).isIntegral

def absLogHeight {ι : Type} [Fintype ι] (x : ι → AlgebraicClosure ℚ) : ℝ :=
  haveI := finiteDimensional_adjoin_range x
  (Module.finrank ℚ (IntermediateField.adjoin ℚ (Set.range x)) : ℝ)⁻¹ *
    Height.logHeight fun i =>
      (⟨x i, IntermediateField.subset_adjoin ℚ (Set.range x) ⟨i, rfl⟩⟩ :
        IntermediateField.adjoin ℚ (Set.range x))

variable {F : Type} [Field F] [Algebra (AlgebraicClosure ℚ) F]

open Classical in

def pivotIndex {r : ℕ} (s : Fin r → F) (v : Place (AlgebraicClosure ℚ) F) (hr : 0 < r) : Fin r :=
  if h : ∃ i : Fin r, ∀ j : Fin r, v.ord (s i) ≤ v.ord (s j) then Classical.choose h else ⟨0, hr⟩

open Classical in

def evalVec {r : ℕ} (s : Fin r → F) (v : Place (AlgebraicClosure ℚ) F) :
    Fin r → AlgebraicClosure ℚ :=
  fun i => if hr : 0 < r then v.evalAt (s i * (s (pivotIndex s v hr))⁻¹) else 0

def chordVec {r : ℕ} (s : Fin r → F) (v w : Place (AlgebraicClosure ℚ) F) :
    Fin r × Fin r → AlgebraicClosure ℚ :=
  fun p => evalVec s v p.1 * evalVec s w p.2 - evalVec s v p.2 * evalVec s w p.1

def pointHt {r : ℕ} (s : Fin r → F) (v : Place (AlgebraicClosure ℚ) F) : ℝ :=
  absLogHeight (evalVec s v)

def pairHt {r : ℕ} (s : Fin r → F) (v w : Place (AlgebraicClosure ℚ) F) : ℝ :=
  pointHt s v + pointHt s w - absLogHeight (chordVec s v w)

open Classical in

def baseHt {r : ℕ} (s : Fin r → F) (b v : Place (AlgebraicClosure ℚ) F) : ℝ :=
  if v = b then 0 else pairHt s v b

def heightFormAux {r : ℕ} (s : Fin r → F) (γ : ℤ) (b : Place (AlgebraicClosure ℚ) F)
    (D : Divisor (AlgebraicClosure ℚ) F) : ℝ :=
  ((γ : ℝ) + (D.sum fun _ n => (n : ℝ)) - 1) * (D.sum fun v n => (n : ℝ) * baseHt s b v)
    - (∑ p ∈ D.support.offDiag, ((D p.1 : ℝ) * (D p.2 : ℝ)) * pairHt s p.1 p.2) / 2
    - (2 - 2 * (γ : ℝ)) * (D.sum fun v n => ((n : ℝ) * ((n : ℝ) - 1) / 2) * baseHt s b v)

def heightForm {r : ℕ} (s : Fin r → F) (γ : ℤ) (b : Place (AlgebraicClosure ℚ) F)
    (D : Divisor (AlgebraicClosure ℚ) F) : ℝ :=
  heightFormAux s γ b (D.erase b)

theorem heightFormAux_two_smul {r : ℕ} (s : Fin r → F) (γ : ℤ) (b : Place (AlgebraicClosure ℚ) F)
    (D : Divisor (AlgebraicClosure ℚ) F) :
    heightFormAux s γ b ((2 : ℤ) • D) = 4 * heightFormAux s γ b D := by
  have hsupp : ((2 : ℤ) • D).support = D.support := Finsupp.support_smul_eq two_ne_zero
  simp only [heightFormAux, Finsupp.sum, hsupp, Finsupp.smul_apply, smul_eq_mul, Int.cast_mul,
    Int.cast_ofNat]
  have h1 : ∑ x ∈ D.support, ((2 : ℝ) * (D x : ℝ)) = 2 * ∑ x ∈ D.support, (D x : ℝ) := by
    rw [Finset.mul_sum]
  have h2 : ∑ x ∈ D.support, (2 : ℝ) * (D x : ℝ) * baseHt s b x
      = 2 * ∑ x ∈ D.support, (D x : ℝ) * baseHt s b x := by
    rw [Finset.mul_sum]; exact Finset.sum_congr rfl fun x _ => by ring
  have h3 : ∑ p ∈ D.support.offDiag, (2 : ℝ) * (D p.1 : ℝ) * ((2 : ℝ) * (D p.2 : ℝ)) * pairHt s p.1 p.2
      = 4 * ∑ p ∈ D.support.offDiag, (D p.1 : ℝ) * (D p.2 : ℝ) * pairHt s p.1 p.2 := by
    rw [Finset.mul_sum]; exact Finset.sum_congr rfl fun x _ => by ring
  have h4 : ∑ x ∈ D.support, (2 : ℝ) * (D x : ℝ) * ((2 : ℝ) * (D x : ℝ) - 1) / 2 * baseHt s b x
      = 4 * (∑ x ∈ D.support, (D x : ℝ) * ((D x : ℝ) - 1) / 2 * baseHt s b x)
        + ∑ x ∈ D.support, (D x : ℝ) * baseHt s b x := by
    rw [Finset.mul_sum, ← Finset.sum_add_distrib]
    exact Finset.sum_congr rfl fun x _ => by ring
  rw [h1, h2, h3, h4]
  ring

theorem heightForm_two_smul {r : ℕ} (s : Fin r → F) (γ : ℤ) (b : Place (AlgebraicClosure ℚ) F)
    (D : Divisor (AlgebraicClosure ℚ) F) :
    heightForm s γ b ((2 : ℤ) • D) = 4 * heightForm s γ b D := by
  unfold heightForm
  rw [two_zsmul, Finsupp.erase_add, ← two_zsmul]
  exact heightFormAux_two_smul s γ b _

theorem heightForm_add_single_base {r : ℕ} (s : Fin r → F) (γ : ℤ) (b : Place (AlgebraicClosure ℚ) F)
    (D : Divisor (AlgebraicClosure ℚ) F) (m : ℤ) :
    heightForm s γ b (D + Finsupp.single b m) = heightForm s γ b D := by
  unfold heightForm
  rw [Finsupp.erase_add, Finsupp.erase_single, add_zero]

end AlgebraicCurve

namespace ModularCurve

variable (N : ℕ) [NeZero N]

def embDegree : ℕ :=
  2 * genusFF (AlgebraicClosure ℚ) (modularFunctionFieldBar N) + 1

def embDivisor : Divisor (AlgebraicClosure ℚ) (modularFunctionFieldBar N) :=
  (embDegree N : ℤ) • Finsupp.single (cuspInftyBar N) 1

def IsEmbBasis {r : ℕ} (s : Fin r → modularFunctionFieldBar N) : Prop :=
  LinearIndependent (AlgebraicClosure ℚ) s ∧
    Submodule.span (AlgebraicClosure ℚ) (Set.range s) = riemannRochSpace (embDivisor N)

def JZero.heightForm {r : ℕ} (s : Fin r → modularFunctionFieldBar N)
    (D : Divisor (AlgebraicClosure ℚ) (modularFunctionFieldBar N)) : ℝ :=
  AlgebraicCurve.heightForm s (genusFF (AlgebraicClosure ℚ) (modularFunctionFieldBar N))
    (cuspInftyBar N) D

theorem JZero.heightForm_two_smul {r : ℕ} (s : Fin r → modularFunctionFieldBar N)
    (D : Divisor (AlgebraicClosure ℚ) (modularFunctionFieldBar N)) :
    JZero.heightForm N s ((2 : ℤ) • D) = 4 * JZero.heightForm N s D :=
  AlgebraicCurve.heightForm_two_smul s _ _ D

theorem JZero.heightForm_add_single_cuspInftyBar {r : ℕ} (s : Fin r → modularFunctionFieldBar N)
    (D : Divisor (AlgebraicClosure ℚ) (modularFunctionFieldBar N)) (m : ℤ) :
    JZero.heightForm N s (D + Finsupp.single (cuspInftyBar N) m) = JZero.heightForm N s D :=
  AlgebraicCurve.heightForm_add_single_base s _ _ D m

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

def JZero.IsRepOf (n : ℕ) (c : ↥(JZero N ^+ ↥K.fixingSubgroup))
    (D : Divisor (AlgebraicClosure ℚ) (modularFunctionFieldBar N)) : Prop :=
  ∃ E : Divisor.degZero (K := AlgebraicClosure ℚ) (F := ↥(modularFunctionFieldBar N)),
    (∀ v, 0 ≤ D v) ∧
    (E : Divisor (AlgebraicClosure ℚ) (modularFunctionFieldBar N))
        + (n : ℤ) • Finsupp.single (cuspInftyBar N) 1 = D ∧
    (∀ σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ, σ ∈ K.fixingSubgroup →
        arithmeticGalois (modularFunctionFieldFull N) σ • D = D) ∧
    Pic0.mk E = (c : JZero N)

theorem JZero.mem_repHeights_iff (n : ℕ) (c : ↥(JZero N ^+ ↥K.fixingSubgroup)) (x : ℝ) :
    x ∈ JZero.repHeights N K n c ↔ ∃ D, JZero.IsRepOf N K n c D ∧ x = divNaiveHeight N K n D := by
  constructor
  · rintro ⟨D, E, h1, h2, h3, h4, h5⟩
    exact ⟨D, ⟨E, h1, h2, h3, h4⟩, h5⟩
  · rintro ⟨D, ⟨E, h1, h2, h3, h4⟩, h5⟩
    exact ⟨D, E, h1, h2, h3, h4, h5⟩

variable {N K}

omit [FiniteDimensional ℚ K] in

theorem JZero.IsRepOf.nsmul {n : ℕ} {c : ↥(JZero N ^+ ↥K.fixingSubgroup)}
    {D : Divisor (AlgebraicClosure ℚ) (modularFunctionFieldBar N)} (h : JZero.IsRepOf N K n c D)
    (m : ℕ) : JZero.IsRepOf N K (m * n) (m • c) (m • D) := by
  obtain ⟨E, hD, hshape, hstab, hc⟩ := h
  refine ⟨m • E, fun v => ?_, ?_, fun σ hσ => ?_, ?_⟩
  · rw [Finsupp.smul_apply]
    exact nsmul_nonneg (hD v) m
  · rw [← hshape, smul_add, AddSubmonoidClass.coe_nsmul, Nat.cast_mul, mul_smul, natCast_zsmul]
  · have key := map_nsmul (DistribSMul.toAddMonoidHom
      (Divisor (AlgebraicClosure ℚ) (modularFunctionFieldBar N))
      (arithmeticGalois (modularFunctionFieldFull N) σ)) m D
    simp only [DistribSMul.toAddMonoidHom_apply] at key
    rw [key, hstab σ hσ]
  · have key : Pic0.mk (m • E) = m • Pic0.mk E := QuotientAddGroup.mk_nsmul _ E m
    rw [key, hc, AddSubmonoidClass.coe_nsmul]

omit [FiniteDimensional ℚ K] in

theorem JZero.IsRepOf.add_single {n : ℕ} {c : ↥(JZero N ^+ ↥K.fixingSubgroup)}
    {D : Divisor (AlgebraicClosure ℚ) (modularFunctionFieldBar N)} (h : JZero.IsRepOf N K n c D)
    (p : ℕ)
    (hfix : ∀ σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ, σ ∈ K.fixingSubgroup →
      arithmeticGalois (modularFunctionFieldFull N) σ • cuspInftyBar N = cuspInftyBar N) :
    JZero.IsRepOf N K (n + p) c (D + (p : ℤ) • Finsupp.single (cuspInftyBar N) 1) := by
  obtain ⟨E, hD, hshape, hstab, hc⟩ := h
  refine ⟨E, fun v => ?_, ?_, fun σ hσ => ?_, hc⟩
  · classical
    have h0 : (0 : ℤ) ≤ ((p : ℤ) • Finsupp.single (cuspInftyBar N) (1 : ℤ)) v := by
      rw [Finsupp.smul_apply, smul_eq_mul, Finsupp.single_apply]
      split_ifs <;> simp
    rw [Finsupp.add_apply]
    exact add_nonneg (hD v) h0
  · rw [← hshape, Nat.cast_add, add_smul, add_assoc]
  · have key := map_zsmul (DistribSMul.toAddMonoidHom
      (Divisor (AlgebraicClosure ℚ) (modularFunctionFieldBar N))
      (arithmeticGalois (modularFunctionFieldFull N) σ)) (p : ℤ)
      (Finsupp.single (cuspInftyBar N) (1 : ℤ))
    simp only [DistribSMul.toAddMonoidHom_apply] at key
    rw [smul_add, hstab σ hσ, key, AlgebraicCurve.SemilinearAut.smul_single, hfix σ hσ]

end ModularCurve

end

Statements phrased using this module (118)