Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_ArithmeticGalois.lean

definition module

Coefficientwise Galois action on base-changed Laurent subfields;

Fix a field L with a \mathbb{Q}-algebra structure and an intermediate field F_0 of \mathbb{Q}((q))/\mathbb{Q}, and let L\cdot F_0 = laurentBaseChange L F₀ be the intermediate field of L((q))/L generated over L by the coefficientwise image of F_0 under \mathbb{Q}\to L. For \sigma : L \simeq_{\mathbb{Q}} L, arithmeticRingAut F₀ σ is the ring automorphism of L\cdot F_0 obtained by applying \sigma to each Laurent coefficient (coeffMap), with inverse given by \sigma^{-1}; stability of L\cdot F_0 under this operation is inherited from coeffMap_mem_laurentBaseChange, and arithmeticRingAut_algebraMap records that it covers \sigma on the constants. arithmeticGalois F₀ packages this as a monoid homomorphism from L \simeq_{\mathbb{Q}} L into SemilinearAut L (L·F₀), the project's group of pairs (automorphism of the big field, automorphism of the constant field) commuting with the structure map: \sigma \mapsto (\mathrm{arithmeticRingAut}\,\sigma,\ \sigma). Accompanying lemmas identify its two components and the induced scalar action.

Pulling back along arithmeticGalois gives SMul and DistribMulAction instances of L\simeq_{\mathbb{Q}}L on Pic0 L (L·F₀), the group of degree-zero divisors (finitely supported \mathbb{Z}-combinations of the project's places of L\cdot F_0/L) modulo principal divisors.

Specialising to \overline{\mathbb{Q}} = AlgebraicClosure ℚ and F_0 = modularFunctionFieldFull N (the field generated over \mathbb{Q} by the q-expansions j(q^d) for d \mid N), the abbreviations modularFunctionFieldBar N and JZero N name the base-changed field and its degree-zero divisor class group; JZero.torsionGaloisRep N n is SemilinearAut.torsionRep composed with arithmeticGalois, a homomorphism from \overline{\mathbb{Q}} \simeq_{\mathbb{Q}} \overline{\mathbb{Q}} to the \mathbb{Z}/n-linear endomorphisms of the n-torsion of JZero N. Nothing about genus, dimension or finiteness is asserted; J_0(N) is here defined as this divisor class group, with no geometric modular curve intervening. N is an arbitrary natural number.

Relation to Mathlib

Mathlib supplies LaurentSeries, IntermediateField and AlgebraicClosure; the notions of place, degree-zero divisor class group Pic0, semilinear automorphism group SemilinearAut and modular function field used here are the project's own, as is the coefficientwise ring homomorphism coeffMap (a packaging of HahnSeries.map). Mathlib declares no action of L\simeq_{\mathbb{Q}}L on an intermediate field of L((q))/L or on its divisor class group.

Where it is used

The mod n representation JZero.torsionGaloisRep is the form in which the Galois action on torsion of the Jacobian of X_0(N) enters the argument: it is the source of the two-dimensional mod \ell representations attached to modular forms that are compared, via level lowering and Ribet's theorem, with the representation on \ell-torsion of a Frey curve.

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. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Publications of the Mathematical Society of Japan 11, Princeton University Press, 1971
  3. 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_ArithmeticGalois.lean

Imports

Imported by

Declarations

Source

import Definitions.Def_ModularCurve_X0
import Definitions.Def_ModularCurve_LaurentCoeff
import Definitions.Def_AlgebraicCurve_BaseChangeGalois
import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure ↗

set_option autoImplicit false

noncomputable section

open IntermediateField HahnSeries AlgebraicCurve

namespace ModularCurve

section ArithmeticGalois

variable {L : Type*} [Field L] [Algebra ℚ L]
variable (F₀ : IntermediateField ℚ (LaurentSeries ℚ))

def arithmeticRingAut (σ : L ≃ₐ[ℚ] L) :
    (laurentBaseChange L F₀) ≃+* (laurentBaseChange L F₀) where
  toFun x := ⟨coeffMap (σ : L →+* L) (x : LaurentSeries L),
    coeffMap_mem_laurentBaseChange σ x.2⟩
  invFun x := ⟨coeffMap (σ.symm : L →+* L) (x : LaurentSeries L),
    coeffMap_mem_laurentBaseChange σ.symm x.2⟩
  left_inv x := Subtype.ext <| by
    show coeffMap (σ.symm : L →+* L) (coeffMap (σ : L →+* L) (x : LaurentSeries L))
      = (x : LaurentSeries L)
    rw [coeffMap_coeffMap,
      coeffMap_congr (g := RingHom.id L) (RingHom.ext fun a => σ.symm_apply_apply a)
        (x : LaurentSeries L),
      coeffMap_id]
  right_inv x := Subtype.ext <| by
    show coeffMap (σ : L →+* L) (coeffMap (σ.symm : L →+* L) (x : LaurentSeries L))
      = (x : LaurentSeries L)
    rw [coeffMap_coeffMap,
      coeffMap_congr (g := RingHom.id L) (RingHom.ext fun a => σ.apply_symm_apply a)
        (x : LaurentSeries L),
      coeffMap_id]
  map_mul' x y :=
    Subtype.ext (map_mul (coeffMap (σ : L →+* L)) (x : LaurentSeries L) (y : LaurentSeries L))
  map_add' x y :=
    Subtype.ext (map_add (coeffMap (σ : L →+* L)) (x : LaurentSeries L) (y : LaurentSeries L))

@[simp]
theorem coe_arithmeticRingAut_apply (σ : L ≃ₐ[ℚ] L) (x : laurentBaseChange L F₀) :
    (arithmeticRingAut F₀ σ x : LaurentSeries L) = coeffMap (σ : L →+* L) (x : LaurentSeries L) :=
  rfl

theorem arithmeticRingAut_algebraMap (σ : L ≃ₐ[ℚ] L) (a : L) :
    arithmeticRingAut F₀ σ (algebraMap L (laurentBaseChange L F₀) a)
      = algebraMap L (laurentBaseChange L F₀) (σ a) :=
  Subtype.ext (coeffMap_algebraMap (σ : L →+* L) a)

def arithmeticGalois : (L ≃ₐ[ℚ] L) →* SemilinearAut L (laurentBaseChange L F₀) where
  toFun σ := ⟨(arithmeticRingAut F₀ σ, σ.toRingEquiv), fun a => arithmeticRingAut_algebraMap F₀ σ a⟩
  map_one' := by
    refine Subtype.ext (Prod.ext (RingEquiv.ext fun x => Subtype.ext ?_) rfl)
    show coeffMap ((1 : L ≃ₐ[ℚ] L) : L →+* L) (x : LaurentSeries L) = (x : LaurentSeries L)
    rw [show ((1 : L ≃ₐ[ℚ] L) : L →+* L) = RingHom.id L from RingHom.ext fun _ => rfl,
      coeffMap_id]
  map_mul' σ τ := by
    refine Subtype.ext (Prod.ext (RingEquiv.ext fun x => Subtype.ext ?_) rfl)
    show coeffMap ((σ * τ : L ≃ₐ[ℚ] L) : L →+* L) (x : LaurentSeries L)
      = coeffMap (σ : L →+* L) (coeffMap (τ : L →+* L) (x : LaurentSeries L))
    rw [coeffMap_coeffMap]
    exact coeffMap_congr (RingHom.ext fun _ => rfl) _

@[simp]
theorem toRingAut_arithmeticGalois (σ : L ≃ₐ[ℚ] L) :
    SemilinearAut.toRingAut (arithmeticGalois F₀ σ) = arithmeticRingAut F₀ σ :=
  rfl

@[simp]
theorem baseAut_arithmeticGalois (σ : L ≃ₐ[ℚ] L) :
    SemilinearAut.baseAut (arithmeticGalois F₀ σ) = σ.toRingEquiv :=
  rfl

theorem coe_arithmeticGalois_smul (σ : L ≃ₐ[ℚ] L) (x : laurentBaseChange L F₀) :
    ((arithmeticGalois F₀ σ • x : laurentBaseChange L F₀) : LaurentSeries L)
      = coeffMap (σ : L →+* L) (x : LaurentSeries L) :=
  rfl

end ArithmeticGalois

section PicAction

variable {L : Type*} [Field L] [Algebra ℚ L]
variable (F₀ : IntermediateField ℚ (LaurentSeries ℚ))

instance : SMul (L ≃ₐ[ℚ] L) (Pic0 L (laurentBaseChange L F₀)) where
  smul σ x := arithmeticGalois F₀ σ • x

theorem galois_smul_pic0_def (σ : L ≃ₐ[ℚ] L) (x : Pic0 L (laurentBaseChange L F₀)) :
    σ • x = arithmeticGalois F₀ σ • x :=
  rfl

instance : DistribMulAction (L ≃ₐ[ℚ] L) (Pic0 L (laurentBaseChange L F₀)) where
  one_smul x := by rw [galois_smul_pic0_def, map_one, one_smul]
  mul_smul σ τ x := by
    rw [galois_smul_pic0_def, galois_smul_pic0_def, galois_smul_pic0_def, map_mul, mul_smul]
  smul_zero σ := by rw [galois_smul_pic0_def, smul_zero]
  smul_add σ x y := by
    rw [galois_smul_pic0_def, galois_smul_pic0_def, galois_smul_pic0_def, smul_add]

end PicAction

section ModularInstance

variable (N : ℕ)

abbrev modularFunctionFieldBar : IntermediateField (AlgebraicClosure ℚ)
    (LaurentSeries (AlgebraicClosure ℚ)) :=
  laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)

abbrev JZero : Type _ :=
  Pic0 (AlgebraicClosure ℚ) (modularFunctionFieldBar N)

example : DistribMulAction (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) (JZero N) :=
  inferInstance

def JZero.torsionGaloisRep (n : ℕ) :
    (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) →*
      Module.End (ZMod n) (Pic0.torsion (AlgebraicClosure ℚ) (modularFunctionFieldBar N) n) :=
  (SemilinearAut.torsionRep _ _ n).comp (arithmeticGalois (modularFunctionFieldFull N))

@[simp]
theorem JZero.torsionGaloisRep_apply {n : ℕ} (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ)
    (x : Pic0.torsion (AlgebraicClosure ℚ) (modularFunctionFieldBar N) n) :
    JZero.torsionGaloisRep N n σ x = arithmeticGalois (modularFunctionFieldFull N) σ • x :=
  rfl

theorem JZero.coe_torsionGaloisRep_apply {n : ℕ} (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ)
    (x : Pic0.torsion (AlgebraicClosure ℚ) (modularFunctionFieldBar N) n) :
    ((JZero.torsionGaloisRep N n σ x : Pic0.torsion (AlgebraicClosure ℚ) (modularFunctionFieldBar N) n) :
        JZero N) = σ • (x : JZero N) :=
  rfl

end ModularInstance

end ModularCurve

Statements phrased using this module (922)

… and 772 more statements (search for the module name to find them).