Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_QExpSemistableSpecializationPinnedV3.lean

definition module

Pinned semistable specialisation datum for -expansion curves, V3

Over the standing data — an intermediate field F_0 of \mathbb{Q}((q))/\mathbb{Q}, a valuation subring P of \overline{\mathbb{Q}}, a subgroup I \le \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}), a natural number q, a field k with a ring homomorphism \pi : P \to k, an intermediate field \bar F of k((q))/k and a further pair F_1 \subseteq \mathbb{Q}((q)), \bar F_1 \subseteq k((q)) — the structure QExpSemistableSpecializationPinnedV3 packages, as fields, a collection of objects together with the properties they are required to satisfy. Its data are: a finite set nodes of pairs of places of \bar F/k whose residue fields are generated by k (the maps k \to residue field are surjective); a semilinear automorphism frob of \bar F over k acting on q-expansions by raising every Laurent coefficient to the q-th power; an additive subgroup dom of \mathrm{Pic}^0 of \overline{\mathbb{Q}}\cdot F_0, pointwise fixed by I and stable under every \varphi that is a Frobenius at P with exponent q and normalises I (in the form \sigma \in I \leftrightarrow \varphi\sigma\varphi^{-1} \in I); and an additive map sp from dom to the glued group \mathrm{GluedPic}^0(k,\bar F,\text{nodes}), that is, admissible pairs of degree-zero divisors vanishing at the nodes together with node units, modulo glued principal data. The asserted properties are: sp is injective and surjective on elements killed by some n>0 with q \nmid n; for each such n the n-torsion of \mathrm{Pic}^0 is finite of order the product of the cardinality of the n-torsion of \mathrm{GluedPic}^0 and that of its subgroup with vanishing image under toPic0Pair; the first component of \mathrm{toPic0Pair}\circ\mathrm{sp} is equivariant for Frobenius at P versus frob; a compatibility identifying that first component with the class of a conorm divisor \bar D, for conorms along integral q-expansion-preserving inclusions \iota, \bar\iota and a place-reduction map r_1 satisfying IsLaurentPlaceReduction and LaurentPrincipalGeneratedByIntegral; and the vanishing of the Weil pairing d.\mathrm{pairing} = \mathrm{evalFun}(f_1,D_2)/\mathrm{evalFun}(f_2,D_1), i.e. its equality with 1, whenever the class of E_1 = D_1 lies in dom with \mathrm{toPic0Pair}(\mathrm{sp}\,E_1) = 0.

Compared with QExpSemistableSpecializationPinned, the present version carries the same fields except that no requirement is imposed that some m>0 multiply every I-fixed class into dom. The accompanying lemmas record that the base automorphism of frob is a \mapsto a^q on k; that the action of frob on \bar F is the same for any two such data with the same F_0,P,q,k,\pi,\bar F; define toricPart as the kernel of \mathrm{toPic0Pair}\circ\mathrm{sp} on dom; and extend the pairing statement, via the symmetry d \mapsto d.\mathrm{symm} which inverts the pairing, to the case where either E_1 or E_2 has class in the toric part.

Relation to Mathlib

Mathlib supplies the ambient notions (Laurent series, intermediate fields, valuation subrings, Frobenius and inertia data for valuations); places, divisors, \mathrm{Pic}^0, the glued Picard group of two branches along a finite set of node pairs, semilinear automorphisms of function fields, Weil data with their pairing, and the reduction predicates for q-expansion fields are all project notions with no Mathlib counterpart.

Where it is used

The structure axiomatises what is needed about the semistable specialisation of the Jacobian of a modular curve presented by q-expansions at a prime above q: the character-group (toric) part, the Frobenius action on the component group side, the comparison with a good-reduction quotient, and the triviality of Weil pairings on the toric part. These inputs feed the level-lowering step for the Galois representation attached to a Frey curve.

References

  1. K. A. Ribet, On modular representations of \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) arising from modular forms, Inventiones Mathematicae 100 (1990), 431–476
  2. 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

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_FLTPrelim_Ramification
import Definitions.Def_EllipticCurve_FrobeniusTrace
import Definitions.Def_AlgebraicCurve_GluedPic0
import Definitions.Def_AlgebraicCurve_Correspondence
import Definitions.Def_AlgebraicCurve_WeilDatum
import Definitions.Def_ModularCurve_ArithmeticGalois
import Definitions.Def_ModularCurve_QExpReductionModL
import Definitions.Def_ModularCurve_QExpSemistableSpecializationPinned

set_option autoImplicit false

noncomputable section

open AlgebraicCurve IntermediateField

namespace ModularCurve

section Datum

variable (F₀ : IntermediateField ℚ (LaurentSeries ℚ))
variable (P : ValuationSubring (AlgebraicClosure ℚ))
variable (I : Subgroup (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ)) (q : ℕ)
variable (k : Type) [Field k] (π : P →+* k)
variable (Fbar : IntermediateField k (LaurentSeries k))
variable (F₁ : IntermediateField ℚ (LaurentSeries ℚ)) (Fbar₁ : IntermediateField k (LaurentSeries k))

set_option maxHeartbeats 1000000 in

structure QExpSemistableSpecializationPinnedV3 where

  nodes : Finset (Place k Fbar × Place k Fbar)

  nodes_rational : ∀ s ∈ nodes,
    Function.Surjective (algebraMap k s.1.ResidueField) ∧
      Function.Surjective (algebraMap k s.2.ResidueField)

  frob : SemilinearAut k Fbar

  coeff_frob_smul : ∀ (x : Fbar) (n : ℤ),
    ((frob • x : Fbar) : LaurentSeries k).coeff n = ((x : LaurentSeries k).coeff n) ^ q

  dom : AddSubgroup (Pic0 (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) F₀))

  smul_eq_self_of_mem_dom : ∀ y ∈ dom, ∀ σ ∈ I, σ • y = y

  smul_mem_dom_of_isFrobeniusAt : ∀ φ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ,
    P.IsFrobeniusAt φ q → (∀ σ, σ ∈ I ↔ φ * σ * φ⁻¹ ∈ I) → ∀ y ∈ dom, φ • y ∈ dom

  sp : dom →+ GluedPic0 k Fbar nodes

  sp_injective : ∀ y : dom,
    (∃ n : ℕ, 0 < n ∧ ¬ q ∣ n ∧
      n • (y : Pic0 (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) F₀)) = 0) →
      sp y = 0 → y = 0

  sp_surjective : ∀ ξ : GluedPic0 k Fbar nodes, (∃ n : ℕ, 0 < n ∧ ¬ q ∣ n ∧ n • ξ = 0) →
    ∃ y : dom, (∃ n : ℕ, 0 < n ∧ ¬ q ∣ n ∧
      n • (y : Pic0 (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) F₀)) = 0) ∧ sp y = ξ

  finite_torsion_and_natCard_eq : ∀ n : ℕ, 0 < n → ¬ q ∣ n →
    Finite (Pic0.torsion (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) F₀) n) ∧
      Nat.card (Pic0.torsion (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) F₀) n) =
        Nat.card {ξ : GluedPic0 k Fbar nodes // n • ξ = 0} *
          Nat.card {ξ : GluedPic0 k Fbar nodes // n • ξ = 0 ∧ GluedPic0.toPic0Pair nodes ξ = 0}

  toPic0Pair_sp_fst_smul_of_isFrobeniusAt : ∀ φ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ,
    P.IsFrobeniusAt φ q → ∀ (y : dom)
      (h : φ • (y : Pic0 (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) F₀)) ∈ dom),
      (GluedPic0.toPic0Pair nodes
          (sp ⟨φ • (y : Pic0 (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) F₀)), h⟩)).1 =
        frob • (GluedPic0.toPic0Pair nodes (sp y)).1

  toPic0Pair_sp_fst_eq :
    ∀ (r₁ : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) F₁) → Place k Fbar₁),
      IsLaurentPlaceReduction P π F₁ Fbar₁ r₁ →
      LaurentPrincipalGeneratedByIntegral P π F₁ Fbar₁ →
      ∀ (ι : laurentBaseChange (AlgebraicClosure ℚ) F₁ →ₐ[AlgebraicClosure ℚ]
          laurentBaseChange (AlgebraicClosure ℚ) F₀)
        (hι : ι.toRingHom.IsIntegral) (ῑ : Fbar₁ →ₐ[k] Fbar) (hῑ : ῑ.toRingHom.IsIntegral),
        QExpSemistable.IsQExpInclusion ι → QExpSemistable.IsQExpInclusion ῑ →
        ∀ (D₁ : Divisor.degZero (K := AlgebraicClosure ℚ)
            (F := laurentBaseChange (AlgebraicClosure ℚ) F₁))
          (D : Divisor.degZero (K := AlgebraicClosure ℚ)
            (F := laurentBaseChange (AlgebraicClosure ℚ) F₀)),
          QExpSemistable.IsConormAlong ι hι
            (D₁ : Divisor (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) F₁))
            (D : Divisor (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) F₀)) →
          ∀ (hD : Pic0.mk D ∈ dom) (Dbar : Divisor.degZero (K := k) (F := Fbar)),
            QExpSemistable.IsConormAlong ῑ hῑ
              (Finsupp.mapDomain r₁
                (D₁ : Divisor (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) F₁)))
              (Dbar : Divisor k Fbar) →
            (GluedPic0.toPic0Pair nodes (sp ⟨Pic0.mk D, hD⟩)).1 = Pic0.mk Dbar

  pairing_eq_one_of_toPic0Pair_sp_eq_zero : ∀ (n : ℕ), 0 < n → ¬ q ∣ n →
    ∀ (d : WeilDatum (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) F₀) n)
      (E₁ E₂ : Divisor.degZero (K := AlgebraicClosure ℚ)
        (F := laurentBaseChange (AlgebraicClosure ℚ) F₀)),
      (E₁ : Divisor (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) F₀)) = d.D₁ →
      (E₂ : Divisor (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) F₀)) = d.D₂ →
      ∀ (h₁ : Pic0.mk E₁ ∈ dom), Pic0.mk E₂ ∈ dom →
        GluedPic0.toPic0Pair nodes (sp ⟨Pic0.mk E₁, h₁⟩) = 0 → d.pairing = 1

end Datum

namespace QExpSemistableSpecializationPinnedV3

variable {F₀ : IntermediateField ℚ (LaurentSeries ℚ)}
variable {P : ValuationSubring (AlgebraicClosure ℚ)}
variable {I : Subgroup (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ)} {q : ℕ}
variable {k : Type} [Field k] {π : P →+* k}
variable {Fbar : IntermediateField k (LaurentSeries k)}
variable {F₁ : IntermediateField ℚ (LaurentSeries ℚ)} {Fbar₁ : IntermediateField k (LaurentSeries k)}
variable (𝒟 : QExpSemistableSpecializationPinnedV3 F₀ P I q k π Fbar F₁ Fbar₁)

theorem baseAut_frob (a : k) : SemilinearAut.baseAut 𝒟.frob a = a ^ q := by
  have hcoe : ∀ b : k, ((algebraMap k Fbar b : Fbar) : LaurentSeries k).coeff 0 = b := fun b => by
    have e : ((algebraMap k Fbar b : Fbar) : LaurentSeries k) = algebraMap k (LaurentSeries k) b :=
      IntermediateField.coe_algebraMap_apply Fbar b
    rw [e, algebraMap_laurentSeries_eq_single, HahnSeries.coeff_single_same]
  have h₁ := 𝒟.coeff_frob_smul (algebraMap k Fbar a) 0
  rw [SemilinearAut.smul_algebraMap, hcoe, hcoe] at h₁
  exact h₁

theorem frob_smul_eq {I' : Subgroup (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ)}
    {F₁' : IntermediateField ℚ (LaurentSeries ℚ)} {Fbar₁' : IntermediateField k (LaurentSeries k)}
    (𝒟' : QExpSemistableSpecializationPinnedV3 F₀ P I' q k π Fbar F₁' Fbar₁') (x : Fbar) :
    𝒟.frob • x = 𝒟'.frob • x := by
  refine Subtype.ext (HahnSeries.ext (funext fun n => ?_))
  rw [𝒟.coeff_frob_smul, 𝒟'.coeff_frob_smul]

def toricPart : AddSubgroup 𝒟.dom :=
  ((GluedPic0.toPic0Pair 𝒟.nodes).comp 𝒟.sp).ker

theorem mem_toricPart {y : 𝒟.dom} :
    y ∈ 𝒟.toricPart ↔ GluedPic0.toPic0Pair 𝒟.nodes (𝒟.sp y) = 0 :=
  Iff.rfl

theorem pairing_eq_one_of_toPic0Pair_sp_eq_zero_right {n : ℕ} (hn : 0 < n) (hqn : ¬ q ∣ n)
    (d : WeilDatum (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) F₀) n)
    (E₁ E₂ : Divisor.degZero (K := AlgebraicClosure ℚ)
      (F := laurentBaseChange (AlgebraicClosure ℚ) F₀))
    (hE₁ : (E₁ : Divisor (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) F₀)) = d.D₁)
    (hE₂ : (E₂ : Divisor (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) F₀)) = d.D₂)
    (h₁ : Pic0.mk E₁ ∈ 𝒟.dom) (h₂ : Pic0.mk E₂ ∈ 𝒟.dom)
    (htor : GluedPic0.toPic0Pair 𝒟.nodes (𝒟.sp ⟨Pic0.mk E₂, h₂⟩) = 0) : d.pairing = 1 := by
  have h := 𝒟.pairing_eq_one_of_toPic0Pair_sp_eq_zero n hn hqn d.symm E₂ E₁ hE₂ hE₁ h₂ h₁ htor
  have hd : d.symm.pairing = d.pairing⁻¹ := by
    show Divisor.evalFun d.f₂ d.D₁ / Divisor.evalFun d.f₁ d.D₂ =
      (Divisor.evalFun d.f₁ d.D₂ / Divisor.evalFun d.f₂ d.D₁)⁻¹
    rw [inv_div]
  rw [hd] at h
  exact inv_eq_one.mp h

theorem pairing_eq_one_of_mem_toricPart {n : ℕ} (hn : 0 < n) (hqn : ¬ q ∣ n)
    (d : WeilDatum (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) F₀) n)
    (E₁ E₂ : Divisor.degZero (K := AlgebraicClosure ℚ)
      (F := laurentBaseChange (AlgebraicClosure ℚ) F₀))
    (hE₁ : (E₁ : Divisor (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) F₀)) = d.D₁)
    (hE₂ : (E₂ : Divisor (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) F₀)) = d.D₂)
    (h₁ : Pic0.mk E₁ ∈ 𝒟.dom) (h₂ : Pic0.mk E₂ ∈ 𝒟.dom)
    (htor : (⟨Pic0.mk E₁, h₁⟩ : 𝒟.dom) ∈ 𝒟.toricPart ∨ (⟨Pic0.mk E₂, h₂⟩ : 𝒟.dom) ∈ 𝒟.toricPart) :
    d.pairing = 1 := by
  rcases htor with ht | ht
  · exact 𝒟.pairing_eq_one_of_toPic0Pair_sp_eq_zero n hn hqn d E₁ E₂ hE₁ hE₂ h₁ h₂ ht
  · exact 𝒟.pairing_eq_one_of_toPic0Pair_sp_eq_zero_right hn hqn d E₁ E₂ hE₁ hE₂ h₁ h₂ ht

end QExpSemistableSpecializationPinnedV3

end ModularCurve

end

Statements phrased using this module (19)