Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_NodeDescentTower.lean

definition module

Tower fieldOver modularFunctionFieldBar, integral at prime level

Fix a natural number N \neq 0 and an intermediate field K of \overline{\mathbb Q}/\mathbb Q. Inside \overline{\mathbb Q}((q)) the project's subfield fieldOver N K is generated by the constant series of elements of K together with the two Laurent series jqModC (= j(q), the q-expansion of j with coefficients read in \overline{\mathbb Q}) and jqNModC (= j(q^N), its image under the N-fold substitution qExpand); modularFunctionFieldBar N is the intermediate field of \overline{\mathbb Q}((q))/\overline{\mathbb Q} generated by the coefficientwise image of \mathbb Q\bigl(j(q^d) : d \mid N\bigr). This module equips these two fields with the algebra structures making them a tower. The constant-series map c \mapsto \mathrm{C}(c) realises K as a subfield of fieldOver N K, compatibly with the structural map \overline{\mathbb Q} \to \overline{\mathbb Q}((q)); the containment fieldOver N K \subseteq modularFunctionFieldBar N (proved from the facts that the coefficient embedding carries j to jqModC and commutes with qExpand) supplies the second algebra map; and the resulting scalar towers K \to fieldOver N K \to modularFunctionFieldBar N and fieldOver N K \to modularFunctionFieldBar N \to \overline{\mathbb Q}((q)) are recorded, as are the characteristic-zero instances for \overline{\mathbb Q}((q)) and for fieldOver N K.

The last section specialises to a prime q, the level being written throughout as 1 \cdot q. Since the divisors of q are 1 and q, the coefficient embedding sends \mathbb Q\bigl(j(q^d) : d \mid q\bigr) into fieldOver (1 * q) K; combined with the fact that every constant c \in \overline{\mathbb Q} is integral over fieldOver (1 * q) K (being algebraic over \mathbb Q), this yields that modularFunctionFieldBar (1 * q) is an integral — hence algebraic — extension of fieldOver (1 * q) K.

Relation to Mathlib

The Laurent/Hahn series, intermediate fields, IsScalarTower and integrality API are Mathlib's; fieldOver, modularFunctionFieldBar, jqModC, jqNModC and qExpand are the project's own notions, and the algebra maps here are built from Mathlib's subfield and subring inclusions.

Where it is used

These instances make a place of fieldOver N K over K, and the restriction along fieldOver N K \subseteq modularFunctionFieldBar N of a place of the geometric modular function field, well-typed; the prime-level integrality is what restriction of places along this inclusion requires. They serve the local analysis of X_0(q) at the nodes of its reduction, used in the level-lowering half of the argument.

References

  1. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Princeton University Press, 1971, Chapter 6
  2. F. Diamond and J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_NodeDescent
import Definitions.Def_ModularCurve_ArithmeticGalois

set_option autoImplicit false

noncomputable section

namespace ModularCurve
namespace NodeLocalized

open CharPReduction

variable (N : ℕ) [NeZero N] (K : IntermediateField ℚ (AlgebraicClosure ℚ))

instance charZero_laurentSeries_algClosure : CharZero (LaurentSeries (AlgebraicClosure ℚ)) :=
  charZero_of_injective_ringHom (HahnSeries.C_injective (Γ := ℤ) (R := AlgebraicClosure ℚ))

instance charZero_fieldOver : CharZero (fieldOver N K) :=
  (fieldOver N K).subtype.charZero

theorem constSeries_mem_fieldOver (c : K) :
    constSeries K.toSubalgebra.toSubring c ∈ fieldOver N K :=
  Subfield.subset_closure (Or.inl ⟨c, rfl⟩)

instance algebraFieldOver : Algebra K (fieldOver N K) :=
  RingHom.toAlgebra
    { toFun := fun c => ⟨constSeries K.toSubalgebra.toSubring c, constSeries_mem_fieldOver N K c⟩
      map_one' := Subtype.ext (map_one _)
      map_mul' := fun x y => Subtype.ext (map_mul _ x y)
      map_zero' := Subtype.ext (map_zero _)
      map_add' := fun x y => Subtype.ext (map_add _ x y) }

theorem algebraMap_fieldOver_coe (c : K) :
    ((algebraMap K (fieldOver N K) c : fieldOver N K) : LaurentSeries (AlgebraicClosure ℚ))
      = algebraMap (AlgebraicClosure ℚ) (LaurentSeries (AlgebraicClosure ℚ)) (c : AlgebraicClosure ℚ) :=
  rfl

theorem coeffEmb_jq_eq : coeffEmb (AlgebraicClosure ℚ) jq = jqModC (AlgebraicClosure ℚ) := by
  rw [← jqModC_rat]
  exact map_jqModC (algebraMap ℚ (AlgebraicClosure ℚ))

theorem coeffEmb_qExpand_eq (x : LaurentSeries ℚ) :
    coeffEmb (AlgebraicClosure ℚ) (qExpand ℚ N x) = qExpand (AlgebraicClosure ℚ) N (coeffEmb (AlgebraicClosure ℚ) x) := by
  ext m
  simp only [coeffEmb_coeff]
  by_cases h : (N : ℤ) ∣ m
  · obtain ⟨k, rfl⟩ := h
    rw [qExpand_coeff_mul, qExpand_coeff_mul, coeffEmb_coeff]
  · rw [qExpand_coeff_of_not_dvd _ _ h, qExpand_coeff_of_not_dvd _ _ h, map_zero]

theorem fieldOver_le_modularFunctionFieldBar :
    (fieldOver N K).toSubring ≤ (modularFunctionFieldBar N).toSubring := by
  change Subfield.closure _ ≤ (modularFunctionFieldBar N).toSubfield
  rw [Subfield.closure_le]
  rintro x (⟨c, rfl⟩ | rfl | rfl)
  · exact (modularFunctionFieldBar N).algebraMap_mem (c : AlgebraicClosure ℚ)
  · change jqModC (AlgebraicClosure ℚ) ∈ modularFunctionFieldBar N
    rw [← coeffEmb_jq_eq]
    exact coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionField_le_full N (jq_mem N))
  · change jqNModC (AlgebraicClosure ℚ) N ∈ modularFunctionFieldBar N
    rw [jqNModC, ← coeffEmb_jq_eq, ← coeffEmb_qExpand_eq]
    exact coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) (jqd_mem_full N (dvd_refl N))

instance algebraFieldOverBar : Algebra (fieldOver N K) (modularFunctionFieldBar N) :=
  (Subring.inclusion (fieldOver_le_modularFunctionFieldBar N K)).toAlgebra

theorem algebraMap_fieldOver_bar_coe (x : fieldOver N K) :
    ((algebraMap (fieldOver N K) (modularFunctionFieldBar N) x : modularFunctionFieldBar N)
      : LaurentSeries (AlgebraicClosure ℚ)) = x :=
  rfl

instance isScalarTower_fieldOver_bar_laurent :
    IsScalarTower (fieldOver N K) (modularFunctionFieldBar N) (LaurentSeries (AlgebraicClosure ℚ)) :=
  IsScalarTower.of_algebraMap_eq (R := fieldOver N K) (S := modularFunctionFieldBar N)
    (A := LaurentSeries (AlgebraicClosure ℚ)) (fun _ => rfl)

instance isScalarTower_K_fieldOver_bar :
    IsScalarTower K (fieldOver N K) (modularFunctionFieldBar N) :=
  IsScalarTower.of_algebraMap_eq (R := K) (S := fieldOver N K) (A := modularFunctionFieldBar N)
    (fun _ => Subtype.ext rfl)

section PrimeLevel

variable (q : ℕ) [Fact q.Prime]

theorem coeffEmb_mem_fieldOver_of_mem_full {x : LaurentSeries ℚ} (hx : x ∈ modularFunctionFieldFull (1 * q)) :
    coeffEmb (AlgebraicClosure ℚ) x ∈ fieldOver (1 * q) K := by
  have hq : q.Prime := Fact.out

  change x ∈ Subfield.closure (Set.range (algebraMap ℚ (LaurentSeries ℚ)) ∪ divisorExpansions (1 * q)) at hx
  induction hx using Subfield.closure_induction with
  | mem y hy =>
      rcases hy with ⟨c, rfl⟩ | ⟨d, hd, hdvd, rfl⟩
      · rw [algebraMap_apply_eq_single, coeffEmb, coeffMap_single]
        rw [← algebraMap_laurentSeries_eq_single]
        exact Subfield.subset_closure (Or.inl ⟨⟨algebraMap ℚ (AlgebraicClosure ℚ) c,
          IntermediateField.algebraMap_mem K c⟩, rfl⟩)
      · haveI := hd
        rw [coeffEmb_qExpand_eq, coeffEmb_jq_eq]
        have hdvd' : d ∣ q := by simpa using hdvd
        rcases (Nat.dvd_prime hq).mp hdvd' with rfl | hdq
        · rw [qExpand_one_apply]
          exact Subfield.subset_closure (Or.inr (Set.mem_insert _ _))
        · have : qExpand (AlgebraicClosure ℚ) d (jqModC (AlgebraicClosure ℚ))
              = jqNModC (AlgebraicClosure ℚ) (1 * q) := by
            rw [jqNModC]; exact qExpand_congr (by rw [hdq, one_mul]) _
          rw [this]
          exact Subfield.subset_closure (Or.inr (Set.mem_insert_of_mem _ rfl))
  | one => rw [map_one]; exact one_mem _
  | add x y _ _ hx hy => rw [map_add]; exact add_mem hx hy
  | neg x _ hx => rw [map_neg]; exact neg_mem hx
  | inv x _ hx => rw [map_inv₀]; exact inv_mem hx
  | mul x y _ _ hx hy => rw [map_mul]; exact mul_mem hx hy

theorem isIntegral_fieldOver_algebraMap_laurent (c : AlgebraicClosure ℚ) :
    IsIntegral (fieldOver (1 * q) K)
      (algebraMap (AlgebraicClosure ℚ) (LaurentSeries (AlgebraicClosure ℚ)) c) := by
  have halg : Algebra.IsAlgebraic ℚ (AlgebraicClosure ℚ) := by
    convert AlgebraicClosure.isAlgebraic ℚ <;>
      first | with_reducible_and_instances rfl | exact Subsingleton.elim _ _
  obtain ⟨p, hp, hpc⟩ := (halg.isAlgebraic c).isIntegral
  refine ⟨p.map (algebraMap ℚ (fieldOver (1 * q) K)), hp.map _, ?_⟩
  rw [Polynomial.eval₂_map,
    RingHom.ext_rat ((algebraMap ↥(fieldOver (1 * q) K) (LaurentSeries (AlgebraicClosure ℚ))).comp
        (algebraMap ℚ ↥(fieldOver (1 * q) K)))
      ((algebraMap (AlgebraicClosure ℚ) (LaurentSeries (AlgebraicClosure ℚ))).comp
        (algebraMap ℚ (AlgebraicClosure ℚ))),
    ← Polynomial.hom_eval₂, hpc, map_zero]

instance algebra_isIntegral_fieldOver_bar :
    Algebra.IsIntegral (fieldOver (1 * q) K) (modularFunctionFieldBar (1 * q)) := by
  refine ⟨fun x => ?_⟩
  rw [← isIntegral_algHom_iff (IsScalarTower.toAlgHom ↥(fieldOver (1 * q) K)
      ↥(modularFunctionFieldBar (1 * q)) (LaurentSeries (AlgebraicClosure ℚ))) Subtype.val_injective]
  change IsIntegral (fieldOver (1 * q) K) (x : LaurentSeries (AlgebraicClosure ℚ))
  suffices h : ∀ y ∈ Subfield.closure
      (Set.range (algebraMap (AlgebraicClosure ℚ) (LaurentSeries (AlgebraicClosure ℚ))) ∪
        ⇑(coeffEmb (AlgebraicClosure ℚ)) '' (modularFunctionFieldFull (1 * q) : Set (LaurentSeries ℚ))),
      IsIntegral (fieldOver (1 * q) K) y from h _ (mem_laurentBaseChange_iff.mp x.2)
  intro y hy
  induction hy using Subfield.closure_induction with
  | mem y hy =>
      rcases hy with ⟨c, rfl⟩ | ⟨z, hz, rfl⟩
      · exact isIntegral_fieldOver_algebraMap_laurent K q c
      · exact isIntegral_algebraMap (R := ↥(fieldOver (1 * q) K))
          (x := ⟨_, coeffEmb_mem_fieldOver_of_mem_full K q hz⟩)
  | one => exact isIntegral_one
  | add y z _ _ hy hz => exact hy.add hz
  | neg y _ hy => exact hy.neg
  | inv y _ hy => exact hy.inv
  | mul y z _ _ hy hz => exact hy.mul hz

end PrimeLevel

end NodeLocalized
end ModularCurve

end

Statements phrased using this module (2)