Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_CerednikDrinfeld_FormalUpperHalfPlaneFrame.lean

definition module

Adic frames relating a valued field to the formal upper half-plane

This module introduces the project's predicate CerednikDrinfeld.FormalOmega.IsAdicFrame, a Prop-valued structure carrying no data, which records the compatibility hypotheses needed to compare the functor of Deligne data over \pi-adic rings with the rigid upper half-plane inside a valued field. Its ambient variables are a commutative ring \mathcal{O}, a field K with an \mathcal{O}-algebra structure, a field C with a K-algebra structure and a valuation v taking values in a linearly ordered commutative group with zero, an element \pi \in \mathcal{O}, a pseudo-uniformiser \varpi of K in C (an element of K with 0 < v(\varpi) < 1 whose integral powers bound the value of every nonzero element of K from both sides), and a ring R which is an \mathcal{O}-algebra mapping to C, with the two scalar towers \mathcal{O} \to R \to C and \mathcal{O} \to K \to C. The fields of IsAdicFrame π ϖ R then assert: \pi is irreducible in \mathcal{O}; R \to C is injective; the image of R in C is exactly \{c : v(c) \le 1\}; R is adically complete (in Mathlib's sense, so also separated) for the ideal generated by the image of \pi; the elements of K of value at most 1 are precisely those coming from \mathcal{O}; the image of K is closed in C for the valuation topology; and \pi and \varpi have the same image in C. Three immediate consequences are recorded: v(\pi) < 1 and v(\pi) > 0 in C, both read off from the pseudo-uniformiser via the last field, and v(r) \le 1 for every r in the image of R.

Relation to Mathlib

Mathlib has no notion of such a frame; it is the project's own, assembled from Mathlib's Valued, IsAdicComplete and Irreducible. The topology implicit in the closedness condition is the valuation topology supplied by Valued C Γ₀.

Where it is used

The predicate serves as the common hypothesis for the comparison statements between points of the formal (Deligne-datum) upper half-plane over \pi-adically complete rings and points of the Drinfel'd upper half-plane inside C, together with their \mathrm{GL}_2(K)-equivariance and the dictionary with the vertex and edge tubes indexed by the Bruhat–Tits tree; these underlie the Čerednik–Drinfel'd uniformisation of Shimura curves used in the study of the modular curves occurring in the proof.

References

  1. V. G. Drinfel'd, Coverings of p-adic symmetric domains, Functional Analysis and its Applications 10 (1976), 107–115
  2. 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
  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_FormalUpperHalfPlaneFrame.lean

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_CerednikDrinfeld_FormalUpperHalfPlanePoints

set_option autoImplicit false

open scoped MatrixGroups
open CerednikDrinfeld.Omega

namespace CerednikDrinfeld
namespace FormalOmega

variable {𝒪 : Type} [CommRing 𝒪] {K : Type} [Field K] [Algebra 𝒪 K]
  {C : Type} [Field C] [Algebra K C] {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] [Valued C Γ₀]

structure IsAdicFrame (π : 𝒪) (ϖ : PseudoUniformizer K C) (R : Type) [CommRing R] [Algebra 𝒪 R] [Algebra R C]
    [Algebra 𝒪 C] [IsScalarTower 𝒪 R C] [IsScalarTower 𝒪 K C] : Prop where

  irreducible : Irreducible π

  injective : Function.Injective (algebraMap R C)

  range_eq : ∀ c : C, Valued.v c ≤ 1 ↔ c ∈ Set.range (algebraMap R C)

  complete : IsAdicComplete (Ideal.span {algebraMap 𝒪 R π}) R

  integers : ∀ a : K, Valued.v (algebraMap K C a) ≤ 1 ↔ a ∈ Set.range (algebraMap 𝒪 K)

  isClosed_range : IsClosed (Set.range (algebraMap K C))

  unif : algebraMap 𝒪 C π = algebraMap K C ϖ.ϖ

namespace IsAdicFrame

variable {π : 𝒪} {ϖ : PseudoUniformizer K C} {R : Type} [CommRing R] [Algebra 𝒪 R] [Algebra R C]
  [Algebra 𝒪 C] [IsScalarTower 𝒪 R C] [IsScalarTower 𝒪 K C]

theorem v_algebraMap_lt_one (h : IsAdicFrame π ϖ R) : Valued.v (algebraMap 𝒪 C π) < 1 := by
  rw [h.unif]; exact ϖ.lt_one

theorem v_algebraMap_pos (h : IsAdicFrame π ϖ R) : 0 < Valued.v (algebraMap 𝒪 C π) := by
  rw [h.unif]; exact ϖ.pos

theorem v_algebraMap_le_one (h : IsAdicFrame π ϖ R) (r : R) : Valued.v (algebraMap R C r) ≤ 1 :=
  (h.range_eq _).mpr ⟨r, rfl⟩

end IsAdicFrame

end FormalOmega
end CerednikDrinfeld

Statements phrased using this module (64)