Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_WeierstrassCurve_DrinfeldBasisGlobal.lean

definition module

Drinfeld bases on projective Weierstrass models; level component

Fix a commutative ring T and a Weierstrass curve W in projective coordinates over T. Write \mathrm{base} for \operatorname{Spec} T and let a section be a morphism into the projective model \mathrm{Proj}-scheme projModelCR W splitting its structure morphism projModelStrCR W. Given a relative group law G on that structure morphism (the project's notion: functorial group structures on T'-valued sections, with associativity, unit, inverse and base-change naturality as fields), linComb G P Q a b is aP + bQ formed with the iterated group law, and basisTuple G q P Q is the family of q^2 morphisms i \mapsto (i / q)P + (i \bmod q)Q indexed by Fin (q * q); basisTuple_over records that each is a section. basisDivisor is the product, inside the ideal-sheaf lattice of the pullback of projModelStrCR W along the identity of the base, of the kernel ideal sheaves of the graphs of these q^2 sections β€” the effective divisor \sum_{a,b \bmod q} [aP+bQ]. torsionIdeal is the kernel ideal sheaf of the morphism from the q-torsion scheme \ker([q]) (the pullback of the multiplication-by-q morphism against the unit section) into that same pullback. IsDrinfeldBasis G q P Q is the equality of these two ideal sheaves: the Drinfeld condition that the divisor of the q^2 linear combinations is exactly W[q].

A GroupLawFamily A assigns such a group law to every A-algebra T and every projective Weierstrass curve over it; IsChordTangent asks that for each of these there exist a bijection between F-valued sections and affine points of the base-changed curve, for all fields F over the base ring, satisfying IsPointsEval, i.e. additive and Galois-equivariant. A RawDrinfeldPair T is a projective Weierstrass curve together with two sections, and IsDrinfeldLevel 𝒒 q W x says that the recorded curve is W and that its two sections form a Drinfeld q-basis. A DrinfeldTransport packages base change along A-algebra maps and the action of Weierstrass variable changes on raw pairs, with the functoriality identities and the two statements that IsDrinfeldLevel is preserved under base change (replacing W by W.\mathrm{map}\,f) and under variable change (replacing W by C \bullet W) as fields. From such data, drinfeldComponent produces a ModularCurve.LevelComponent A, and fullLevelRigidData combines it, via ModularCurve.weierstrassLevelRigidData, with the cyclic-N-kernel and level-\ell components to give rigid Weierstrass moduli data for curves with unit discriminant carrying all three level structures.

Relation to Mathlib

Mathlib has no relative group law on a projective Weierstrass model and no Drinfeld level structures; both are the project's own, built on Mathlib's WeierstrassCurve.Projective, the Proj construction and Scheme.IdealSheafData.

Where it is used

This supplies the full level-q (Drinfeld basis) component of the project's moduli description of Weierstrass curves with level structure, alongside the \Gamma_0(N) cyclic-kernel and level-\ell point components, and feeds into the rigid Weierstrass data from which the relevant modular curves and their q-expansion theory are obtained.

References

  1. N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, Annals of Mathematics Studies 108, Princeton University Press, 1985
  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. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_WeierstrassCurve_ProjModel
import Definitions.Def_AlgebraicGeometry_RelEffCartierDivSum
import Definitions.Def_ModularCurve_WeierstrassLevelComponents

set_option autoImplicit false

universe u

noncomputable section

open AlgebraicGeometry CategoryTheory CategoryTheory.Limits NeronModelInfra WeierstrassProjModel

namespace WeierstrassCurve.DrinfeldGlobal

variable {T : Type u} [CommRing T] (W : WeierstrassCurve.Projective T)

abbrev base : Scheme.{u} := Spec (CommRingCat.of T)

abbrev Section : Type u := SchemeHomOver (πŸ™ (base (T := T))) (projModelStrCR W)

variable {W}

def linComb (G : RelativeGroupLaw T (projModelStrCR W)) (P Q : Section W) (a b : β„•) : Section W :=
  G.mul _ (G.nsmul _ a P) (G.nsmul _ b Q)

def basisTuple (G : RelativeGroupLaw T (projModelStrCR W)) (q : β„•) (P Q : Section W) :
    Fin (q * q) β†’ (base (T := T) ⟢ projModelCR W) :=
  fun i => (linComb G P Q (i.val / q) (i.val % q)).1

theorem basisTuple_over (G : RelativeGroupLaw T (projModelStrCR W)) (q : β„•) (P Q : Section W) (i : Fin (q * q)) :
    basisTuple G q P Q i ≫ projModelStrCR W = πŸ™ _ :=
  (linComb G P Q (i.val / q) (i.val % q)).2

def basisDivisor (G : RelativeGroupLaw T (projModelStrCR W)) (q : β„•) (P Q : Section W) :
    (pullback (projModelStrCR W) (πŸ™ (base (T := T)))).IdealSheafData :=
  prodKerGraph (projModelStrCR W) (basisTuple G q P Q) (basisTuple_over G q P Q)

def toPullbackId : projModelCR W ⟢ pullback (projModelStrCR W) (πŸ™ (base (T := T))) :=
  pullback.lift (πŸ™ _) (projModelStrCR W) (by simp)

def torsionIdeal (G : RelativeGroupLaw T (projModelStrCR W)) (q : β„•) :
    (pullback (projModelStrCR W) (πŸ™ (base (T := T)))).IdealSheafData :=
  (pullback.fst (G.schemeNsmul q) (G.one (πŸ™ (base (T := T)))).1 ≫ toPullbackId).ker

def IsDrinfeldBasis (G : RelativeGroupLaw T (projModelStrCR W)) (q : β„•) (P Q : Section W) : Prop :=
  basisDivisor G q P Q = torsionIdeal G q

abbrev GroupLawFamily (A : Type u) [CommRing A] : Type (u + 1) :=
  βˆ€ (T : Type u) [CommRing T] [Algebra A T] (W : WeierstrassCurve.Projective T), RelativeGroupLaw T (projModelStrCR W)

def GroupLawFamily.IsChordTangent {A : Type u} [CommRing A] (𝒒 : GroupLawFamily A) : Prop :=
  βˆ€ (T : Type u) [CommRing T] [Algebra A T] (W : WeierstrassCurve.Projective T), βˆƒ ev, IsPointsEval W (𝒒 T W) ev

structure RawDrinfeldPair (T : Type u) [CommRing T] where

  curve : WeierstrassCurve.Projective T

  P : Section curve

  Q : Section curve

def IsDrinfeldLevel {A : Type u} [CommRing A] (𝒒 : GroupLawFamily A) (q : β„•)
    {T : Type u} [CommRing T] [Algebra A T] (W : WeierstrassCurve.Projective T) (x : RawDrinfeldPair T) : Prop :=
  x.curve = W ∧ IsDrinfeldBasis (𝒒 T x.curve) q x.P x.Q

structure DrinfeldTransport (A : Type u) [CommRing A] (𝒒 : GroupLawFamily A) (q : β„•) where

  map : {T T' : Type u} β†’ [CommRing T] β†’ [Algebra A T] β†’ [CommRing T'] β†’ [Algebra A T'] β†’
    (T →ₐ[A] T') β†’ RawDrinfeldPair T β†’ RawDrinfeldPair T'

  act : {T : Type u} β†’ [CommRing T] β†’ [Algebra A T] β†’
    WeierstrassCurve.VariableChange T β†’ RawDrinfeldPair T β†’ RawDrinfeldPair T
  map_id : βˆ€ {T : Type u} [CommRing T] [Algebra A T] (x : RawDrinfeldPair T), map (AlgHom.id A T) x = x
  map_comp : βˆ€ {T T' T'' : Type u} [CommRing T] [Algebra A T] [CommRing T'] [Algebra A T'] [CommRing T'']
    [Algebra A T''] (f : T →ₐ[A] T') (g : T' →ₐ[A] T'') (x : RawDrinfeldPair T),
    map (g.comp f) x = map g (map f x)
  act_one : βˆ€ {T : Type u} [CommRing T] [Algebra A T] (x : RawDrinfeldPair T),
    act (1 : WeierstrassCurve.VariableChange T) x = x
  act_mul : βˆ€ {T : Type u} [CommRing T] [Algebra A T] (C C' : WeierstrassCurve.VariableChange T)
    (x : RawDrinfeldPair T), act (C * C') x = act C (act C' x)
  map_act : βˆ€ {T T' : Type u} [CommRing T] [Algebra A T] [CommRing T'] [Algebra A T'] (f : T →ₐ[A] T')
    (C : WeierstrassCurve.VariableChange T) (x : RawDrinfeldPair T),
    map f (act C x) = act (C.map f.toRingHom) (map f x)
  isLevel_map : βˆ€ {T T' : Type u} [CommRing T] [Algebra A T] [CommRing T'] [Algebra A T'] (f : T →ₐ[A] T')
    (W : WeierstrassCurve T) (x : RawDrinfeldPair T),
    IsDrinfeldLevel 𝒒 q W x β†’ IsDrinfeldLevel 𝒒 q (W.map f.toRingHom) (map f x)
  isLevel_act : βˆ€ {T : Type u} [CommRing T] [Algebra A T] (C : WeierstrassCurve.VariableChange T)
    (W : WeierstrassCurve T) (x : RawDrinfeldPair T),
    IsDrinfeldLevel 𝒒 q W x β†’ IsDrinfeldLevel 𝒒 q (C β€’ W) (act C x)

def drinfeldComponent (A : Type u) [CommRing A] (𝒒 : GroupLawFamily A) (q : β„•) (𝒯 : DrinfeldTransport A 𝒒 q) :
    ModularCurve.LevelComponent A where
  obj T _ _ := RawDrinfeldPair T
  IsLevel W x := IsDrinfeldLevel 𝒒 q W x
  map f x := 𝒯.map f x
  act C x := 𝒯.act C x
  map_id x := 𝒯.map_id x
  map_comp f g x := 𝒯.map_comp f g x
  act_one x := 𝒯.act_one x
  act_mul C C' x := 𝒯.act_mul C C' x
  map_act f C x := 𝒯.map_act f C x
  isLevel_map f W x h := 𝒯.isLevel_map f W x h
  isLevel_act C W x h := 𝒯.isLevel_act C W x h

noncomputable def fullLevelRigidData (A : Type u) [CommRing A] (β„“ N q : β„•)
    (hβ„“ : βˆ€ (T : Type u) [CommRing T] [Algebra A T] (W : WeierstrassCurve T) (C : WeierstrassCurve.VariableChange T)
      (D : ModularCurve.LevelPData T), ModularCurve.IsLevelPStructure W β„“ D β†’
        ModularCurve.IsLevelPStructure (C β€’ W) β„“ (D.variableChange C))
    (hN : βˆ€ (T : Type u) [CommRing T] [Algebra A T] (W : WeierstrassCurve T) (C : WeierstrassCurve.VariableChange T)
      (h : Polynomial T), W.IsCyclicKernel N h β†’ (C β€’ W).IsCyclicKernel N (ModularCurve.kernelVariableChangeDeg C ((N - 1) / 2) h))
    (𝒒 : GroupLawFamily A) (𝒯 : DrinfeldTransport A 𝒒 q) : ModularCurve.RigidWeierstrassData.{u} A :=
  ModularCurve.weierstrassLevelRigidData A β„“ N hβ„“ hN (drinfeldComponent A 𝒒 q 𝒯)

end WeierstrassCurve.DrinfeldGlobal

end

Statements phrased using this module (473)

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