Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_MvPolynomial_CrossingQuotient.lean

definition module

Coordinate ring of the crossing

Over a commutative ring W and an element t : W, MvPolynomial.CrossingQuotient W t is defined to be the quotient of the polynomial ring in two variables W[X_0, X_1] (indexed by Fin 2) by the principal ideal generated by X_0 X_1 - t, i.e. the coordinate ring W[x,y]/(xy - t) of the crossing xy = t. The quotient map mk t is the W-algebra homomorphism W[X_0,X_1] \to W[x,y]/(xy-t); mk_apply identifies it with the underlying ring-theoretic quotient map, mk_surjective records surjectivity, and mk_X_mul_mk_X records the defining relation in the quotient, namely that the product of the classes of X_0 and X_1 is the image of t under the structure map W \to W[x,y]/(xy-t).

On top of this, monomial t is a family of elements of the quotient indexed by \mathbb{Z}: for n \ge 0 it is the n-th power of the class x of X_0, and for n < 0 it is the (-n)-th power of the class y of X_1; the accompanying lemmas evaluate it on the two branches, on nonnegative and nonpositive integer casts, and at 0, where it is 1. Finally, for a natural number e, powMap t e is the W-algebra homomorphism W[u,v]/(uv - t^e) \longrightarrow W[x,y]/(xy - t) obtained by factoring the evaluation u \mapsto x^e, v \mapsto y^e through the quotient; this is well defined because x^e y^e = (xy)^e = t^e. The lemmas powMap_mk and powMap_mk_X describe it on the class of an arbitrary polynomial, as the evaluation sending each variable X_i to the e-th power of the class of X_i, and on the classes of the two variables themselves.

Relation to Mathlib

Everything here is assembled from Mathlib's MvPolynomial and Ideal.Quotient API; Mathlib has no dedicated name for this quotient, so CrossingQuotient and its monomial and power-map vocabulary are the project's own abbreviations.

Where it is used

These definitions furnish the algebraic vocabulary for crossings xy = t, the local models of the non-smooth points of semistable degenerations of curves, together with the power maps relating the crossing with parameter t^e to the one with parameter t. They serve as the polynomial counterpart of the corresponding power-series crossing model used in the study of models of modular curves.

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

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

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib

set_option autoImplicit false

noncomputable section

namespace MvPolynomial

variable (W : Type*) [CommRing W]

abbrev CrossingQuotient (t : W) : Type _ :=
  MvPolynomial (Fin 2) W ⧸ Ideal.span {(X 0 * X 1 - C t : MvPolynomial (Fin 2) W)}

variable {W}

namespace CrossingQuotient

variable (t : W)

abbrev mk : MvPolynomial (Fin 2) W →ₐ[W] CrossingQuotient W t :=
  Ideal.Quotient.mkₐ W (Ideal.span {(X 0 * X 1 - C t : MvPolynomial (Fin 2) W)})

theorem mk_apply (p : MvPolynomial (Fin 2) W) :
    mk t p = Ideal.Quotient.mk (Ideal.span {(X 0 * X 1 - C t : MvPolynomial (Fin 2) W)}) p := rfl

theorem mk_surjective : Function.Surjective (mk t) := Ideal.Quotient.mkₐ_surjective W _

theorem mk_X_mul_mk_X : mk t (X 0) * mk t (X 1) = algebraMap W (CrossingQuotient W t) t := by
  rw [← map_mul, Ideal.Quotient.mkₐ_eq_mk, ← Ideal.Quotient.mk_algebraMap, algebraMap_eq, Ideal.Quotient.eq]
  exact Ideal.subset_span rfl

def monomial (n : ℤ) : CrossingQuotient W t :=
  if 0 ≤ n then mk t (X 0) ^ n.toNat else mk t (X 1) ^ (-n).toNat

theorem monomial_of_nonneg {n : ℤ} (h : 0 ≤ n) : monomial t n = mk t (X 0) ^ n.toNat := if_pos h

theorem monomial_of_neg {n : ℤ} (h : n < 0) : monomial t n = mk t (X 1) ^ (-n).toNat := if_neg (not_le.mpr h)

@[simp] theorem monomial_natCast (n : ℕ) : monomial t (n : ℤ) = mk t (X 0) ^ n := by
  rw [monomial_of_nonneg t (Int.natCast_nonneg n), Int.toNat_natCast]

@[simp] theorem monomial_neg_natCast (n : ℕ) : monomial t (-(n : ℤ)) = mk t (X 1) ^ n := by
  rcases Nat.eq_zero_or_pos n with rfl | hn
  · rw [Nat.cast_zero, neg_zero, monomial_of_nonneg t le_rfl, Int.toNat_zero, pow_zero, pow_zero]
  · rw [monomial_of_neg t (by omega), neg_neg, Int.toNat_natCast]

@[simp] theorem monomial_zero : monomial t 0 = 1 := by
  rw [monomial_of_nonneg t le_rfl, Int.toNat_zero, pow_zero]

def powMap (e : ℕ) : CrossingQuotient W (t ^ e) →ₐ[W] CrossingQuotient W t :=
  Ideal.Quotient.liftₐ (Ideal.span {(X 0 * X 1 - C (t ^ e) : MvPolynomial (Fin 2) W)})
    (aeval fun i : Fin 2 => mk t (X i) ^ e) (by
      intro p hp
      obtain ⟨c, rfl⟩ := Ideal.mem_span_singleton'.mp hp
      rw [map_mul, map_sub, map_mul, aeval_X, aeval_X, aeval_C, ← mul_pow, mk_X_mul_mk_X, ← map_pow, sub_self,
        mul_zero])

theorem powMap_mk (e : ℕ) (p : MvPolynomial (Fin 2) W) :
    powMap t e (mk (t ^ e) p) = aeval (fun i : Fin 2 => mk t (X i) ^ e) p := rfl

@[simp] theorem powMap_mk_X (e : ℕ) (i : Fin 2) : powMap t e (mk (t ^ e) (X i)) = mk t (X i) ^ e := by
  rw [powMap_mk, aeval_X]

end CrossingQuotient

end MvPolynomial

end

Statements phrased using this module (4)