Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_HahnSpecialise.lean

definition module

Specialisation of points and cyclic subgroups over Hahn series

Write H=\bar{\mathbb Q}((s^{\mathbb Q})) for the Hahn-series field with rational exponents over \bar{\mathbb Q}. The module first supplies two facts about the reduction homomorphism reduceHom attached to a Weierstrass model W over a valuation subring A of a field L whose reduction W\bmod\mathfrak m has non-vanishing discriminant: a point P of W_L killed by N, with N invertible in the residue field, and with vanishing reduction is itself 0; consequently reduceHom is injective on the set of points killed by N. Next, CycSubOf G N is the type of subgroups of an additive group G of the form \langle g\rangle for some g of additive order exactly N; for a homomorphism f injective on N-torsion, CycSubOf.addOrderOf_map_of_injOn shows orders are preserved and CycSubOf.map transports such subgroups along f.

The bulk of the module sets up specialisation at s=0. valuationSubringH is the subring \{x\in H:0\le\operatorname{orderTop}(x)\}, upgraded to a valuation subring; resH is the constant-term ring homomorphism to \bar{\mathbb Q}, shown surjective with kernel the maximal ideal, whence residueFieldEquiv identifies the residue field with \bar{\mathbb Q} (and residueAlgEquiv does so as an algebra, algebraQbar being the algebra structure via resH). A unit of the valuation subring is characterised by \operatorname{orderTop}=0. For E over H with IntegralCoeffs E (all a_i of non-negative order), liftModel is the corresponding model over the valuation subring; its reduction, transported along residueFieldEquiv, is specialFibre E (coefficients a_i(0)), and the discriminant \Delta of specialFibre E is non-zero exactly when \operatorname{orderTop}(\Delta(E))=0. Under that hypothesis, specialise is the group homomorphism from E(H) to the group of \bar{\mathbb Q}-points of specialFibre E, reducing a point and applying the residue identification: it sends 0 to 0, sends (x,y) with 0\le\operatorname{orderTop}(x) to (x(0),y(0)), and sends points with x of negative order to 0. It is injective on points killed by a non-zero N, preserves additive order N, and therefore induces specialiseCycSub, a map from cyclic subgroups of E(H) with a generator of order N to those of the special fibre, given on underlying subgroups by the image under specialise.

Relation to Mathlib

Mathlib supplies the ambient notions (HahnSeries, ValuationSubring, residue fields, WeierstrassCurve and its affine point group); CycSubOf is a generic form of the project's CycSub and CycSubH, and the reduction homomorphism reduceHom on points of a Weierstrass model over a valuation subring is the project's own.

Where it is used

The specialisation map is used to compare \Gamma_0(N)-structures on the generic deformation E_{j_0+s} of an elliptic curve of invariant j_0 with those on the curve over \bar{\mathbb Q} obtained at s=0: cyclic subgroups generated by a point of exact order N specialise injectively, which feeds the moduli dictionary for modular polynomials and level structures.

References

  1. J. H. Silverman, The Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 106, Springer, 1986, Ch. VII

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_WeierstrassCurve_ReduceHom
import Definitions.Def_ModularCurve_SpecialisationVocab
import Mathlib.RingTheory.LocalRing.ResidueField.Basic ↗
import Mathlib.RingTheory.Ideal.Quotient.Operations ↗
import Mathlib.GroupTheory.OrderOfElement ↗

set_option autoImplicit false

noncomputable section

open IsLocalRing ValuationSubring
open ModularCurve.TatePoint (Qbar H CycSubH)

namespace WeierstrassCurve

variable {L : Type*} [Field L] {A : ValuationSubring L} {W : WeierstrassCurve A}
variable [DecidableEq L] [DecidableEq (ResidueField A)]
variable (hΔ : (W.map (residue A)).Δ ≠ 0)

omit [DecidableEq (ResidueField A)] in

theorem eq_zero_of_nsmul_eq_zero_of_reducePoint_eq_zero' {N : ℕ} (hN : (N : ResidueField A) ≠ 0)
    (P : (W.map A.subtype).toAffine.Point) (hP : N • P = 0) (h0 : reducePoint hΔ P = 0) :
    P = 0 := by
  cases P with
  | zero => rfl
  | some x y h =>
    exfalso
    have hx : x ∈ A := X_mem_of_nsmul_eq_zero' W hN h hP
    rw [reducePoint_some_of_mem hΔ h hx] at h0
    exact Affine.Point.some_ne_zero _ h0

theorem reduceHom_injOn_nsmul_eq_zero {N : ℕ} (hN : (N : ResidueField A) ≠ 0)
    {P Q : (W.map A.subtype).toAffine.Point} (hP : N • P = 0) (hQ : N • Q = 0)
    (h : reduceHom hΔ P = reduceHom hΔ Q) : P = Q := by
  have h1 : N • (P - Q) = 0 := by rw [nsmul_sub, hP, hQ, sub_zero]
  have h2 : reducePoint hΔ (P - Q) = 0 := by
    show reduceHom hΔ (P - Q) = 0
    rw [map_sub, h, sub_self]
  exact sub_eq_zero.mp (eq_zero_of_nsmul_eq_zero_of_reducePoint_eq_zero' hΔ hN _ h1 h2)

end WeierstrassCurve

def CycSubOf (G : Type*) [AddGroup G] (N : ℕ) : Type _ :=
  {S : AddSubgroup G // ∃ g : G, addOrderOf g = N ∧ S = AddSubgroup.zmultiples g}

namespace CycSubOf

variable {G G' : Type*} [AddCommGroup G] [AddCommGroup G'] (f : G →+ G') {N : ℕ}
variable (hf : ∀ ⦃P Q : G⦄, N • P = 0 → N • Q = 0 → f P = f Q → P = Q)

include hf in

theorem addOrderOf_map_of_injOn {g : G} (hg : addOrderOf g = N) : addOrderOf (f g) = N := by
  apply Nat.dvd_antisymm
  · apply addOrderOf_dvd_of_nsmul_eq_zero
    rw [← map_nsmul, ← hg, addOrderOf_nsmul_eq_zero, map_zero]
  · rw [← hg]
    apply addOrderOf_dvd_of_nsmul_eq_zero
    refine hf ?_ (smul_zero _) ?_
    · rw [smul_comm, ← hg, addOrderOf_nsmul_eq_zero, smul_zero]
    · rw [map_nsmul, addOrderOf_nsmul_eq_zero, map_zero]

def map : CycSubOf G N → CycSubOf G' N := fun S =>
  ⟨S.1.map f, by
    obtain ⟨g, hg, hS⟩ := S.2
    exact ⟨f g, addOrderOf_map_of_injOn f hf hg, by rw [hS, AddMonoidHom.map_zmultiples]⟩⟩

@[simp] theorem coe_map (S : CycSubOf G N) : (map f hf S).1 = S.1.map f := rfl

end CycSubOf

namespace ModularCurve.HahnSpecialise

open ModularCurve.B3

open ModularCurve.TatePoint

def valuationSubringH : ValuationSubring H :=
  { integralO with
  mem_or_inv_mem' := fun x => by
    by_cases hx0 : x = 0
    · left; simp [hx0]
    rcases le_or_gt 0 x.orderTop with h | h
    · exact Or.inl h
    · right
      show 0 ≤ x⁻¹.orderTop
      have hinv : x⁻¹ ≠ 0 := inv_ne_zero hx0
      have h1 : (x * x⁻¹).order = x.order + x⁻¹.order := HahnSeries.order_mul hx0 hinv
      rw [mul_inv_cancel₀ hx0, HahnSeries.order_one] at h1
      have hxord : x.order < 0 := by
        have h' : ((x.order : ℚ) : WithTop ℚ) < 0 := by
          rw [HahnSeries.order_eq_orderTop_of_ne_zero hx0]; exact h
        exact_mod_cast h'
      have h2 : 0 ≤ x⁻¹.order := by linarith
      rw [← HahnSeries.order_eq_orderTop_of_ne_zero hinv]
      exact_mod_cast h2 }

theorem mem_valuationSubringH {x : H} : x ∈ valuationSubringH ↔ 0 ≤ x.orderTop := Iff.rfl

def resH : valuationSubringH →+* Qbar where
  toFun x := (x : H).coeff 0
  map_one' := by simp
  map_mul' x y := coeff_zero_mul_of_integral x.2 y.2
  map_zero' := by simp
  map_add' x y := by simp

@[simp] theorem resH_apply (x : valuationSubringH) : resH x = (x : H).coeff 0 := rfl

theorem resH_eq_resO (x : valuationSubringH) : resH x = resO ⟨(x : H), x.2⟩ := rfl

theorem resH_surjective : Function.Surjective resH := fun c => by
  refine ⟨⟨HahnSeries.C c, ?_⟩, ?_⟩
  · show 0 ≤ (HahnSeries.C c : H).orderTop
    by_cases hc : c = 0
    · simp [hc]
    · rw [HahnSeries.C_apply, HahnSeries.orderTop_single hc]; exact le_rfl
  · show (HahnSeries.C c : H).coeff 0 = c
    simp

theorem ker_resH : RingHom.ker resH = maximalIdeal valuationSubringH :=
  IsLocalRing.eq_maximalIdeal (RingHom.ker_isMaximal_of_surjective resH resH_surjective)

def residueFieldEquiv : ResidueField valuationSubringH ≃+* Qbar :=
  (Ideal.quotEquivOfEq ker_resH.symm).trans (RingHom.quotientKerEquivOfSurjective resH_surjective)

theorem residueFieldEquiv_residue (x : valuationSubringH) :
    residueFieldEquiv (residue valuationSubringH x) = (x : H).coeff 0 := rfl

end ModularCurve.HahnSpecialise

namespace ModularCurve.HahnSpecialise

open ModularCurve.B3

open WeierstrassCurve

def liftModel (E : WeierstrassCurve H) (hE : IntegralCoeffs E) : WeierstrassCurve valuationSubringH :=
  ⟨⟨E.a₁, hE.1⟩, ⟨E.a₂, hE.2.1⟩, ⟨E.a₃, hE.2.2.1⟩, ⟨E.a₄, hE.2.2.2.1⟩, ⟨E.a₆, hE.2.2.2.2⟩⟩

@[simp] theorem liftModel_map_subtype (E : WeierstrassCurve H) (hE : IntegralCoeffs E) :
    (liftModel E hE).map valuationSubringH.subtype = E := by
  cases E; rfl

theorem liftModel_map_residue_map_equiv (E : WeierstrassCurve H) (hE : IntegralCoeffs E) :
    ((liftModel E hE).map (residue valuationSubringH)).map residueFieldEquiv.toRingHom
      = specialFibre E := by
  cases E
  rw [WeierstrassCurve.map_map]
  rfl

theorem isUnit_iff_orderTop_eq_zero (x : valuationSubringH) :
    IsUnit x ↔ (x : H).orderTop = 0 := by
  constructor
  · intro hu
    obtain ⟨y, hy⟩ := hu.exists_right_inv
    have hxy : (x : H) * (y : H) = 1 := by
      have := congrArg (fun z : valuationSubringH => (z : H)) hy
      simpa using this
    have hx0 : (x : H) ≠ 0 := left_ne_zero_of_mul_eq_one hxy
    have hy0 : (y : H) ≠ 0 := right_ne_zero_of_mul_eq_one hxy
    have h1 := HahnSeries.order_mul hx0 hy0
    rw [hxy, HahnSeries.order_one] at h1
    have hx' : 0 ≤ (x : H).order := by
      have h : 0 ≤ (x : H).orderTop := x.2
      rw [← HahnSeries.order_eq_orderTop_of_ne_zero hx0] at h
      exact_mod_cast h
    have hy' : 0 ≤ (y : H).order := by
      have h : 0 ≤ (y : H).orderTop := y.2
      rw [← HahnSeries.order_eq_orderTop_of_ne_zero hy0] at h
      exact_mod_cast h
    have h2 : (x : H).order = 0 := by linarith
    rw [← HahnSeries.order_eq_orderTop_of_ne_zero hx0]
    exact_mod_cast h2
  · intro h0
    have hx0 : (x : H) ≠ 0 := by
      intro hx; rw [hx, HahnSeries.orderTop_zero] at h0; exact WithTop.top_ne_coe h0
    have hinv : 0 ≤ (x : H)⁻¹.orderTop := by
      have hi0 : (x : H)⁻¹ ≠ 0 := inv_ne_zero hx0
      have h1 : ((x : H) * (x : H)⁻¹).order = (x : H).order + (x : H)⁻¹.order :=
        HahnSeries.order_mul hx0 hi0
      rw [mul_inv_cancel₀ hx0, HahnSeries.order_one] at h1
      have hx : (x : H).order = 0 := by
        have := (HahnSeries.order_eq_orderTop_of_ne_zero hx0).trans h0
        exact_mod_cast this
      rw [← HahnSeries.order_eq_orderTop_of_ne_zero hi0]
      have : (x : H)⁻¹.order = 0 := by linarith
      exact_mod_cast this.symm.le
    exact ⟨⟨x, ⟨(x : H)⁻¹, hinv⟩, Subtype.ext (mul_inv_cancel₀ hx0),
      Subtype.ext (inv_mul_cancel₀ hx0)⟩, rfl⟩

theorem map_residue_Δ_ne_zero_of_specialFibre (E : WeierstrassCurve H) (hE : IntegralCoeffs E)
    (hΔ : (specialFibre E).Δ ≠ 0) :
    ((liftModel E hE).map (residue valuationSubringH)).Δ ≠ 0 := by
  intro h0
  apply hΔ
  rw [← liftModel_map_residue_map_equiv E hE, WeierstrassCurve.map_Δ, h0, map_zero]

theorem specialFibre_Δ_ne_zero_iff (E : WeierstrassCurve H) (hE : IntegralCoeffs E) :
    (specialFibre E).Δ ≠ 0 ↔ E.Δ.orderTop = 0 := by
  have h1 : ((liftModel E hE).map valuationSubringH.subtype).Δ =
      valuationSubringH.subtype (liftModel E hE).Δ := by
    simp only [WeierstrassCurve.map_Δ]
  rw [liftModel_map_subtype] at h1
  have h2 : (specialFibre E).Δ =
      residueFieldEquiv (((liftModel E hE).map (residue valuationSubringH)).Δ) := by
    rw [← liftModel_map_residue_map_equiv E hE, WeierstrassCurve.map_Δ]; rfl
  rw [h2, residueFieldEquiv.map_ne_zero_iff, WeierstrassCurve.map_residue_Δ_ne_zero_iff,
    isUnit_iff_orderTop_eq_zero, h1]
  rfl

end ModularCurve.HahnSpecialise

namespace ModularCurve.HahnSpecialise

open ModularCurve.B3

open WeierstrassCurve
open scoped Classical

@[reducible] def algebraQbar : Algebra valuationSubringH Qbar := resH.toAlgebra

attribute [local instance] algebraQbar

@[simp] theorem algebraMap_Qbar_apply (x : valuationSubringH) :
    algebraMap valuationSubringH Qbar x = (x : H).coeff 0 := rfl

def residueAlgEquiv : ResidueField valuationSubringH ≃ₐ[valuationSubringH] Qbar :=
  AlgEquiv.ofRingEquiv (f := residueFieldEquiv) (fun _ => rfl)

variable (E : WeierstrassCurve H) (hE : IntegralCoeffs E)

def specialFibrePointMap :
    ((liftModel E hE).map (residue valuationSubringH)).toAffine.Point →+
      (specialFibre E).toAffine.Point :=
  (Affine.Point.map (W' := (liftModel E hE).toAffine)
    (residueAlgEquiv : ResidueField valuationSubringH →ₐ[valuationSubringH] Qbar) :)

theorem specialFibrePointMap_injective : Function.Injective (specialFibrePointMap E hE) :=
  Affine.Point.map_injective _

def specialise (hΔ : (specialFibre E).Δ ≠ 0) : E.toAffine.Point →+ (specialFibre E).toAffine.Point :=
  (specialFibrePointMap E hE).comp
    ((reduceHom (map_residue_Δ_ne_zero_of_specialFibre E hE hΔ) :
      ((liftModel E hE).map valuationSubringH.subtype).toAffine.Point →+ _) :)

include hE in

theorem nonsingular_specialFibre_coeff_zero (hΔ : (specialFibre E).Δ ≠ 0) {x y : H}
    (h : E.toAffine.Nonsingular x y) (hx : 0 ≤ x.orderTop) :
    (specialFibre E).toAffine.Nonsingular (x.coeff 0) (y.coeff 0) := by
  have h' : ((liftModel E hE).map valuationSubringH.subtype).toAffine.Nonsingular x y := by
    rw [liftModel_map_subtype]; exact h
  have hy : y ∈ valuationSubringH := WeierstrassCurve.Affine.Y_mem_of_X_mem (liftModel E hE) h'.1 hx
  have hres := WeierstrassCurve.Affine.nonsingular_residue (liftModel E hE)
    (map_residue_Δ_ne_zero_of_specialFibre E hE hΔ) (x := ⟨x, hx⟩) (y := ⟨y, hy⟩) h'.1
  have hmap := ((((liftModel E hE).map (residue valuationSubringH)).toAffine.map_nonsingular
    (f := residueFieldEquiv.toRingHom) residueFieldEquiv.injective
    (residue valuationSubringH ⟨x, hx⟩) (residue valuationSubringH ⟨y, hy⟩)).mpr hres)
  rw [show ((liftModel E hE).map (residue valuationSubringH)).toAffine.map residueFieldEquiv.toRingHom
      = (specialFibre E).toAffine from liftModel_map_residue_map_equiv E hE] at hmap
  exact hmap

@[simp] theorem specialise_zero (hΔ : (specialFibre E).Δ ≠ 0) : specialise E hE hΔ 0 = 0 :=
  map_zero _

theorem specialise_some_of_nonneg (hΔ : (specialFibre E).Δ ≠ 0) {x y : H}
    (h : E.toAffine.Nonsingular x y) (hx : 0 ≤ x.orderTop) :
    specialise E hE hΔ (.some x y h) =
      .some (x.coeff 0) (y.coeff 0) (nonsingular_specialFibre_coeff_zero E hE hΔ h hx) := by
  have h' : ((liftModel E hE).map valuationSubringH.subtype).toAffine.Nonsingular x y := by
    rw [liftModel_map_subtype]; exact h
  show specialFibrePointMap E hE (reducePoint (map_residue_Δ_ne_zero_of_specialFibre E hE hΔ)
    (.some x y h')) = _
  rw [WeierstrassCurve.reducePoint_some_of_mem _ h' hx]
  show Affine.Point.map _ (Affine.Point.some _ _ _) = _
  rw [Affine.Point.map_some]
  rfl

theorem specialise_some_of_neg (hΔ : (specialFibre E).Δ ≠ 0) {x y : H}
    (h : E.toAffine.Nonsingular x y) (hx : ¬ 0 ≤ x.orderTop) :
    specialise E hE hΔ (.some x y h) = 0 := by
  have h' : ((liftModel E hE).map valuationSubringH.subtype).toAffine.Nonsingular x y := by
    rw [liftModel_map_subtype]; exact h
  show specialFibrePointMap E hE (reducePoint (map_residue_Δ_ne_zero_of_specialFibre E hE hΔ)
    (.some x y h')) = _
  rw [WeierstrassCurve.reducePoint_some_of_notMem _ h' hx, map_zero]

theorem natCast_residueField_ne_zero {N : ℕ} (hN : N ≠ 0) :
    (N : ResidueField valuationSubringH) ≠ 0 := by
  intro h
  have := congrArg residueFieldEquiv h
  rw [map_natCast, map_zero] at this
  exact (Nat.cast_ne_zero.mpr hN) this

theorem specialise_injOn_nsmul_eq_zero (hΔ : (specialFibre E).Δ ≠ 0) {N : ℕ} (hN : N ≠ 0)
    {P Q : E.toAffine.Point} (hP : N • P = 0) (hQ : N • Q = 0)
    (h : specialise E hE hΔ P = specialise E hE hΔ Q) : P = Q :=
  reduceHom_injOn_nsmul_eq_zero (W := liftModel E hE) (map_residue_Δ_ne_zero_of_specialFibre E hE hΔ)
    (natCast_residueField_ne_zero hN) hP hQ (specialFibrePointMap_injective E hE h)

theorem addOrderOf_specialise (hΔ : (specialFibre E).Δ ≠ 0) {N : ℕ} (hN : N ≠ 0)
    {g : E.toAffine.Point} (hg : addOrderOf g = N) : addOrderOf (specialise E hE hΔ g) = N :=
  CycSubOf.addOrderOf_map_of_injOn (specialise E hE hΔ)
    (fun _ _ hP hQ h => specialise_injOn_nsmul_eq_zero E hE hΔ hN hP hQ h) hg

end ModularCurve.HahnSpecialise

namespace ModularCurve.HahnSpecialise

open ModularCurve.B3

open scoped Classical

variable (E : WeierstrassCurve H) (hE : IntegralCoeffs E) (hΔ : (specialFibre E).Δ ≠ 0)

def specialiseCycSub (N : ℕ) [NeZero N] : CycSubH E N → CycSub (specialFibre E) N :=
  (CycSubOf.map (specialise E hE hΔ)
    (fun _ _ hP hQ h => specialise_injOn_nsmul_eq_zero E hE hΔ (NeZero.ne N) hP hQ h) :)

@[simp] theorem coe_specialiseCycSub (N : ℕ) [NeZero N] (S : CycSubH E N) :
    (specialiseCycSub E hE hΔ N S).1 = S.1.map (specialise E hE hΔ) := rfl

end ModularCurve.HahnSpecialise

end

Statements phrased using this module (3)