Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_WeierstrassCurve_DrinfeldTransportPin.lean

definition module

Section-compatibility pin for Drinfeld transport data

The module fixes a Weierstrass curve W in projective form over a commutative ring T and works with its projective model: the quotient of T[X_0,X_1,X_2] by the homogeneous ideal generated by the Weierstrass cubic, with its induced grading, and the scheme \mathrm{Proj} of that grading. The abbreviation cls sends a polynomial to its class in this quotient.

Two predicates single out graded ring maps by their effect on coordinate classes. For a change of variables C=(u,r,s,t) over T, IsVariableChangeHom says of a graded homomorphism \varphi from the model ring of W to that of C\bullet W that it fixes constants and satisfies X_0\mapsto u^2X_0+rX_2, X_1\mapsto u^3X_1+u^2sX_0+tX_2, X_2\mapsto X_2. For a ring map f, IsCoefficientHom says that \varphi from the model ring of W to that of W mapped by f acts on constants by a\mapsto f(a) and fixes each coordinate class.

The main definition is a predicate on a transport datum \mathcal T for raw Drinfeld pairs (a curve together with two sections of its projective model over the base) over A-algebras. IsSectionTransport asserts two things. First, for every A-algebra T, every change of variables C and every raw pair x, the curve of \mathcal T.\mathrm{act}\,C\,x equals C\bullet x.\mathrm{curve}, and, for every \varphi as in IsVariableChangeHom admitting the irrelevant-ideal hypothesis needed to form Proj.map, each of the two sections of \mathcal T.\mathrm{act}\,C\,x followed by the identification of models and by \mathrm{Proj}(\varphi) recovers the corresponding section of x. Second, for f : T \to T' an A-algebra map, the curve of \mathcal T.\mathrm{map}\,f\,x is x.\mathrm{curve} mapped by f, and for every \varphi as in IsCoefficientHom the sections of \mathcal T.\mathrm{map}\,f\,x followed by the model identification and \mathrm{Proj}(\varphi) agree with \mathrm{Spec}(f) followed by the sections of x.

Relation to Mathlib

Mathlib supplies WeierstrassCurve.Projective, WeierstrassCurve.VariableChange, and the functoriality Proj.map of \mathrm{Proj} in graded ring maps; the projective model scheme of a Weierstrass curve, raw Drinfeld pairs with their transport data, and the compatibility predicates defined here are the project's own.

Where it is used

The transport datum of a Drinfeld full-level component is a priori only assumed to satisfy the functoriality laws; this predicate pins it to the geometrically canonical transport, so that representability of the associated rigid level-moduli functor can be asserted for transport data satisfying the pin rather than for arbitrary lawful data. It thus sits in the construction of the modular curves with Drinfeld level structure used on the modularity side of the argument.

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

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_WeierstrassCurve_ProjModel
import Definitions.Def_WeierstrassCurve_DrinfeldBasisGlobal

set_option autoImplicit false

universe u

noncomputable section

open AlgebraicGeometry CategoryTheory WeierstrassProjModel MvPolynomial

attribute [local instance] MvPolynomial.gradedAlgebra

namespace WeierstrassCurve.DrinfeldGlobal

abbrev cls {T : Type u} [CommRing T] (W : WeierstrassCurve.Projective T) (p : MvPolynomial (Fin 3) T) :
    ProjModelRingCR W :=
  Ideal.Quotient.mk (projModelHomogeneousIdealCR W).toIdeal p

def IsVariableChangeHom {T : Type u} [CommRing T] (W : WeierstrassCurve.Projective T)
    (C : WeierstrassCurve.VariableChange T) (φ : projModelGradingCR W →+*ᵍ projModelGradingCR (C • W)) : Prop :=
  (∀ a : T, φ (cls W (MvPolynomial.C a)) = cls (C • W) (MvPolynomial.C a)) ∧
  φ (cls W (X 0)) = cls (C • W) (MvPolynomial.C ((C.u : T) ^ 2) * X 0 + MvPolynomial.C C.r * X 2) ∧
  φ (cls W (X 1)) = cls (C • W)
    (MvPolynomial.C ((C.u : T) ^ 3) * X 1 + MvPolynomial.C ((C.u : T) ^ 2 * C.s) * X 0 + MvPolynomial.C C.t * X 2) ∧
  φ (cls W (X 2)) = cls (C • W) (X 2)

def IsCoefficientHom {T T' : Type u} [CommRing T] [CommRing T'] (W : WeierstrassCurve.Projective T) (f : T →+* T')
    (φ : projModelGradingCR W →+*ᵍ projModelGradingCR (W.map f)) : Prop :=
  (∀ a : T, φ (cls W (MvPolynomial.C a)) = cls (W.map f) (MvPolynomial.C (f a))) ∧
  ∀ i : Fin 3, φ (cls W (X i)) = cls (W.map f) (X i)

variable {A : Type u} [CommRing A]

def DrinfeldTransport.IsSectionTransport {𝒢 : GroupLawFamily A} {q : ℕ} (𝒯 : DrinfeldTransport 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)

end WeierstrassCurve.DrinfeldGlobal

end

Statements phrased using this module (299)

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