Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_WeierstrassCurve_DrinfeldLevelFunctor.lean

definition module

Guarded group laws and the Drinfeld level component

Let A be a commutative ring. GroupLaws A is the type of families assigning, to every A-algebra T, every projective Weierstrass curve W over T and every proof that \Delta(W) is a unit, a RelativeGroupLaw on the structure morphism \mathrm{Proj}\,(T[X,Y,Z]/(W))\to\operatorname{Spec}T β€” that is, a group structure on the sets of sections \mathrm{Hom}_{/\operatorname{Spec}T}(T',\cdot), natural in T', with the group axioms and naturality of multiplication as fields. Compared with the unguarded family of the imported module, the quantifier is restricted to curves with invertible discriminant. Two predicates pin such a family down: IsChordTangent asks, for each T,W,h_\Delta, the existence of bijections between sections over \operatorname{Spec}F and the affine point group of W_F, for all fields F over T, which are additive and equivariant for T-automorphisms of F; IsOriginIdentity asks that the identity section factor through the chart D_+(Y) via a ring homomorphism \chi from the homogeneous localisation away from Y with \chi(X/Y)=\chi(Z/Y)=0, i.e. that the identity be [0:1:0].

For a raw triple x=(W',P,Q), RawDrinfeldPair.IsLevel 𝒒 q W x says W'=W and, for some unit proof, the q^2 sections aP+bQ (0\le a,b<q) form a Drinfeld basis: the product of the kernel ideal sheaves of their graphs equals the ideal sheaf of the q-torsion subscheme. LevelTransport is a structure carrying base change along A-algebra maps and an action of variable changes on raw pairs, with functoriality, compatibility and preservation of IsLevel as fields; IsSectionTransport pins these operations on sections, requiring the transported P,Q to pull back to the original ones along any graded homomorphism realising the variable change, respectively the coefficient map. Finally levelComponent assembles this into a ModularCurve.LevelComponent A, and rigidData combines it with the \Gamma_0(N) cyclic-kernel and level-\ell components into a ModularCurve.RigidWeierstrassData A.

Relation to Mathlib

Mathlib supplies WeierstrassCurve.Projective, VariableChange, Proj and ideal sheaf data; the relative group law on a morphism of schemes, the graded Proj model of a Weierstrass cubic, Drinfeld bases and level components are the project's own notions, defined in the imported modules.

Where it is used

These data furnish the moduli problem of elliptic curves with a \Gamma_0(N)-structure, a level-\ell structure and a Drinfeld basis of the q-torsion, in the rigidified form used for the representability statement underlying the modular curves of the Frey-curve argument.

References

  1. N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, Annals of Mathematics Studies 108, Princeton University Press, 1985
  2. V. G. Drinfeld, Elliptic modules, Mat. Sbornik 94 (1974), 594–627
  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_DrinfeldLevelFunctor.lean

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_WeierstrassCurve_ProjModel
import Definitions.Def_ModularCurve_WeierstrassLevelComponents
import Definitions.Def_WeierstrassCurve_DrinfeldBasisGlobal
import Definitions.Def_WeierstrassCurve_DrinfeldTransportPin
import Definitions.Def_WeierstrassCurve_SectionAtOrigin

set_option autoImplicit false

universe u

noncomputable section

open AlgebraicGeometry CategoryTheory WeierstrassProjModel

attribute [local instance] MvPolynomial.gradedAlgebra

namespace WeierstrassCurve.DrinfeldGlobal

variable {A : Type u} [CommRing A]

abbrev GroupLaws (A : Type u) [CommRing A] : Type (u + 1) :=
  βˆ€ (T : Type u) [CommRing T] [Algebra A T] (W : WeierstrassCurve.Projective T), IsUnit W.Ξ” β†’
    RelativeGroupLaw T (projModelStrCR W)

def GroupLaws.IsChordTangent (𝒒 : GroupLaws A) : Prop :=
  βˆ€ (T : Type u) [CommRing T] [Algebra A T] (W : WeierstrassCurve.Projective T) (hΞ” : IsUnit W.Ξ”),
    βˆƒ ev, IsPointsEval W (𝒒 T W hΞ”) ev

def GroupLaws.IsOriginIdentity (𝒒 : GroupLaws A) : Prop :=
  βˆ€ (T : Type u) [CommRing T] [Algebra A T] (W : WeierstrassCurve.Projective T) (hΞ” : IsUnit W.Ξ”),
    βˆƒ Ο‡ : OriginChartRing W β†’+* T,
      IsOriginChartSection ((𝒒 T W hΞ”).one (πŸ™ _)) Ο‡ ∧ Ο‡ (xOverY W) = 0 ∧ Ο‡ (zOverY W) = 0

def RawDrinfeldPair.IsLevel (𝒒 : GroupLaws A) (q : β„•)
    {T : Type u} [CommRing T] [Algebra A T] (W : WeierstrassCurve.Projective T) (x : RawDrinfeldPair T) : Prop :=
  x.curve = W ∧ βˆƒ hΞ” : IsUnit x.curve.Ξ”, IsDrinfeldBasis (𝒒 T x.curve hΞ”) q x.P x.Q

structure LevelTransport (A : Type u) [CommRing A] (𝒒 : GroupLaws 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),
    RawDrinfeldPair.IsLevel 𝒒 q W x β†’ RawDrinfeldPair.IsLevel 𝒒 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),
    RawDrinfeldPair.IsLevel 𝒒 q W x β†’ RawDrinfeldPair.IsLevel 𝒒 q (C β€’ W) (act C x)

def LevelTransport.IsSectionTransport {𝒒 : GroupLaws A} {q : β„•} (𝒯 : LevelTransport A 𝒒 q) : Prop :=
  (βˆ€ (T : Type u) [CommRing T] [Algebra A T] (C : WeierstrassCurve.VariableChange T) (x : RawDrinfeldPair T),
    βˆƒ hc : (𝒯.act C x).curve = C β€’ x.curve,
      βˆ€ (Ο† : projModelGradingCR x.curve β†’+*ᡍ projModelGradingCR (C β€’ x.curve))
        (hΟ† : HomogeneousIdeal.irrelevant (projModelGradingCR (C β€’ x.curve)) ≀
          (HomogeneousIdeal.irrelevant (projModelGradingCR x.curve)).map Ο†),
        IsVariableChangeHom x.curve C Ο† β†’
          (𝒯.act C x).P.1 ≫ eqToHom (congrArg projModelCR hc) ≫ Proj.map Ο† hΟ† = x.P.1 ∧
          (𝒯.act C x).Q.1 ≫ eqToHom (congrArg projModelCR hc) ≫ Proj.map Ο† hΟ† = x.Q.1) ∧
  (βˆ€ (T T' : Type u) [CommRing T] [Algebra A T] [CommRing T'] [Algebra A T'] (f : T →ₐ[A] T')
    (x : RawDrinfeldPair T),
    βˆƒ hc : (𝒯.map f x).curve = x.curve.map f.toRingHom,
      βˆ€ (Ο† : projModelGradingCR x.curve β†’+*ᡍ projModelGradingCR (x.curve.map f.toRingHom))
        (hΟ† : HomogeneousIdeal.irrelevant (projModelGradingCR (x.curve.map f.toRingHom)) ≀
          (HomogeneousIdeal.irrelevant (projModelGradingCR x.curve)).map Ο†),
        IsCoefficientHom x.curve f.toRingHom Ο† β†’
          (𝒯.map f x).P.1 ≫ eqToHom (congrArg projModelCR hc) ≫ Proj.map Ο† hΟ† =
            Spec.map (CommRingCat.ofHom f.toRingHom) ≫ x.P.1 ∧
          (𝒯.map f x).Q.1 ≫ eqToHom (congrArg projModelCR hc) ≫ Proj.map Ο† hΟ† =
            Spec.map (CommRingCat.ofHom f.toRingHom) ≫ x.Q.1)

def levelComponent (A : Type u) [CommRing A] (𝒒 : GroupLaws A) (q : β„•) (𝒯 : LevelTransport A 𝒒 q) :
    ModularCurve.LevelComponent A where
  obj T _ _ := RawDrinfeldPair T
  IsLevel W x := RawDrinfeldPair.IsLevel 𝒒 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

def rigidData (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))
    (𝒒 : GroupLaws A) (𝒯 : LevelTransport A 𝒒 q) : ModularCurve.RigidWeierstrassData.{u} A :=
  ModularCurve.weierstrassLevelRigidData A β„“ N hβ„“ hN (levelComponent A 𝒒 q 𝒯)

end WeierstrassCurve.DrinfeldGlobal

end

Statements phrased using this module (419)

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