Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_FullLevelSemistableCoveringW2.lean

definition module

Clauses for a semistable covering: Drinfeld, Igusa, inertia, width

Throughout, q is a prime, M' a level, A a valuation subring of \overline{\mathbb{Q}}, and W a finite set of places of modularFunctionFieldC (ResidueField A) M'; \mathcal{C} is a SemistableCovering q M' A W of the big field fieldBar q M', i.e. component charts CIg ℓ indexed by \ell\in\mathbb{P}^1(\mathbb{F}_q) with reduced fields FIg ℓ, charts CSS s indexed by s\in W with reduced fields FSS s, and two families of annuli An, An' attached to them. InducesOnChart C g φ asserts, for a semilinear automorphism g of the big field and a ring automorphism \varphi of the reduced field, that f\in C.\mathrm{integers}\iff g\cdot f\in C.\mathrm{integers} and that C.\mathrm{residue}(g\cdot f)=\varphi(C.\mathrm{residue}\,f) for integral f (formulated as a dependent existential over the stability proof, so amounting to their conjunction). DrinfeldCurve.quotField q κ C, for a subgroup C\le\mu_{q+1}(\mathbb{F}_{q^2}), is the intermediate field of \kappa\subseteq\operatorname{Frac}(\mathrm{CoordRing}\,q\,\kappa) fixed by the group generated by the automorphisms hFunctionFieldAction q κ ⟨(1, ζ), _⟩ for \zeta\in C.

The remaining declarations are predicates on \mathcal{C}. DrinfeldClause π ι η ζ s asserts the existence of C\le\mu_{q+1}(\mathbb{F}_{q^2}) and of a \mathrm{ResidueField}\,A-algebra isomorphism e from FSS s onto that fixed field such that: (i) every \gamma\in\Gamma_0(M') has levelAutBar q M' ζ γ⁻¹ inducing some \varphi on CSS s, and each induced \varphi becomes, through e, the action of the pair (\mathrm{redQ}\,q\,\gamma,1); (ii) every \tau in the inertia subgroup of A over \mathbb{Q} with A.\mathrm{tameCharacter}\,\pi\,\tau=\iota(\alpha), \alpha\in\mathbb{F}_{q^2}^\times, has the coefficientwise arithmetic Galois automorphism inducing some \varphi, and each such \varphi becomes, through e, the action of (\mathrm{diagOneElem}\,q\,(d^{\eta})^{-1},\alpha^{\eta}) for any d\in(\mathbb{Z}/q)^\times whose image is \alpha^{q+1}. In both cases the prescribed action is required only under a hypothesis that the relevant pair lies in hSubgroup q, quantified over its proof. IgusaUnipotentClause ζ requires levelAutBar q M' ζ γ⁻¹ to induce the identity on the chart CIg (lineInfty q) whenever \mathrm{redQ}\,q\,\gamma is of unipotent type. LevelPinClauses hle R₀ compares the covering with a constant reduction R_0 of the base-changed level-M' field: a level-M' function f integral for R_0, regular wherever j is, and with R_0-residue in the valuation subring of s, is integral on CSS s with residue the constant given by evaluating that residue at s; and for each \ell there is a ring homomorphism j from the reduced level-M' field to FIg ℓ computing the residues of level-M' functions on CIg ℓ and pulling the valuation subring of 𝒞.xs ℓ s back to that of s. InertiaClause π requires every \tau in the inertia subgroup with trivial tame character to induce the identity on all charts, to preserve their domains and placeMap, to preserve the annulus domains, and to fix the parameters of An and An'. WidthClause π requires each (𝒞.An ℓ s).modulus to be u\pi^{w} with u\in A^\times and w\ge1. W2Clauses π ι η is the conjunction of all Drinfeld clauses and all Igusa unipotent clauses.

Relation to Mathlib

Component charts, annuli, semistable coverings, the Drinfeld coordinate ring and its function field, hSubgroup and SemilinearAut are the project's own notions; Mathlib supplies the ambient machinery used in their formulation (ValuationSubring and its inertia subgroup, IsLocalRing.ResidueField, IntermediateField.fixedField, FractionRing, rootsOfUnity, GaloisField, Projectivization).

Where it is used

These predicates constitute the specification of the semistable covering of the full-level modular function field at q whose existence is asserted elsewhere: the reduced components over supersingular points are fixed fields inside a Drinfeld function field carrying prescribed \Gamma_0(M')- and inertia-actions, the level-M' functions pin the charts to the reduced level-M' curve, and the annuli have positive width. They are the input to the computation of the reduction at q of the Jacobian and of the action of inertia at q on its torsion, as used in the level-lowering step.

References

  1. N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, Annals of Mathematics Studies 108, Princeton University Press, 1985, §13
  2. 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
  3. I. I. Bouw and S. Wewers, Stable reduction of modular curves, in: Modular Curves and Abelian Varieties, Progress in Mathematics 224, Birkhäuser, 2004, 1–22

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

Imports

Imported by

Declarations

Source

import Definitions.Def_ModularCurve_FullLevelSemistableCovering
import Definitions.Def_AlgebraicCurve_SemistableChartsComap
import Definitions.Def_AlgebraicCurve_ConstantReduction
import Definitions.Def_DrinfeldCurve_FunctionField
import Definitions.Def_GaloisRep_TameCharacter
import Definitions.Def_FLTPrelim_Ramification
import Definitions.Def_ModularCurve_ArithmeticGalois

set_option autoImplicit false

noncomputable section

namespace ModularCurve.FullLevel.SemistableCovering

open AlgebraicCurve IsLocalRing DrinfeldCurve CongruenceSubgroup
open scoped MatrixGroups

attribute [local instance] ModularCurve.instDecidableEqResidueFieldSemistable
  ModularCurve.instAlgebraResidueFieldModularFunctionFieldCSemistable

variable {q : ℕ} [Fact q.Prime] {M' : ℕ} [NeZero M'] {A : ValuationSubring (AlgebraicClosure ℚ)}
  {W : Finset (Place (ResidueField A) (modularFunctionFieldC (ResidueField A) M'))}

def InducesOnChart {Fbar : Type} [Field Fbar] [Algebra (ResidueField A) Fbar]
    (C : ComponentChart A (fieldBar q M') Fbar) (g : SemilinearAut (AlgebraicClosure ℚ) (fieldBar q M'))
    (φ : Fbar ≃+* Fbar) : Prop :=
  ∃ hst : ∀ f : fieldBar q M', f ∈ C.integers ↔ g • f ∈ C.integers,
    ∀ (f : fieldBar q M') (hf : f ∈ C.integers), C.residue ⟨g • f, (hst f).mp hf⟩ = φ (C.residue ⟨f, hf⟩)

variable (𝒞 : SemistableCovering q M' A W)

abbrev _root_.DrinfeldCurve.quotField (q : ℕ) [Fact q.Prime] (κ : Type) [Field κ] [Algebra (GaloisField q 2) κ]
    [IsDomain (CoordRing q κ)] (C : Subgroup (rootsOfUnity (q + 1) (GaloisField q 2))) :
    IntermediateField κ (drinfeldFunctionField q κ) :=
  IntermediateField.fixedField (Subgroup.closure (Set.range fun ζ : ↥C =>
    hFunctionFieldAction q κ ⟨(1, ((ζ : rootsOfUnity (q + 1) (GaloisField q 2)) : (GaloisField q 2)ˣ)),
      one_mem_hSubgroup_of_mem q ζ⟩))

def DrinfeldClause [Algebra (GaloisField q 2) (ResidueField A)] [IsDomain (CoordRing q (ResidueField A))]
    (π : AlgebraicClosure ℚ) (ι : GaloisField q 2 →+* ResidueField A)
    (η : ℕ) (ζ : Idx q) (s : ↥W) : Prop :=
  ∃ (C : Subgroup (rootsOfUnity (q + 1) (GaloisField q 2)))
    (e : 𝒞.FSS s ≃ₐ[ResidueField A] ↥(DrinfeldCurve.quotField q (ResidueField A) C)),

    (∀ (γ : SL(2, ℤ)), γ ∈ Gamma0 M' →
      (∃ φ : 𝒞.FSS s ≃+* 𝒞.FSS s, InducesOnChart (𝒞.CSS s) (SemilinearAut.ofAlgAut (levelAutBar q M' ζ γ⁻¹)) φ) ∧
      ∀ φ : 𝒞.FSS s ≃+* 𝒞.FSS s,
        InducesOnChart (𝒞.CSS s) (SemilinearAut.ofAlgAut (levelAutBar q M' ζ γ⁻¹)) φ →
        ∀ hmem : (redQ q γ, (1 : (GaloisField q 2)ˣ)) ∈ hSubgroup q,
          ∀ x : 𝒞.FSS s, ((e (φ x) : ↥(DrinfeldCurve.quotField q (ResidueField A) C)) : drinfeldFunctionField q (ResidueField A)) =
            hFunctionFieldAction q (ResidueField A) ⟨_, hmem⟩
              ((e x : ↥(DrinfeldCurve.quotField q (ResidueField A) C)) : drinfeldFunctionField q (ResidueField A))) ∧

    (∀ τ ∈ A.inertiaSubgroupIn ℚ, ∀ α : (GaloisField q 2)ˣ, ι (α : GaloisField q 2) = A.tameCharacter π τ →
      (∃ φ : 𝒞.FSS s ≃+* 𝒞.FSS s, InducesOnChart (𝒞.CSS s)
          (ModularCurve.arithmeticGalois (xHFunctionField (q ^ 2 * M') (levelH q M')) τ) φ) ∧
      ∀ φ : 𝒞.FSS s ≃+* 𝒞.FSS s,
        InducesOnChart (𝒞.CSS s)
          (ModularCurve.arithmeticGalois (xHFunctionField (q ^ 2 * M') (levelH q M')) τ) φ →
        ∀ (d : (ZMod q)ˣ), algebraMap (ZMod q) (GaloisField q 2) (d : ZMod q) = (α : GaloisField q 2) ^ (q + 1) →
          ∀ hmem : (diagOneElem q (d ^ η)⁻¹, α ^ η) ∈ hSubgroup q,
            ∀ x : 𝒞.FSS s, ((e (φ x) : ↥(DrinfeldCurve.quotField q (ResidueField A) C)) : drinfeldFunctionField q (ResidueField A)) =
              hFunctionFieldAction q (ResidueField A) ⟨_, hmem⟩
                ((e x : ↥(DrinfeldCurve.quotField q (ResidueField A) C)) : drinfeldFunctionField q (ResidueField A)))

def IgusaUnipotentClause (ζ : Idx q) : Prop :=
  ∀ (γ : SL(2, ℤ)), γ ∈ Gamma0 M' → (∃ t : ZMod q, redQ q γ = CuspidalType.unipotent q t) →
    InducesOnChart (𝒞.CIg (lineInfty q)) (SemilinearAut.ofAlgAut (levelAutBar q M' ζ γ⁻¹)) (RingEquiv.refl _)

def LevelPinClauses (hle : modularFunctionFieldBar M' ≤ fieldBar q M')
    (R₀ : ConstantReduction A ↥(modularFunctionFieldBar M') (modularFunctionFieldC (ResidueField A) M')) : Prop :=

  (∀ (s : ↥W) (f : ↥(modularFunctionFieldBar M')) (hf : f ∈ R₀.integers),
    (∀ P : Place (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar M'),
      0 ≤ P.ord ((⟨coeffEmb (AlgebraicClosure ℚ) jq,
        coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionField_le_full M' (jq_mem M'))⟩ :
        ↥(modularFunctionFieldBar M')) : ↥(modularFunctionFieldBar M')) → 0 ≤ P.ord (f : ↥(modularFunctionFieldBar M'))) →
    (R₀.residue ⟨f, hf⟩ : modularFunctionFieldC (ResidueField A) M') ∈
        (s : Place (ResidueField A) (modularFunctionFieldC (ResidueField A) M')).toValuationSubring →
      ∃ hC : (IntermediateField.inclusion hle f : fieldBar q M') ∈ (𝒞.CSS s).integers,
        (𝒞.CSS s).residue ⟨_, hC⟩ = algebraMap (ResidueField A) (𝒞.FSS s)
          ((s : Place (ResidueField A) (modularFunctionFieldC (ResidueField A) M')).evalAt (R₀.residue ⟨f, hf⟩))) ∧
  (∀ ℓ : CuspidalType.ProjLine q,
    ∃ j : modularFunctionFieldC (ResidueField A) M' →+* 𝒞.FIg ℓ,
      (∀ (f : ↥(modularFunctionFieldBar M')) (hf : f ∈ R₀.integers),
        ∃ hC : (IntermediateField.inclusion hle f : fieldBar q M') ∈ (𝒞.CIg ℓ).integers,
          (𝒞.CIg ℓ).residue ⟨_, hC⟩ = j (R₀.residue ⟨f, hf⟩)) ∧
      ∀ (s : ↥W) (g : modularFunctionFieldC (ResidueField A) M'),
        g ∈ (s : Place (ResidueField A) (modularFunctionFieldC (ResidueField A) M')).toValuationSubring ↔
          j g ∈ (𝒞.xs ℓ s).toValuationSubring)

def InertiaClause (π : AlgebraicClosure ℚ) : Prop :=
  ∀ τ ∈ A.inertiaSubgroupIn ℚ, A.tameCharacter π τ = 1 →
    let g := ModularCurve.arithmeticGalois (xHFunctionField (q ^ 2 * M') (levelH q M')) τ
    (∀ ℓ, InducesOnChart (𝒞.CIg ℓ) g (RingEquiv.refl _) ∧
      (∀ P, (𝒞.CIg ℓ).placeMap (g • P) = (𝒞.CIg ℓ).placeMap P) ∧ (∀ P, P ∈ (𝒞.CIg ℓ).dom ↔ g • P ∈ (𝒞.CIg ℓ).dom)) ∧
    (∀ s, InducesOnChart (𝒞.CSS s) g (RingEquiv.refl _) ∧
      (∀ P, (𝒞.CSS s).placeMap (g • P) = (𝒞.CSS s).placeMap P) ∧ (∀ P, P ∈ (𝒞.CSS s).dom ↔ g • P ∈ (𝒞.CSS s).dom)) ∧
    (∀ ℓ s, (∀ P, P ∈ (𝒞.An ℓ s).dom ↔ g • P ∈ (𝒞.An ℓ s).dom) ∧
      g • (𝒞.An ℓ s).param = (𝒞.An ℓ s).param ∧ g • (𝒞.An' ℓ s).param = (𝒞.An' ℓ s).param)

def WidthClause (π : A) : Prop :=
  ∀ ℓ s, ∃ w : ℕ, 1 ≤ w ∧ ∃ u : Aˣ, (𝒞.An ℓ s).modulus = u * π ^ w

def W2Clauses [Algebra (GaloisField q 2) (ResidueField A)] [IsDomain (CoordRing q (ResidueField A))]
    (π : AlgebraicClosure ℚ) (ι : GaloisField q 2 →+* ResidueField A) (η : ℕ) : Prop :=
  (∀ (ζ : Idx q) (s : ↥W), 𝒞.DrinfeldClause π ι η ζ s) ∧ ∀ ζ : Idx q, 𝒞.IgusaUnipotentClause ζ

end ModularCurve.FullLevel.SemistableCovering

end

Statements phrased using this module (368)

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