Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_CerednikDrinfeld_FormalUpperHalfPlanePoints.lean

definition module

Adic points and chart loci of the formal upper half-plane

Throughout, \mathcal{O} is a commutative ring with a distinguished element \pi, K a field which is an \mathcal{O}-algebra, and B, R commutative \mathcal{O}-algebras; a Deligne datum d over B assigns to every full lattice M \subset K^2 a submodule d.\mathrm{line}\,M of the base change M \otimes_{\mathcal{O}} B, subject to the conditions packaged in the structure DeligneDatum.

The first group of definitions records pointwise nondegeneracy conditions. DeligneDatum.VertexNondegAt d 𝔭 M says that for every v \in M which is not of the form \pi w with w \in M, the element 1 \otimes v does not lie in d.\mathrm{line}\,M + \mathfrak{p}\cdot(M\otimes_{\mathcal O}B). DeligneDatum.EdgeNondegAt d 𝔭 M' M is the conjunction: M' \subseteq M; \pi M \subseteq M'; for v \in M \setminus M' the element 1 \otimes v avoids d.\mathrm{line}\,M + \mathfrak{p}\cdot\top; and for v' \in M' not in \pi M, 1 \otimes v' avoids d.\mathrm{line}\,M' + \mathfrak{p}\cdot\top. The predicates InVertexChart and InEdgeChart impose these at every prime \mathfrak{p} of B, and exists_edgeNondegAt restates the nondegeneracy field of a Deligne datum: at each prime some pair (M',M) satisfies EdgeNondegAt.

The second group builds adic points. modPow Ο€ R n is R/(\pi^{n+1}), with \mathcal{O}-algebra transition maps to R/(\pi^{n}) and with the image of \pi nilpotent there. An AdicPoint K Ο€ R is a family of Deligne data x_n over R/(\pi^{n+1}) together with the compatibility \mathrm{map}(x_{n+1}) = x_n under the transitions; two adic points agree as soon as their families do. With \mathcal{O}^2 \subset K^2 as stdFullLattice and e_i its standard vectors, \mathrm{coordToTensor}\,n\,w = \sum_i \bar{w_i} \otimes e_i is additive and semilinear for reduction; AdicPoint.stdLine x is the R-submodule of w \in R^2 with \mathrm{coordToTensor}\,n\,w \in x_n.\mathrm{line}(\mathcal{O}^2) for all n. The group \mathrm{GL}_2(K) acts levelwise by pullback along g^{-1}, with x.\mathrm{act}\,1 = x and x.\mathrm{act}(gh) = (x.\mathrm{act}\,h).\mathrm{act}\,g. For a field C that is an R-algebra, lineC is the C-span in C^2 of the image of stdLine, and toOmega x is the unique z \in C with (z,1) \in lineC when such a z exists and is unique, and 0 otherwise; vecCons_toOmega_mem records that under that hypothesis (\mathrm{toOmega}\,x, 1) does lie in lineC.

Finally, for a field K_0 and a valued field C over it, diagFst a is the matrix \mathrm{diag}(a,1) \in \mathrm{GL}_2(K_0) for a unit a, with its action v \mapsto (a v_0, v_1); edgeFlip is \mathrm{diag}(\varpi, 1) for a pseudo-uniformizer \varpi, whose underlying element has positive valuation in C and hence is nonzero, and its image in \mathrm{PGL}_2(K_0) acts on C by z \mapsto \varpi z.

Relation to Mathlib

Mathlib has no notion of Drinfel'd's formal upper half-plane, of Deligne data, or of their adic points; these are the project's own, phrased with Mathlib's tensor products, quotients of ideals and general linear groups.

Where it is used

These notions are the point-level interface of the project's Čerednik–Drinfel'd material: an adic point is a compatible family of Deligne data over the truncations R/(\pi^{n+1}), and toOmega attaches to it a coordinate in a field C, to be compared with the rigid-analytic upper half-plane and with the vertex and edge tubes attached to the Bruhat–Tits tree. The chart loci InVertexChart and InEdgeChart are the conditions used on the formal side of that comparison.

References

  1. J.-F. Boutot and H. Carayol, Uniformisation p-adique des courbes de Shimura: les thΓ©orΓ¨mes de Čerednik et de Drinfel'd, AstΓ©risque 196–197 (1991), 45–158
  2. V. G. Drinfel'd, Coverings of p-adic symmetric domains, Functional Analysis and its Applications 10 (1976), 107–115
  3. D. Mumford, An analytic construction of degenerating curves over complete local rings, Compositio Mathematica 24 (1972), 129–174

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_CerednikDrinfeld_FormalUpperHalfPlaneFunctor
import Definitions.Def_CerednikDrinfeld_OmegaTubes

set_option autoImplicit false

noncomputable section

open scoped TensorProduct MatrixGroups
open LT.LatticeTree TensorProduct Matrix

namespace CerednikDrinfeld
namespace FormalOmega

section ChartLoci

variable {π’ͺ : Type} [CommRing π’ͺ] {K : Type} [Field K] [Algebra π’ͺ K] (Ο€ : π’ͺ)
variable {B : Type} [CommRing B] [Algebra π’ͺ B]

def DeligneDatum.VertexNondegAt (d : DeligneDatum (K := K) Ο€ B) (𝔭 : Ideal B) (M : FullLattice π’ͺ K) : Prop :=
  βˆ€ v : β†₯M.1, (Β¬ βˆƒ w : β†₯M.1, (v : Fin 2 β†’ K) = (algebraMap π’ͺ K Ο€) β€’ (w : Fin 2 β†’ K)) β†’
    (1 : B) βŠ—β‚œ[π’ͺ] v βˆ‰ d.line M βŠ” (𝔭 β€’ ⊀ : Submodule B (latticeBaseChange π’ͺ K B M))

def DeligneDatum.EdgeNondegAt (d : DeligneDatum (K := K) Ο€ B) (𝔭 : Ideal B) (M' M : FullLattice π’ͺ K) : Prop :=
  M'.1 ≀ M.1 ∧ (βˆ€ v : β†₯M.1, (algebraMap π’ͺ K Ο€) β€’ (v : Fin 2 β†’ K) ∈ M'.1) ∧
    (βˆ€ v : β†₯M.1, (v : Fin 2 β†’ K) βˆ‰ M'.1 β†’
      (1 : B) βŠ—β‚œ[π’ͺ] v βˆ‰ d.line M βŠ” (𝔭 β€’ ⊀ : Submodule B (latticeBaseChange π’ͺ K B M))) ∧
    (βˆ€ v' : β†₯M'.1, (Β¬ βˆƒ w : β†₯M.1, (v' : Fin 2 β†’ K) = (algebraMap π’ͺ K Ο€) β€’ (w : Fin 2 β†’ K)) β†’
      (1 : B) βŠ—β‚œ[π’ͺ] v' βˆ‰ d.line M' βŠ” (𝔭 β€’ ⊀ : Submodule B (latticeBaseChange π’ͺ K B M')))

theorem DeligneDatum.exists_edgeNondegAt (d : DeligneDatum (K := K) Ο€ B) (𝔭 : Ideal B) (h𝔭 : 𝔭.IsPrime) :
    βˆƒ M' M : FullLattice π’ͺ K, d.EdgeNondegAt Ο€ 𝔭 M' M := by
  obtain ⟨M', M, h, hΟ€, h1, h2⟩ := d.nondeg 𝔭 h𝔭
  exact ⟨M', M, h, hΟ€, h1, h2⟩

def DeligneDatum.InVertexChart (d : DeligneDatum (K := K) Ο€ B) (M : FullLattice π’ͺ K) : Prop :=
  βˆ€ 𝔭 : Ideal B, 𝔭.IsPrime β†’ d.VertexNondegAt Ο€ 𝔭 M

def DeligneDatum.InEdgeChart (d : DeligneDatum (K := K) Ο€ B) (M' M : FullLattice π’ͺ K) : Prop :=
  βˆ€ 𝔭 : Ideal B, 𝔭.IsPrime β†’ d.EdgeNondegAt Ο€ 𝔭 M' M

end ChartLoci

section AdicPoints

variable {π’ͺ : Type} [CommRing π’ͺ] (K : Type) [Field K] [Algebra π’ͺ K] (Ο€ : π’ͺ)
variable (R : Type) [CommRing R] [Algebra π’ͺ R]

abbrev modPow (n : β„•) : Type := R β§Έ Ideal.span {algebraMap π’ͺ R Ο€ ^ (n + 1)}

theorem span_pow_succ_le (n : β„•) :
    Ideal.span {algebraMap π’ͺ R Ο€ ^ (n + 1 + 1)} ≀ Ideal.span {algebraMap π’ͺ R Ο€ ^ (n + 1)} :=
  Ideal.span_singleton_le_span_singleton.mpr (pow_dvd_pow _ (Nat.le_succ _))

def modPowTransition (n : β„•) : modPow Ο€ R (n + 1) →ₐ[π’ͺ] modPow Ο€ R n :=
  Ideal.Quotient.factorₐ π’ͺ (span_pow_succ_le Ο€ R n)

theorem isNilpotent_algebraMap_modPow (n : β„•) : IsNilpotent (algebraMap π’ͺ (modPow Ο€ R n) Ο€) :=
  ⟨n + 1, by
    rw [← map_pow, IsScalarTower.algebraMap_apply π’ͺ R (modPow Ο€ R n), Ideal.Quotient.algebraMap_eq, map_pow,
      Ideal.Quotient.eq_zero_iff_mem]
    exact Ideal.subset_span (Set.mem_singleton _)⟩

structure AdicPoint : Type where

  pt : βˆ€ n : β„•, OmegaObj (K := K) Ο€ (modPow Ο€ R n)

  compat : βˆ€ n : β„•, DeligneDatum.map Ο€ (modPowTransition Ο€ R n) (pt (n + 1)) = pt n

def stdFullLattice : FullLattice π’ͺ K := ⟨stdLattice π’ͺ K, isFullLattice_stdLattice⟩

def stdBasisVec (i : Fin 2) : β†₯(stdFullLattice (π’ͺ := π’ͺ) K).1 :=
  ⟨Pi.single i 1, single_one_mem_stdLattice π’ͺ K i⟩

def coordToTensor (n : β„•) (w : Fin 2 β†’ R) : latticeBaseChange π’ͺ K (modPow Ο€ R n) (stdFullLattice K) :=
  βˆ‘ i : Fin 2, (Ideal.Quotient.mk (Ideal.span {algebraMap π’ͺ R Ο€ ^ (n + 1)}) (w i)) βŠ—β‚œ[π’ͺ] stdBasisVec K i

theorem coordToTensor_add (n : β„•) (w w' : Fin 2 β†’ R) :
    coordToTensor K Ο€ R n (w + w') = coordToTensor K Ο€ R n w + coordToTensor K Ο€ R n w' := by
  simp only [coordToTensor, Pi.add_apply, map_add, add_tmul, Finset.sum_add_distrib]

theorem coordToTensor_smul (n : β„•) (r : R) (w : Fin 2 β†’ R) :
    coordToTensor K Ο€ R n (r β€’ w) =
      Ideal.Quotient.mk (Ideal.span {algebraMap π’ͺ R Ο€ ^ (n + 1)}) r β€’ coordToTensor K Ο€ R n w := by
  simp only [coordToTensor, Pi.smul_apply, smul_eq_mul, map_mul, Finset.smul_sum, smul_tmul', smul_eq_mul]

theorem coordToTensor_zero (n : β„•) : coordToTensor K Ο€ R n 0 = 0 := by
  simp only [coordToTensor, Pi.zero_apply, map_zero, zero_tmul, Finset.sum_const_zero]

variable {K Ο€ R}

def AdicPoint.stdLine (x : AdicPoint K Ο€ R) : Submodule R (Fin 2 β†’ R) where
  carrier := {w | βˆ€ n : β„•, coordToTensor K Ο€ R n w ∈ (x.pt n).line (stdFullLattice K)}
  zero_mem' n := by rw [coordToTensor_zero]; exact zero_mem _
  add_mem' {w w'} hw hw' n := by rw [coordToTensor_add]; exact add_mem (hw n) (hw' n)
  smul_mem' r {w} hw n := by rw [coordToTensor_smul]; exact Submodule.smul_mem _ _ (hw n)

theorem AdicPoint.mem_stdLine_iff (x : AdicPoint K Ο€ R) (w : Fin 2 β†’ R) :
    w ∈ x.stdLine ↔ βˆ€ n : β„•, coordToTensor K Ο€ R n w ∈ (x.pt n).line (stdFullLattice K) := Iff.rfl

theorem AdicPoint.ext' {x y : AdicPoint K Ο€ R} (h : x.pt = y.pt) : x = y := by
  cases x; cases y; cases h; rfl

def AdicPoint.act (g : GL (Fin 2) K) (x : AdicPoint K Ο€ R) : AdicPoint K Ο€ R where
  pt n := (Omega.action K Ο€).act (modPow Ο€ R n) g (x.pt n)
  compat n := by
    have h := (Omega.action K Ο€).act_map (modPowTransition Ο€ R n) g (x.pt (n + 1))
    change DeligneDatum.map Ο€ (modPowTransition Ο€ R n) ((Omega.action K Ο€).act (modPow Ο€ R (n + 1)) g (x.pt (n + 1))) =
      (Omega.action K Ο€).act (modPow Ο€ R n) g (DeligneDatum.map Ο€ (modPowTransition Ο€ R n) (x.pt (n + 1))) at h
    rw [h, x.compat]

theorem AdicPoint.act_pt (g : GL (Fin 2) K) (x : AdicPoint K Ο€ R) (n : β„•) :
    (x.act g).pt n = DeligneDatum.pullback Ο€ (modPow Ο€ R n) g⁻¹ (x.pt n) := rfl

theorem AdicPoint.act_one (x : AdicPoint K Ο€ R) : x.act 1 = x :=
  AdicPoint.ext' (funext fun n => (Omega.action K Ο€).act_one (modPow Ο€ R n) (x.pt n))

theorem AdicPoint.act_mul (g h : GL (Fin 2) K) (x : AdicPoint K Ο€ R) : x.act (g * h) = (x.act h).act g :=
  AdicPoint.ext' (funext fun n => (Omega.action K Ο€).act_mul (modPow Ο€ R n) g h (x.pt n))

variable (C : Type) [Field C] [Algebra R C]

def AdicPoint.lineC (x : AdicPoint K Ο€ R) : Submodule C (Fin 2 β†’ C) :=
  Submodule.span C ((fun w : Fin 2 β†’ R => fun i => algebraMap R C (w i)) '' (x.stdLine : Set (Fin 2 β†’ R)))

open Classical in

def AdicPoint.toOmega (x : AdicPoint K Ο€ R) : C :=
  if h : βˆƒ! z : C, (![z, 1] : Fin 2 β†’ C) ∈ x.lineC C then Classical.choose h.exists else 0

theorem AdicPoint.vecCons_toOmega_mem (x : AdicPoint K Ο€ R) (h : βˆƒ! z : C, (![z, 1] : Fin 2 β†’ C) ∈ x.lineC C) :
    (![x.toOmega C, 1] : Fin 2 β†’ C) ∈ x.lineC C := by
  classical
  rw [AdicPoint.toOmega, dif_pos h]
  exact (Classical.choose_spec h.exists)

end AdicPoints

section Sigma

variable (Kβ‚€ : Type) [Field Kβ‚€] {C : Type} [Field C] [Algebra Kβ‚€ C]
variable {Ξ“β‚€ : Type} [LinearOrderedCommGroupWithZero Ξ“β‚€] [Valued C Ξ“β‚€]

omit Ξ“β‚€ in

def diagFst (a : Kβ‚€Λ£) : GL (Fin 2) Kβ‚€ :=
  ⟨Matrix.diagonal ![(a : Kβ‚€), 1], Matrix.diagonal ![((a⁻¹ : Kβ‚€Λ£) : Kβ‚€), 1], by
    rw [Matrix.diagonal_mul_diagonal, ← Matrix.diagonal_one]
    congr 1
    funext i
    fin_cases i <;> simp, by
    rw [Matrix.diagonal_mul_diagonal, ← Matrix.diagonal_one]
    congr 1
    funext i
    fin_cases i <;> simp⟩

@[simp] theorem diagFst_coe (a : Kβ‚€Λ£) : ((diagFst Kβ‚€ a : GL (Fin 2) Kβ‚€) : Matrix (Fin 2) (Fin 2) Kβ‚€) = Matrix.diagonal ![(a : Kβ‚€), 1] :=
  rfl

theorem diagFst_mulVec (a : Kβ‚€Λ£) (v : Fin 2 β†’ Kβ‚€) :
    ((diagFst Kβ‚€ a : GL (Fin 2) Kβ‚€) : Matrix (Fin 2) (Fin 2) Kβ‚€) *α΅₯ v = ![(a : Kβ‚€) * v 0, v 1] := by
  rw [diagFst_coe]
  funext i
  rw [Matrix.mulVec_diagonal]
  fin_cases i <;> simp

variable (Ο– : Omega.PseudoUniformizer Kβ‚€ C)

theorem edgeFlip_ne_zero : Ο–.Ο– β‰  0 := by
  intro h
  have := Ο–.pos
  rw [h, map_zero, map_zero] at this
  exact lt_irrefl _ this

def edgeFlip : GL (Fin 2) Kβ‚€ := diagFst Kβ‚€ (Units.mk0 Ο–.Ο– (edgeFlip_ne_zero Kβ‚€ Ο–))

theorem edgeFlip_mulVec (v : Fin 2 β†’ Kβ‚€) :
    ((edgeFlip Kβ‚€ Ο– : GL (Fin 2) Kβ‚€) : Matrix (Fin 2) (Fin 2) Kβ‚€) *α΅₯ v = ![Ο–.Ο– * v 0, v 1] :=
  diagFst_mulVec Kβ‚€ _ v

theorem pmoebius_edgeFlip [DecidableEq C] (z : C) :
    Omega.pmoebius Kβ‚€ (Matrix.ProjGenLinGroup.mk (edgeFlip Kβ‚€ Ο–)) z = algebraMap Kβ‚€ C Ο–.Ο– * z := by
  have h10 : (edgeFlip Kβ‚€ Ο– : GL (Fin 2) Kβ‚€) 1 0 = 0 := by
    show Matrix.diagonal ![Ο–.Ο–, (1 : Kβ‚€)] 1 0 = 0
    simp
  have h11 : (edgeFlip Kβ‚€ Ο– : GL (Fin 2) Kβ‚€) 1 1 = 1 := by
    show Matrix.diagonal ![Ο–.Ο–, (1 : Kβ‚€)] 1 1 = 1
    simp
  have h00 : (edgeFlip Kβ‚€ Ο– : GL (Fin 2) Kβ‚€) 0 0 = Ο–.Ο– := by
    show Matrix.diagonal ![Ο–.Ο–, (1 : Kβ‚€)] 0 0 = Ο–.Ο–
    simp
  have h01 : (edgeFlip Kβ‚€ Ο– : GL (Fin 2) Kβ‚€) 0 1 = 0 := by
    show Matrix.diagonal ![Ο–.Ο–, (1 : Kβ‚€)] 0 1 = 0
    simp
  rw [Omega.pmoebius_mk Kβ‚€ (edgeFlip Kβ‚€ Ο–) z (by rw [h10, h11, map_zero, zero_mul, zero_add, map_one]; exact one_ne_zero),
    Omega.moebius, h10, h11, h00, h01, map_zero, map_one, zero_mul, zero_add, add_zero, div_one]

end Sigma

end FormalOmega
end CerednikDrinfeld

end

Statements phrased using this module (95)