Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_CoeffSemilinearAut.lean

definition module

Coefficientwise semilinear automorphisms of modular function fields

Fix a field K and N \ge 1. The modular function field of level N over K is the intermediate field F_N(K) = K(j(\mathsf q), j(\mathsf q)|_{\mathsf q \mapsto \mathsf q^N}) of K((\mathsf q)) obtained by adjoining the two Laurent series jqModC K = \mathsf q^{-1}\cdot(E_4^3\eta^{-24}), with coefficients the images of the integral j-expansion coefficients, and jqNModC K N, its image under the exponent-scaling ring homomorphism qExpand K N (\mathsf q \mapsto \mathsf q^N on Hahn-series supports). A ring homomorphism f of coefficient rings induces coeffMap f on Laurent series, acting on each coefficient; the first group of lemmas records that coeffMap f commutes with qExpand and carries jqModC and jqNModC of one ring to those of the other, the latter because the expansion coefficients come from \mathbb Z. From this, coeffMap_mem_modularFunctionFieldC shows that for any ring endomorphism \tau of K the map coeffMap\,\tau sends F_N(K) into itself, by induction over the presentation of F_N(K) as the subfield of K((\mathsf q)) generated by the constants together with the two distinguished series.

For a ring automorphism \tau of K, coeffRingAut N τ is the resulting ring automorphism of F_N(K), coefficientwise application of \tau, with inverse given by \tau^{-1}; it satisfies c(\tau)(a) = \tau(a) on constants. Packaging this, coeffSemilinearAut N τ is the pair (c(\tau), \tau) viewed as an element of SemilinearAut K (modularFunctionFieldC K N), the group of pairs (automorphism of the field, automorphism of the base) that are compatible via the structure map; the accompanying lemmas identify its two components, describe its action on elements through coeffMap, and state that it fixes the two generators j(\mathsf q) and j(\mathsf q^N). Finally, for K a perfect field of prime characteristic q, arithFrobC q K N is coeffSemilinearAut N applied to the Frobenius automorphism of K: the semilinear automorphism of F_N(K) raising coefficients to the q-th power, whose base component is a \mapsto a^q and which fixes j(\mathsf q) and j(\mathsf q^N).

Relation to Mathlib

SemilinearAut, coeffMap, qExpand and the modular function field modularFunctionFieldC are the project's own notions; Mathlib supplies the underlying Laurent/Hahn series and HahnSeries.map, intermediate fields and their description as subfield closures, and frobeniusEquiv for perfect fields of prime characteristic.

Where it is used

The semilinear automorphisms constructed here give the action of automorphisms of the constant field on the function field of X_0(N) in the formal \mathsf q-expansion model, and in particular the arithmetic Frobenius in characteristic q, which is what acts on the reduction of J_0(Nq) at q in the level-lowering part of the argument.

References

  1. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Publications of the Mathematical Society of Japan 11, Princeton University Press, 1971, §6

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

Imports

Imported by

Declarations

Source

import Definitions.Def_ModularCurve_JqCoeff
import Definitions.Def_ModularCurve_LaurentCoeff
import Definitions.Def_AlgebraicCurve_BaseChangeGalois
import Mathlib.FieldTheory.Perfect ↗

set_option autoImplicit false

noncomputable section

open AlgebraicCurve IntermediateField HahnSeries

namespace ModularCurve

namespace coeffSemilinearAut

section CoeffMapLemmas

variable {R S : Type*} [CommRing R] [CommRing S]

theorem coeffMap_qExpand (f : R →+* S) (n : ℕ) [NeZero n] (x : LaurentSeries R) :
    coeffMap f (qExpand R n x) = qExpand S n (coeffMap f x) := by
  ext k
  by_cases h : (n : ℤ) ∣ k
  · obtain ⟨m, rfl⟩ := h
    rw [coeffMap_coeff, qExpand_coeff_mul, qExpand_coeff_mul, coeffMap_coeff]
  · rw [coeffMap_coeff, qExpand_coeff_of_not_dvd _ _ h, qExpand_coeff_of_not_dvd _ _ h, map_zero]

theorem coeffMap_jqModC (f : R →+* S) : coeffMap f (jqModC R) = jqModC S :=
  map_jqModC f

theorem coeffMap_jqNModC (f : R →+* S) (N : ℕ) [NeZero N] :
    coeffMap f (jqNModC R N) = jqNModC S N := by
  rw [jqNModC, jqNModC, coeffMap_qExpand, coeffMap_jqModC]

end CoeffMapLemmas

end coeffSemilinearAut

section CoeffAut

variable {K : Type*} [Field K] (N : ℕ) [NeZero N]

theorem coeffSemilinearAut.coeffMap_mem_modularFunctionFieldC (τ : K →+* K) {x : LaurentSeries K}
    (hx : x ∈ modularFunctionFieldC K N) :
    coeffMap τ x ∈ modularFunctionFieldC K N := by
  change x ∈ Subfield.closure (Set.range (algebraMap K (LaurentSeries K)) ∪
      {jqModC K, jqNModC K N}) at hx
  induction hx using Subfield.closure_induction with
  | mem y hy =>
      rcases hy with ⟨a, rfl⟩ | hy
      · rw [coeffMap_algebraMap]
        exact (modularFunctionFieldC K N).algebraMap_mem _
      · rcases hy with rfl | hy
        · rw [coeffSemilinearAut.coeffMap_jqModC]
          exact jqModC_mem K N
        · rw [Set.mem_singleton_iff] at hy
          subst hy
          rw [coeffSemilinearAut.coeffMap_jqNModC]
          exact jqNModC_mem K N
  | one => simp
  | add x y _ _ hx hy => simpa using add_mem hx hy
  | neg x _ hx => simpa using neg_mem hx
  | inv x _ hx => simpa using inv_mem hx
  | mul x y _ _ hx hy => simpa using mul_mem hx hy

def coeffRingAut (τ : K ≃+* K) : modularFunctionFieldC K N ≃+* modularFunctionFieldC K N where
  toFun x := ⟨coeffMap (τ : K →+* K) (x : LaurentSeries K),
    coeffSemilinearAut.coeffMap_mem_modularFunctionFieldC N (τ : K →+* K) x.2⟩
  invFun x := ⟨coeffMap (τ.symm : K →+* K) (x : LaurentSeries K),
    coeffSemilinearAut.coeffMap_mem_modularFunctionFieldC N (τ.symm : K →+* K) x.2⟩
  left_inv x := Subtype.ext <| by
    show coeffMap (τ.symm : K →+* K) (coeffMap (τ : K →+* K) (x : LaurentSeries K))
      = (x : LaurentSeries K)
    rw [coeffMap_coeffMap,
      coeffMap_congr (g := RingHom.id K) (RingHom.ext fun a => τ.symm_apply_apply a) _, coeffMap_id]
  right_inv x := Subtype.ext <| by
    show coeffMap (τ : K →+* K) (coeffMap (τ.symm : K →+* K) (x : LaurentSeries K))
      = (x : LaurentSeries K)
    rw [coeffMap_coeffMap,
      coeffMap_congr (g := RingHom.id K) (RingHom.ext fun a => τ.apply_symm_apply a) _, coeffMap_id]
  map_mul' x y :=
    Subtype.ext (map_mul (coeffMap (τ : K →+* K)) (x : LaurentSeries K) (y : LaurentSeries K))
  map_add' x y :=
    Subtype.ext (map_add (coeffMap (τ : K →+* K)) (x : LaurentSeries K) (y : LaurentSeries K))

@[simp]
theorem coe_coeffRingAut_apply (τ : K ≃+* K) (x : modularFunctionFieldC K N) :
    (coeffRingAut N τ x : LaurentSeries K) = coeffMap (τ : K →+* K) (x : LaurentSeries K) :=
  rfl

theorem coeffRingAut_algebraMap (τ : K ≃+* K) (a : K) :
    coeffRingAut N τ (algebraMap K (modularFunctionFieldC K N) a)
      = algebraMap K (modularFunctionFieldC K N) (τ a) :=
  Subtype.ext (coeffMap_algebraMap (τ : K →+* K) a)

def coeffSemilinearAut (τ : K ≃+* K) : SemilinearAut K (modularFunctionFieldC K N) :=
  ⟨(coeffRingAut N τ, τ), fun a => coeffRingAut_algebraMap N τ a⟩

@[simp]
theorem toRingAut_coeffSemilinearAut (τ : K ≃+* K) :
    SemilinearAut.toRingAut (coeffSemilinearAut N τ) = coeffRingAut N τ := rfl

@[simp]
theorem baseAut_coeffSemilinearAut (τ : K ≃+* K) :
    SemilinearAut.baseAut (coeffSemilinearAut N τ) = τ := rfl

theorem coe_coeffSemilinearAut_smul (τ : K ≃+* K) (x : modularFunctionFieldC K N) :
    ((coeffSemilinearAut N τ • x : modularFunctionFieldC K N) : LaurentSeries K)
      = coeffMap (τ : K →+* K) (x : LaurentSeries K) := rfl

theorem coeffSemilinearAut_smul_jq (τ : K ≃+* K) :
    coeffSemilinearAut N τ • (⟨jqModC K, jqModC_mem K N⟩ : modularFunctionFieldC K N)
      = ⟨jqModC K, jqModC_mem K N⟩ :=
  Subtype.ext (coeffSemilinearAut.coeffMap_jqModC (τ : K →+* K))

theorem coeffSemilinearAut_smul_jqN (τ : K ≃+* K) :
    coeffSemilinearAut N τ • (⟨jqNModC K N, jqNModC_mem K N⟩ : modularFunctionFieldC K N)
      = ⟨jqNModC K N, jqNModC_mem K N⟩ :=
  Subtype.ext (coeffSemilinearAut.coeffMap_jqNModC (τ : K →+* K) N)

end CoeffAut

section Frobenius

variable (q : ℕ) (K : Type*) [Field K] [Fact q.Prime] [CharP K q] [PerfectField K]
  (N : ℕ) [NeZero N]

def arithFrobC : SemilinearAut K (modularFunctionFieldC K N) :=
  coeffSemilinearAut N (frobeniusEquiv K q)

@[simp]
theorem baseAut_arithFrobC_apply (a : K) :
    SemilinearAut.baseAut (arithFrobC q K N) a = a ^ q :=
  rfl

theorem arithFrobC_smul_jq :
    arithFrobC q K N • (⟨jqModC K, jqModC_mem K N⟩ : modularFunctionFieldC K N)
      = ⟨jqModC K, jqModC_mem K N⟩ :=
  coeffSemilinearAut_smul_jq N _

theorem arithFrobC_smul_jqN :
    arithFrobC q K N • (⟨jqNModC K N, jqNModC_mem K N⟩ : modularFunctionFieldC K N)
      = ⟨jqNModC K N, jqNModC_mem K N⟩ :=
  coeffSemilinearAut_smul_jqN N _

end Frobenius

end ModularCurve

end

Statements phrased using this module (182)

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