Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_JqCoeff.lean

definition module

The -expansion over any commutative ring, and

Two pieces of coefficient bookkeeping for the formal q-expansion of the modular j-invariant, carried out inside Laurent series rather than on any curve.

First, for any commutative ring K, ModularCurve.jqModC K : LaurentSeries K is defined as HahnSeries.single (-1) 1 * HahnSeries.ofPowerSeries ℤ K (jNum.map (Int.castRingHom K)): the integral power series jNum of the imported module has its coefficients pushed along the unique ring map \mathbb{Z} \to K and the result is shifted by q^{-1}, so that one obtains q^{-1} + 744 + 196884\,q + \cdots read in K. By construction this is definitionally the project's rational series jq when K = \mathbb{Q} (jqModC_rat, proved by rfl), and it commutes with arbitrary change of coefficients: map_jqModC states (jqModC K).map f = jqModC K' for every ring homomorphism f : K \to K', whence jqModC_eq_map_intCast : jqModC K = (jqModC ℤ).map (Int.castRingHom K). For N with NeZero N, jqNModC K N := qExpand K N (jqModC K) is the substitution q \mapsto q^N applied to this series, i.e. j(q^N), with jqNModC_one recording N = 1.

Second, for a field K and N \geq 1, ModularCurve.modularFunctionFieldC K N is the intermediate field IntermediateField.adjoin K {jqModC K, jqNModC K N} of K((q)), that is K(j(q), j(q^N)) generated by the two displayed Laurent series; jqModC_mem and jqNModC_mem record that the two generators lie in it, modularFunctionFieldC_one that for N = 1 it is the single-generator field, and modularFunctionFieldC_rat that over \mathbb{Q} it is definitionally the two-generator field modularFunctionField N of the imported module (not the full modular function field). No property of these series — order of the pole, non-vanishing, transcendence, Frobenius identities in characteristic \ell — is asserted here; the module is purely definitional.

Relation to Mathlib

Built on Mathlib's LaurentSeries/HahnSeries and IntermediateField.adjoin; Mathlib has no q-expansion of j with coefficients in an arbitrary commutative ring, so jqModC and the field it generates are the project's own, defined by transporting the project's integral series jNum along \mathbb{Z} \to K.

Where it is used

These series provide the single definition of 'the j-expansion with coefficients in K' used throughout the project, allowing the characteristic-zero and characteristic-\ell situations (e.g. K = \mathbb{Z}, K = \mathbb{Q}, K = \mathbb{Z}/\ell) to be compared through a common formula, and the fields K(j(q),j(q^N)) serve as the function-field model of the modular curve X_0(N) used in the algebraic construction of modular curves and their Jacobians.

References

  1. F. Diamond and J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005
  2. J.-P. Serre, A Course in Arithmetic, Graduate Texts in Mathematics 7, Springer, 1973

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

Imports

Imported by

Declarations

Source

import Definitions.Def_ModularCurve_X0

set_option autoImplicit false

noncomputable section

open HahnSeries

namespace ModularCurve

section JExpansion

variable (K : Type*) [CommRing K]

def jqModC : LaurentSeries K :=
  HahnSeries.single (-1 : ℤ) 1 * HahnSeries.ofPowerSeries ℤ K (jNum.map (Int.castRingHom K))

def jqNModC (N : ℕ) [NeZero N] : LaurentSeries K := qExpand K N (jqModC K)

@[simp]
theorem jqNModC_one : jqNModC K 1 = jqModC K := qExpand_one_apply _

theorem jqModC_rat : jqModC ℚ = jq := rfl

variable {K} in

theorem map_jqModC {K' : Type*} [CommRing K'] (f : K →+* K') :
    (jqModC K).map f = jqModC K' := by
  have hmul : ∀ x y : LaurentSeries K, (x * y).map f = x.map f * y.map f :=
    fun x y => HahnSeries.map_mul f.toNonUnitalRingHom
  have hsingle : (HahnSeries.single (-1 : ℤ) (1 : K)).map f = HahnSeries.single (-1 : ℤ) 1 := by
    ext g
    rw [HahnSeries.map_coeff, HahnSeries.coeff_single, HahnSeries.coeff_single, apply_ite f,
      map_one, map_zero]
  have hseries : ∀ u : PowerSeries K,
      (HahnSeries.ofPowerSeries ℤ K u).map f = HahnSeries.ofPowerSeries ℤ K' (u.map f) := by
    intro u
    ext k
    rw [HahnSeries.map_coeff]
    rcases le_or_gt 0 k with hk | hk
    · lift k to ℕ using hk
      rw [HahnSeries.ofPowerSeries_apply_coeff, HahnSeries.ofPowerSeries_apply_coeff,
        PowerSeries.coeff_map]
    · rw [ofPowerSeries_coeff_of_neg _ hk, ofPowerSeries_coeff_of_neg _ hk, map_zero]
  rw [jqModC, jqModC, hmul, hsingle, hseries,
    show (jNum.map (Int.castRingHom K)).map f = jNum.map (Int.castRingHom K') from by
      rw [show PowerSeries.map f (PowerSeries.map (Int.castRingHom K) jNum)
            = PowerSeries.map (f.comp (Int.castRingHom K)) jNum from
          (congrFun (congrArg DFunLike.coe (PowerSeries.map_comp (Int.castRingHom K) f)) jNum).symm,
        RingHom.ext_int (f.comp (Int.castRingHom K)) (Int.castRingHom K')]]

theorem jqModC_eq_map_intCast : jqModC K = (jqModC ℤ).map (Int.castRingHom K) :=
  (map_jqModC (Int.castRingHom K)).symm

end JExpansion

section FunctionField

variable (K : Type*) [Field K]

def modularFunctionFieldC (N : ℕ) [NeZero N] :
    IntermediateField K (LaurentSeries K) :=
  IntermediateField.adjoin K {jqModC K, jqNModC K N}

theorem jqModC_mem (N : ℕ) [NeZero N] : jqModC K ∈ modularFunctionFieldC K N :=
  IntermediateField.subset_adjoin _ _ (Set.mem_insert _ _)

theorem jqNModC_mem (N : ℕ) [NeZero N] : jqNModC K N ∈ modularFunctionFieldC K N :=
  IntermediateField.subset_adjoin _ _ (Set.mem_insert_of_mem _ rfl)

theorem modularFunctionFieldC_rat (N : ℕ) [NeZero N] :
    modularFunctionFieldC ℚ N = modularFunctionField N := rfl

theorem modularFunctionFieldC_one :
    modularFunctionFieldC K 1 = IntermediateField.adjoin K {jqModC K} := by
  unfold modularFunctionFieldC
  rw [jqNModC_one, Set.pair_eq_singleton]

end FunctionField

end ModularCurve

end

Statements phrased using this module (901)

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