Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_UVCrossingModel.lean

definition module

Crossing local model and its branch swap

For a commutative ring W and an element \pi \in W, uvCrossingIdeal is the principal ideal of the two-variable formal power series ring W[[u,v]] (realised as MvPowerSeries (Fin 2) W, with u = X_0, v = X_1) generated by X_0 X_1 - C\,\pi, and UVCrossingModel W π is the quotient ring W[[u,v]]/(uv - \pi). Attached to it are the quotient map mk, the images U and V of the two variables, the element const π w given by the image of the constant series C\,w together with the ring homomorphism constHom \colon W \to W[[u,v]]/(uv-\pi) obtained by composing C with mk, and the surjectivity of mk. The abbreviation wittCrossingModel p k, for a prime p and a field k, specialises this to W = W(p,k), the ring of p-typical Witt vectors of k, and \pi = p, giving W(k)[[u,v]]/(uv - p).

The second half constructs the involution exchanging the two variables. uvSwapEquiv is the ring automorphism of W[[u,v]] induced by renaming along the transposition of 0 and 1 in Fin 2; the lemmas record that it sends X_0 \mapsto X_1, X_1 \mapsto X_0, fixes constants, fixes the generator X_0X_1 - C\,\pi, and hence carries uvCrossingIdeal W π onto itself. Consequently crossingSwap π is the induced ring automorphism of W[[u,v]]/(uv-\pi), compatible with mk and uvSwapEquiv. Finally S π and D π are the symmetric and antisymmetric coordinates u + v and u - v, and fixedSubring π is the subring on which crossingSwap π agrees with the identity, i.e. \{x : \text{crossingSwap}\,\pi\,(x) = x\}, this characterisation being recorded as mem_fixedSubring_iff. All of this is a construction of a specific ring with an involution; no regularity, completeness or moduli-theoretic property is asserted here.

Relation to Mathlib

Built directly on Mathlib's MvPowerSeries, Ideal.Quotient and MvPowerSeries.renameEquiv; Mathlib has no notion of such a crossing local model, so the ring, the variable-swap automorphism and the fixed subring are the project's own definitions.

Where it is used

The ring W(\overline{\mathbb F}_p)[[u,v]]/(uv-p) is the standard local model for the completed local ring of a modular curve with \Gamma_0(p)-level structure at a supersingular point, where the two branches u = 0 and v = 0 of the special fibre correspond to the two components of the mod p fibre and the variable swap models the Atkin–Lehner involution w_p. It therefore serves as the local input for the study of modular curves and their Jacobians at p in the route to Fermat's Last Theorem.

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 (Ch. V)
  2. N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, Annals of Mathematics Studies 108, Princeton University Press, 1985, Theorem 13.4.7
  3. B. Mazur, Modular curves and the Eisenstein ideal, Publications Mathématiques de l'IHÉS 47 (1977), 33–186

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

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib

set_option autoImplicit false

universe u

namespace ModularCurve

noncomputable section

abbrev uvCrossingIdeal (W : Type u) [CommRing W] (π : W) : Ideal (MvPowerSeries (Fin 2) W) :=
  Ideal.span {(MvPowerSeries.X 0 : MvPowerSeries (Fin 2) W) * MvPowerSeries.X 1 -
    MvPowerSeries.C π}

abbrev UVCrossingModel (W : Type u) [CommRing W] (π : W) : Type u :=
  MvPowerSeries (Fin 2) W ⧸ uvCrossingIdeal W π

namespace UVCrossingModel

variable {W : Type u} [CommRing W]

def mk (π : W) : MvPowerSeries (Fin 2) W →+* UVCrossingModel W π :=
  Ideal.Quotient.mk _

def U (π : W) : UVCrossingModel W π := mk π (MvPowerSeries.X 0)

def V (π : W) : UVCrossingModel W π := mk π (MvPowerSeries.X 1)

def const (π : W) (w : W) : UVCrossingModel W π := mk π (MvPowerSeries.C w)

def constHom (π : W) : W →+* UVCrossingModel W π :=
  (mk π).comp (MvPowerSeries.C : W →+* MvPowerSeries (Fin 2) W)

theorem constHom_apply (π : W) (w : W) : constHom π w = const π w := rfl

theorem mk_surjective (π : W) : Function.Surjective (mk (W := W) π) :=
  Ideal.Quotient.mk_surjective

end UVCrossingModel

abbrev wittCrossingModel (p : ℕ) [Fact p.Prime] (k : Type u) [Field k] : Type u :=
  UVCrossingModel (WittVector p k) (p : WittVector p k)

section VariableSwap

variable {W : Type u} [CommRing W]

def uvSwapEquiv : MvPowerSeries (Fin 2) W ≃+* MvPowerSeries (Fin 2) W :=
  (MvPowerSeries.renameEquiv W (Equiv.swap (0 : Fin 2) 1)).toRingEquiv

theorem uvSwapEquiv_apply (f : MvPowerSeries (Fin 2) W) :
    uvSwapEquiv f = MvPowerSeries.rename (⇑(Equiv.swap (0 : Fin 2) 1)) f := rfl

theorem uvSwapEquiv_X_zero :
    uvSwapEquiv (MvPowerSeries.X (0 : Fin 2) : MvPowerSeries (Fin 2) W) =
      MvPowerSeries.X 1 := by
  rw [uvSwapEquiv_apply, MvPowerSeries.rename_X, Equiv.swap_apply_left]

theorem uvSwapEquiv_X_one :
    uvSwapEquiv (MvPowerSeries.X (1 : Fin 2) : MvPowerSeries (Fin 2) W) =
      MvPowerSeries.X 0 := by
  rw [uvSwapEquiv_apply, MvPowerSeries.rename_X, Equiv.swap_apply_right]

theorem uvSwapEquiv_C (w : W) :
    uvSwapEquiv (MvPowerSeries.C w : MvPowerSeries (Fin 2) W) = MvPowerSeries.C w := by
  rw [uvSwapEquiv_apply, MvPowerSeries.rename_C]

theorem uvSwapEquiv_crossing (π : W) :
    uvSwapEquiv ((MvPowerSeries.X 0 : MvPowerSeries (Fin 2) W) * MvPowerSeries.X 1 -
        MvPowerSeries.C π) =
      (MvPowerSeries.X 0 : MvPowerSeries (Fin 2) W) * MvPowerSeries.X 1 -
        MvPowerSeries.C π := by
  rw [map_sub, map_mul, uvSwapEquiv_X_zero, uvSwapEquiv_X_one, uvSwapEquiv_C, mul_comm]

theorem map_uvSwapEquiv_uvCrossingIdeal (π : W) :
    Ideal.map (uvSwapEquiv (W := W)) (uvCrossingIdeal W π) = uvCrossingIdeal W π := by
  rw [show uvCrossingIdeal W π = Ideal.span {(MvPowerSeries.X 0 : MvPowerSeries (Fin 2) W) *
    MvPowerSeries.X 1 - MvPowerSeries.C π} from rfl, Ideal.map_span, Set.image_singleton,
    uvSwapEquiv_crossing]

end VariableSwap

namespace UVCrossingModel

variable {W : Type u} [CommRing W]

def crossingSwap (π : W) : UVCrossingModel W π ≃+* UVCrossingModel W π :=
  Ideal.quotientEquiv (uvCrossingIdeal W π) (uvCrossingIdeal W π) uvSwapEquiv
    (map_uvSwapEquiv_uvCrossingIdeal π).symm

theorem crossingSwap_mk (π : W) (f : MvPowerSeries (Fin 2) W) :
    crossingSwap π (UVCrossingModel.mk π f) = UVCrossingModel.mk π (uvSwapEquiv f) := rfl

def S (π : W) : UVCrossingModel W π := U π + V π

def D (π : W) : UVCrossingModel W π := U π - V π

theorem S_def (π : W) : S π = U π + V π := rfl

theorem D_def (π : W) : D π = U π - V π := rfl

def fixedSubring (π : W) : Subring (UVCrossingModel W π) :=
  RingHom.eqLocus
    (crossingSwap π : UVCrossingModel W π →+* UVCrossingModel W π) (RingHom.id _)

theorem mem_fixedSubring_iff {π : W} {x : UVCrossingModel W π} :
    x ∈ fixedSubring π ↔ crossingSwap π x = x :=
  Iff.rfl

end UVCrossingModel

end

end ModularCurve

Statements phrased using this module (624)

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