Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AlgebraicCurve_RelCartier.lean

definition module

Invertible ideal sheaves, Cartier relative divisors, base change of ideal homomorphisms

For a scheme X, an ideal sheaf datum I is declared IsInvertible when every point x of X admits an affine open U and a section f \in \Gamma(X,U) with x \in D(f) such that, on the affine open D(f), the ideal I(D(f)) is the span of a single element g of \Gamma(X,D(f)) which is a non-zero-divisor. Thus local principality alone is not enough: the generator is required to be a non-zero-divisor, so the zero ideal sheaf on a non-empty scheme fails the condition. Two closure properties are recorded: the unit ideal sheaf \top is invertible, and the product of two invertible ideal sheaf data is invertible (a common basic affine open is found on which the product is generated by the product of the two generators, again a non-zero-divisor by localisation).

For a morphism f \colon X' \to X and affine opens U \subseteq X, U' \subseteq f^{-1}(U), the restriction-along-f map f.appLE carries I(U) into (I \text{ comap } f)(U'); this is appLE_mem_comap_ideal. With it, IsBaseChangeAlong is the predicate on a pair consisting of \varphi \colon I \to J and \varphi' \colon f^{*}I \to f^{*}J (homomorphisms of ideal sheaf data in the project's sense, given by compatible \Gamma(X,U)-linear maps on sections) asserting that for all such U, U' and all x \in I(U) the section \varphi'_{U'} applied to the pull-back of x equals the pull-back of \varphi_U(x). It is a compatibility relation between two given homomorphisms, not a construction of \varphi'.

Over a field k: a relative effective divisor Z of degree d in C \times_k T is IsCartier when its ideal sheaf datum Z.I is invertible. Given D of degree r over the base \operatorname{Spec} k itself (with structure map the identity), const is its pull-back along t \colon T \to \operatorname{Spec} k, the constant family of degree r over T. Finally, \varphi \colon I \to J on C \times_k T is FibrewiseNonvanishing when for every point s of T there exists a homomorphism \varphi' on the fibre C \times_k \kappa(s) which is a base change of \varphi along the induced map and is non-zero.

Relation to Mathlib

Mathlib supplies Scheme.IdealSheafData together with comap and the associated closed subscheme; invertibility of such a datum, homomorphisms between ideal sheaf data, the base-change relation between them, and relative effective divisors on a curve are the project's own notions.

Where it is used

These predicates are part of the theory of relative effective divisors on a curve over a field and of their universal families, the geometric input for the moduli constructions (and the associated Hecke-theoretic geometry) used in the modularity 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_AlgebraicCurve_RelCartier.lean

Imports

Imported by

Declarations

Source

import Definitions.Def_AlgebraicGeometry_IdealSheafHom
import Definitions.Def_AlgebraicCurve_UniversalDivisor

open CategoryTheory CategoryTheory.Limits TopologicalSpace Opposite

universe u

namespace AlgebraicGeometry.Scheme.IdealSheafData

variable {X : Scheme.{u}}

def IsInvertible (I : X.IdealSheafData) : Prop :=
  ∀ x : X, ∃ (U : X.affineOpens) (f : Γ(X, U)), x ∈ X.basicOpen f ∧
    ∃ g ∈ nonZeroDivisors Γ(X, X.affineBasicOpen f), I.ideal (X.affineBasicOpen f) = Ideal.span {g}

theorem isInvertible_top : (⊤ : X.IdealSheafData).IsInvertible := by
  intro x
  obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
    X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ
  refine ⟨⟨U, hU⟩, 1, by simpa using hxU, 1, one_mem _, ?_⟩
  rw [ideal_top, Pi.top_apply, Ideal.span_singleton_one]

theorem IsInvertible.mul {I J : X.IdealSheafData} (hI : I.IsInvertible) (hJ : J.IsInvertible) :
    (I * J).IsInvertible := by
  intro x
  obtain ⟨U, f, hxf, g, hg, hIg⟩ := hI x
  obtain ⟨U', f', hxf', g', hg', hJg⟩ := hJ x

  obtain ⟨h, h', hhh', hxh⟩ := exists_basicOpen_le_affine_inter (X.affineBasicOpen f).2
    (X.affineBasicOpen f').2 x ⟨hxf, hxf'⟩
  have hW : (X.affineBasicOpen h : X.Opens) ≤ X.affineBasicOpen f := X.basicOpen_le h
  have hW' : (X.affineBasicOpen h : X.Opens) ≤ X.affineBasicOpen f' :=
    hhh'.trans_le (X.basicOpen_le h')
  refine ⟨X.affineBasicOpen f, h, hxh, ((X.presheaf.map (homOfLE hW).op).hom g :
    Γ(X, X.affineBasicOpen h)) * (X.presheaf.map (homOfLE hW').op).hom g', mul_mem ?_ ?_, ?_⟩
  ·
    letI := (X.affineBasicOpen f).2.isLocalization_basicOpen h
    exact IsLocalization.nonZeroDivisors_le_comap (M := .powers h)
      (S := Γ(X, X.basicOpen h)) hg
  ·
    letI := (X.presheaf.map (homOfLE hW').op).hom.toAlgebra
    haveI := (X.affineBasicOpen f').2.isLocalization_of_eq_basicOpen h' (homOfLE hW') hhh'
    exact IsLocalization.nonZeroDivisors_le_comap (M := .powers h')
      (S := Γ(X, X.affineBasicOpen h)) hg'
  · rw [ideal_mul, Pi.mul_apply,
      ← I.map_ideal (U := X.affineBasicOpen h) (V := X.affineBasicOpen f) hW, hIg,
      ← J.map_ideal (U := X.affineBasicOpen h) (V := X.affineBasicOpen f') hW', hJg,
      Ideal.map_span, Set.image_singleton, Ideal.map_span, Set.image_singleton,
      Ideal.span_singleton_mul_span_singleton]
    rfl

namespace IdealHom

variable {X' : Scheme.{u}} (f : X' ⟶ X) {I J : X.IdealSheafData}

theorem appLE_mem_comap_ideal (U : X.affineOpens) (U' : X'.affineOpens)
    (h : (U' : X'.Opens) ≤ f ⁻¹ᵁ U) (x : I.ideal U) :
    f.appLE U U' h x ∈ (I.comap f).ideal U' := by

  have hx : (x : Γ(X, U)) ∈ ((I.comap f).map f).ideal U := (le_def.mp (I.le_map_comap f)) U x.2
  have h0 : ((I.comap f).subschemeι ≫ f).app U x = 0 :=
    RingHom.mem_ker.mp (Scheme.Hom.ideal_ker_le _ U hx)

  have key : (I.comap f).ideal U' = RingHom.ker ((I.comap f).subschemeι.app U').hom := by
    conv_lhs => rw [← (I.comap f).ker_subschemeι]
    exact Scheme.Hom.ker_apply _ U'
  rw [key, RingHom.mem_ker, Scheme.Hom.appLE, CommRingCat.comp_apply, ← CommRingCat.comp_apply,
    Scheme.Hom.naturality, CommRingCat.comp_apply]
  have h0' : (I.comap f).subschemeι.app (f ⁻¹ᵁ U) (f.app U x) = 0 := h0
  rw [h0', map_zero]

def IsBaseChangeAlong (φ : IdealHom I J) (φ' : IdealHom (I.comap f) (J.comap f)) : Prop :=
  ∀ (U : X.affineOpens) (U' : X'.affineOpens) (h : (U' : X'.Opens) ≤ f ⁻¹ᵁ U) (x : I.ideal U),
    (φ'.app U' ⟨f.appLE U U' h x, appLE_mem_comap_ideal f U U' h x⟩ : Γ(X', U')) =
      f.appLE U U' h (φ.app U x)

end IdealHom

end AlgebraicGeometry.Scheme.IdealSheafData

namespace AlgebraicCurve

open AlgebraicGeometry Scheme.IdealSheafData

variable {k : Type u} [Field k] {C : Scheme.{u}} {c : C ⟶ Spec (.of k)}

def RelEffDivisor.IsCartier {d : ℕ} {T : Scheme.{u}} {t : T ⟶ Spec (.of k)}
    (Z : RelEffDivisor C c d T t) : Prop :=
  Z.I.IsInvertible

noncomputable def RelEffDivisor.const {r : ℕ}
    (D : RelEffDivisor C c r (Spec (.of k)) (𝟙 _)) {T : Scheme.{u}} (t : T ⟶ Spec (.of k)) :
    RelEffDivisor C c r T t :=
  D.pullbackAlong t (Category.comp_id t)

def IdealHom.FibrewiseNonvanishing (c : C ⟶ Spec (.of k)) {T : Scheme.{u}}
    (t : T ⟶ Spec (.of k)) {I J : (pullback c t).IdealSheafData} (φ : IdealHom I J) : Prop :=
  ∀ s : T, ∃ φ' : IdealHom (I.comap (mapOnProd c (T.fromSpecResidueField s) rfl))
      (J.comap (mapOnProd c (T.fromSpecResidueField s) rfl)),
    φ.IsBaseChangeAlong (mapOnProd c (T.fromSpecResidueField s) rfl) φ' ∧ φ' ≠ 0

end AlgebraicCurve

Statements phrased using this module (111)