Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_MvPolynomial_CrossingResolution.lean

definition module

Charts and transitions resolving the crossing

Throughout, W is a commutative ring and t \in W; CrossingQuotient W t denotes W[x_0,x_1]/(x_0x_1 - C\,t), the quotient of MvPolynomial (Fin 2) W by the ideal generated by X_0X_1 - C\,t, with mk t the quotient W-algebra map. The abbreviations U t and V t are the classes of X_0 and X_1, and U_mul_V records U\cdot V = \mathrm{algebraMap}_W\,t. The universal property is packaged by lift: given a W-algebra A and a, b \in A with ab equal to the image of t, lift t a b h is the W-algebra homomorphism CrossingQuotient W t \to A obtained from \mathrm{aeval} at the vector [a,b], the preliminary lemma aeval_rel_eq_zero supplying the vanishing of the relation; lift_mk, lift_U and lift_V state that it sends the class of a polynomial p to p(a,b), and in particular U \mapsto a, V \mapsto b.

Two families of maps are then defined by this recipe. For e : \mathbb{N} and i \in \mathrm{Fin}\,e, resolutionChart t e i is the W-algebra homomorphism CrossingQuotient W (t ^ e) \to CrossingQuotient W t with U \mapsto t^{i}\,U and V \mapsto t^{e-1-i}\,V (where t^{k} means its image under the structure map); this is legitimate because i + (e-1-i) + 1 = e for i < e, and resolutionChart_U, resolutionChart_V record the two values. Next, transitionUp t is the W-algebra homomorphism from CrossingQuotient W t to the localisation Localization.Away (V t) sending U to the inverse IsLocalization.Away.invSelf (V t) of V and V to t times the image of V; transitionDown t is its counterpart into Localization.Away (U t), sending U to t times the image of U and V to the inverse of U. The lemmas transitionUp_U, transitionUp_V, transitionDown_U, transitionDown_V give these values. Only the maps and their computation rules on U and V are set up here; no regularity, covering or isomorphism assertion is made.

Relation to Mathlib

Built on Mathlib's MvPolynomial, Ideal.Quotient.liftₐ, aeval, Localization.Away and IsLocalization.Away.invSelf; the crossing quotient W[x,y]/(xy-t) together with these chart and transition maps is the project's own vocabulary.

Where it is used

These maps are the affine vocabulary for the explicit resolution of the A_{e-1} singularity uv = t^{e} over a base such as a discrete valuation ring with uniformiser t: the e charts \mathrm{Spec}\,W[x,y]/(xy-t) mapping to \mathrm{Spec}\,W[u,v]/(uv-t^{e}), glued along the two transition maps on the loci where U or V is invertible. They serve the local analysis of models of modular curves at points where the special fibre acquires an ordinary double point of thickness e.

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
  2. W. Fulton, Introduction to Toric Varieties, Annals of Mathematics Studies 131, Princeton University Press, 1993

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_MvPolynomial_CrossingQuotient

set_option autoImplicit false

noncomputable section

namespace MvPolynomial

namespace CrossingQuotient

variable {W : Type*} [CommRing W] (t : W)

abbrev U : CrossingQuotient W t := mk t (X 0)

abbrev V : CrossingQuotient W t := mk t (X 1)

theorem U_mul_V : U t * V t = algebraMap W (CrossingQuotient W t) t := mk_X_mul_mk_X t

theorem aeval_rel_eq_zero {A : Type*} [CommRing A] [Algebra W A] (a b : A)
    (h : a * b = algebraMap W A t) :
    aeval ![a, b] (X 0 * X 1 - C t : MvPolynomial (Fin 2) W) = 0 := by
  rw [map_sub, map_mul, aeval_X, aeval_X, aeval_C]
  simp only [Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_fin_one]
  rw [h, sub_self]

def lift {A : Type*} [CommRing A] [Algebra W A] (a b : A) (h : a * b = algebraMap W A t) :
    CrossingQuotient W t →ₐ[W] A :=
  Ideal.Quotient.liftₐ (Ideal.span {(X 0 * X 1 - C t : MvPolynomial (Fin 2) W)}) (aeval ![a, b])
    (fun p hp => by
      obtain ⟨c, rfl⟩ := Ideal.mem_span_singleton'.mp hp
      rw [map_mul, aeval_rel_eq_zero t a b h, mul_zero])

theorem lift_mk {A : Type*} [CommRing A] [Algebra W A] (a b : A) (h : a * b = algebraMap W A t)
    (p : MvPolynomial (Fin 2) W) : lift t a b h (mk t p) = aeval ![a, b] p := rfl

@[simp] theorem lift_U {A : Type*} [CommRing A] [Algebra W A] (a b : A)
    (h : a * b = algebraMap W A t) : lift t a b h (U t) = a := by
  rw [lift_mk, aeval_X]; rfl

@[simp] theorem lift_V {A : Type*} [CommRing A] [Algebra W A] (a b : A)
    (h : a * b = algebraMap W A t) : lift t a b h (V t) = b := by
  rw [lift_mk, aeval_X]; rfl

def resolutionChart (e : ℕ) (i : Fin e) : CrossingQuotient W (t ^ e) →ₐ[W] CrossingQuotient W t :=
  lift (t ^ e) (algebraMap W _ (t ^ (i : ℕ)) * U t) (algebraMap W _ (t ^ (e - 1 - i)) * V t) (by
    have hi : (i : ℕ) + (e - 1 - i) + 1 = e := by have := i.2; omega
    rw [mul_mul_mul_comm, U_mul_V, ← map_mul, ← map_mul, ← pow_add, ← pow_succ, hi])

theorem resolutionChart_U (e : ℕ) (i : Fin e) :
    resolutionChart t e i (U (t ^ e)) = algebraMap W _ (t ^ (i : ℕ)) * U t := lift_U _ _ _ _

theorem resolutionChart_V (e : ℕ) (i : Fin e) :
    resolutionChart t e i (V (t ^ e)) = algebraMap W _ (t ^ (e - 1 - i)) * V t := lift_V _ _ _ _

def transitionUp : CrossingQuotient W t →ₐ[W] Localization.Away (V t) :=
  lift t (IsLocalization.Away.invSelf (V t))
    (algebraMap W _ t * algebraMap (CrossingQuotient W t) _ (V t)) (by
      rw [mul_left_comm, mul_comm (IsLocalization.Away.invSelf (V t)),
        IsLocalization.Away.mul_invSelf, mul_one,
        IsScalarTower.algebraMap_apply W (CrossingQuotient W t) (Localization.Away (V t))])

theorem transitionUp_U :
    transitionUp t (U t) = IsLocalization.Away.invSelf (V t) := lift_U _ _ _ _

theorem transitionUp_V : transitionUp t (V t) =
    algebraMap W _ t * algebraMap (CrossingQuotient W t) (Localization.Away (V t)) (V t) :=
  lift_V _ _ _ _

def transitionDown : CrossingQuotient W t →ₐ[W] Localization.Away (U t) :=
  lift t (algebraMap W _ t * algebraMap (CrossingQuotient W t) _ (U t))
    (IsLocalization.Away.invSelf (U t)) (by
      rw [mul_assoc, IsLocalization.Away.mul_invSelf, mul_one,
        IsScalarTower.algebraMap_apply W (CrossingQuotient W t) (Localization.Away (U t))])

theorem transitionDown_U : transitionDown t (U t) =
    algebraMap W _ t * algebraMap (CrossingQuotient W t) (Localization.Away (U t)) (U t) :=
  lift_U _ _ _ _

theorem transitionDown_V :
    transitionDown t (V t) = IsLocalization.Away.invSelf (U t) := lift_V _ _ _ _

end CrossingQuotient

end MvPolynomial

end

Statements phrased using this module (6)