Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AlgebraicGeometry_SmallExtensionPairTangent.lean

definition module

Pair ring, first-order thickening, Schlessinger maps, tangent relation

Fix a local ring T' with residue field k = ResidueField T', an ideal I \subseteq T', a k-vector space V (carrying compatible k-, k^{\mathrm{op}}- and T'-module structures with central scalars and the scalar tower over T'), a T'-linear map \iota \colon V \to T', and a commutative T'-algebra C. The ring pairRing I C is the subring of C \times C on which the two projections agree after reduction modulo IC = I \cdot C (the ideal generated by the image of I), i.e. the set of pairs (x, y) with x \equiv y \pmod{IC}; mem_pairRing records this membership criterion, and pairFst, pairSnd are its two projections to C, with their evaluation lemmas. The abbreviation thickening T' V C is the ring (k \otimes_{T'} C) \otimes_k (k \oplus V), where k \oplus V is the trivial square-zero extension TrivSqZeroExt k V; toReduction is the ring map C \to k \otimes_{T'} C given by c \mapsto 1 \otimes c.

For a ring homomorphism \vartheta from pairRing I C to this thickening, IsSchlessingerMap is the conjunction of two conditions: \vartheta(a,a) = (1 \otimes a) \otimes 1 for every a \in C, and \vartheta(0, \iota(v)c) = (1 \otimes c) \otimes (0,v) for all v \in V, c \in C for which (0, \iota(v)c) lies in the pair ring. No existence claim is part of the definition, and no hypothesis ties \iota to I or imposes smallness of I.

Finally, for a scheme Y, morphisms u, v \colon \operatorname{Spec} C \to Y and w \colon \operatorname{Spec} of the thickening \to Y, the predicate IsTangentOfPair asserts the existence of a Schlessinger map \vartheta and of \varphi \colon \operatorname{Spec}(\mathrm{pairRing}\,I\,C) \to Y such that \operatorname{Spec}(\mathrm{pr}_1) followed by \varphi is u, \operatorname{Spec}(\mathrm{pr}_2) followed by \varphi is v, and w equals \operatorname{Spec}(\vartheta) followed by \varphi. It is thus a relation between (u,v) and w formulated on these explicit presentations, not a constructed bijection.

Relation to Mathlib

Built on Mathlib's RingHom.eqLocus, TrivSqZeroExt and Spec/CommRingCat machinery; the pair ring, the Schlessinger-map condition and the tangent relation are the project's own notions, Mathlib having no deformation-theoretic counterpart.

Where it is used

These definitions give the affine form of Schlessinger's comparison between the fibre square C \times_{C/IC} C and a first-order thickening of \operatorname{Spec}(k \otimes_{T'} C) in the direction V, used to compare two morphisms to a scheme Y agreeing modulo a small ideal with a tangent-vector-valued morphism out of the thickening. The module is imported throughout the deformation-theoretic part of the development.

References

  1. M. Schlessinger, Functors of Artin rings, Transactions of the American Mathematical Society 130 (1968), 208–222
  2. E. Sernesi, Deformations of Algebraic Schemes, Grundlehren der mathematischen Wissenschaften 334, Springer, 2006

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

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib

set_option autoImplicit false
set_option linter.unusedSectionVars false

noncomputable section

universe u

open TensorProduct IsLocalRing CategoryTheory AlgebraicGeometry

namespace AlgebraicGeometry.SmallExtension

variable {T' : Type u} [CommRing T'] [IsLocalRing T'] (I : Ideal T')
  (V : Type u) [AddCommGroup V] [Module (ResidueField T') V] [Module (ResidueField T')ᵐᵒᵖ V]
  [IsCentralScalar (ResidueField T') V] [Module T' V] [IsScalarTower T' (ResidueField T') V]
  (ι : V →ₗ[T'] T')
  (C : Type u) [CommRing C] [Algebra T' C]

def pairRing : Subring (C × C) :=
  RingHom.eqLocus ((Ideal.Quotient.mk (I.map (algebraMap T' C))).comp (RingHom.fst C C))
    ((Ideal.Quotient.mk (I.map (algebraMap T' C))).comp (RingHom.snd C C))

theorem mem_pairRing {x : C × C} :
    x ∈ pairRing I C ↔ Ideal.Quotient.mk (I.map (algebraMap T' C)) x.1 = Ideal.Quotient.mk (I.map (algebraMap T' C)) x.2 :=
  Iff.rfl

def pairFst : pairRing I C →+* C := (RingHom.fst C C).comp (pairRing I C).subtype

def pairSnd : pairRing I C →+* C := (RingHom.snd C C).comp (pairRing I C).subtype

@[simp] theorem pairFst_apply (x : pairRing I C) : pairFst I C x = (x : C × C).1 := rfl
@[simp] theorem pairSnd_apply (x : pairRing I C) : pairSnd I C x = (x : C × C).2 := rfl

variable (T') in

abbrev thickening : Type u := (ResidueField T' ⊗[T'] C) ⊗[ResidueField T'] TrivSqZeroExt (ResidueField T') V

variable (T') in

def toReduction : C →+* ResidueField T' ⊗[T'] C := Algebra.TensorProduct.includeRight.toRingHom

def IsSchlessingerMap (ϑ : pairRing I C →+* thickening T' V C) : Prop :=
  (∀ (a : C) (ha : (a, a) ∈ pairRing I C), ϑ ⟨(a, a), ha⟩ = toReduction T' C a ⊗ₜ (1 : TrivSqZeroExt (ResidueField T') V)) ∧
  (∀ (v : V) (c : C) (h : ((0 : C), algebraMap T' C (ι v) * c) ∈ pairRing I C),
    ϑ ⟨((0 : C), algebraMap T' C (ι v) * c), h⟩ = toReduction T' C c ⊗ₜ TrivSqZeroExt.inr v)

def IsTangentOfPair {Y : Scheme.{u}} (u v : Spec (CommRingCat.of C) ⟶ Y)
    (w : Spec (CommRingCat.of (thickening T' V C)) ⟶ Y) : Prop :=
  ∃ (ϑ : pairRing I C →+* thickening T' V C) (_ : IsSchlessingerMap I V ι C ϑ)
    (φ : Spec (CommRingCat.of (pairRing I C)) ⟶ Y),
    Spec.map (CommRingCat.ofHom (pairFst I C)) ≫ φ = u ∧
    Spec.map (CommRingCat.ofHom (pairSnd I C)) ≫ φ = v ∧
    w = Spec.map (CommRingCat.ofHom ϑ) ≫ φ

end AlgebraicGeometry.SmallExtension

end

Statements phrased using this module (108)