Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_JHCuspChartSet.lean

definition module

Pole-chart integral elements and infinity-side cusp chart sets

Throughout, a prime p, a modulus M with p \mid M and a subgroup H \le (\mathbb{Z}/M)^{\times} are fixed; the two fields involved are F_{M} = xHFunctionFieldBar M H and F_{M/p} = xHFunctionFieldBar (M / p) (ModularCurve.infSubgroup p M H hpM), each an algebra over \overline{\mathbb{Q}} = AlgebraicClosure ℚ, the second being taken at the level obtained from M/p and the subgroup infSubgroup p M H hpM attached to H. Two subsets are defined, and nothing is asserted about them here.

Given a valuation subring A \subseteq \overline{\mathbb{Q}} and an element x' \in F_{M/p}, integralOverPoleChart A x' views F_{M/p} as an A-algebra through the inclusion A \hookrightarrow \overline{\mathbb{Q}} followed by the structure map \overline{\mathbb{Q}} \to F_{M/p}, forms the A-subalgebra A[x'^{-1}] = Algebra.adjoin A {x'⁻¹} generated by the inverse of x', and returns the set of elements s \in F_{M/p} that are integral over that subalgebra, i.e. satisfy a monic polynomial with coefficients in A[x'^{-1}]. This is the integral closure of A[1/x'] in F_{M/p}, delivered as a bare subset rather than as a subalgebra; for x' = 0 the adjoined element is 0 and the subalgebra is the image of A.

Given in addition a \overline{\mathbb{Q}}-algebra homomorphism \alpha \colon F_{M/p} \to F_M and an element t \in F_M, cuspChartSetInf A α x' t is the subset of F_M \alpha\bigl(\text{integralOverPoleChart}(A, x')\bigr) \cup \{\, t - a \;:\; a \in A \,\}, where a is transported into F_M along \overline{\mathbb{Q}} \to F_M. No relation between \alpha, x' and t is imposed, and \alpha is not required to be integral; in the intended application \alpha is a degeneracy map, x' is the j-invariant at level M/p, and t is a function whose q-expansion is the ratio j(q^{p})/j(q)^{p}, so that the A-translates t - a serve to separate the places on the other component. Both sets are independent of any choice of place or model.

Relation to Mathlib

The definitions are phrased with Mathlib's ValuationSubring, Algebra.adjoin and IsIntegral, applied to the A-algebra structure induced on the function fields by A \subseteq \overline{\mathbb{Q}}; the chart sets themselves are project notions with no Mathlib counterpart.

Where it is used

These sets provide the generating data for affine charts at the cuspidal places lying on the \infty-component, in the study of the reduction at p of the modular curve of level H and of the induced specialisation of J_H. That specialisation, with its glued Picard description of the special fibre, is what feeds the level-lowering step of the Frey–Serre–Ribet argument.

References

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

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_JHNeronObjectAtP
import Definitions.Def_ModularCurve_JHPlaceSpecialization

set_option autoImplicit false

open AlgebraicCurve IsLocalRing ModularCurve
open scoped MatrixGroups

namespace ModularCurve.JHPlaceSpecialization

variable {p M : ℕ} [Fact p.Prime] [NeZero M] {H : Subgroup (ZMod M)ˣ} {hpM : p ∣ M}

def integralOverPoleChart (A : ValuationSubring (AlgebraicClosure ℚ))
    (x' : ↥(xHFunctionFieldBar (M / p) (ModularCurve.infSubgroup p M H hpM))) :
    Set ↥(xHFunctionFieldBar (M / p) (ModularCurve.infSubgroup p M H hpM)) :=
  letI : Algebra ↥A ↥(xHFunctionFieldBar (M / p) (ModularCurve.infSubgroup p M H hpM)) :=
    ((algebraMap (AlgebraicClosure ℚ) ↥(xHFunctionFieldBar (M / p) (ModularCurve.infSubgroup p M H hpM))).comp A.subtype).toAlgebra
  {s | IsIntegral ↥(Algebra.adjoin ↥A ({x'⁻¹} : Set ↥(xHFunctionFieldBar (M / p) (ModularCurve.infSubgroup p M H hpM)))) s}

def cuspChartSetInf (A : ValuationSubring (AlgebraicClosure ℚ))
    (α : ↥(xHFunctionFieldBar (M / p) (ModularCurve.infSubgroup p M H hpM)) →ₐ[AlgebraicClosure ℚ] ↥(xHFunctionFieldBar M H))
    (x' : ↥(xHFunctionFieldBar (M / p) (ModularCurve.infSubgroup p M H hpM))) (t : ↥(xHFunctionFieldBar M H)) :
    Set ↥(xHFunctionFieldBar M H) :=
  (α '' integralOverPoleChart (p := p) A x') ∪
    Set.range (fun a : ↥A => t - algebraMap (AlgebraicClosure ℚ) ↥(xHFunctionFieldBar M H) (a : AlgebraicClosure ℚ))

end ModularCurve.JHPlaceSpecialization

Statements phrased using this module (6)