Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_CerednikDrinfeld_DiscreteProjectiveAction.lean

definition module

Valuative discreteness of a representation into

The module introduces a single predicate, CerednikDrinfeld.Omega.IsDiscrete, formulated for a field K_0, an extension field K of K_0 (an algebra over K_0) carrying a valuation v with values in a linearly ordered commutative group with zero \Gamma_0, a group G, and a homomorphism \rho \colon G \to \mathrm{PGL}_2(K_0). The predicate asserts: for every \varepsilon \in \Gamma_0 with \varepsilon \neq 0, the set of those \gamma \in G for which there exists g \in \mathrm{GL}_2(K_0) with

[g] = \rho(\gamma) in \mathrm{PGL}_2(K_0), v(g_{ij}) \le 1 for all i,j, and v(\det g) \ge \varepsilon,

is finite. Here the entries and the determinant of g, which lie in K_0, are transported into K along the structure map K_0 \to K before v is applied, and [g] denotes the image of g under the projection \mathrm{GL}_2(K_0) \to \mathrm{PGL}_2(K_0). Thus discreteness is expressed entirely through the valuation of K: an element of G is counted when its image admits an integral representative matrix whose determinant is not too small in valuation, and for each fixed bound only finitely many elements of G are counted. No topology on G, on K_0 or on \mathrm{PGL}_2(K_0) enters, and the condition is imposed on \rho itself, so it simultaneously constrains the kernel of \rho and the image. The extension field K together with its valuation is an explicit argument of the predicate.

Relation to Mathlib

Built on Mathlib's Valued, GL (Fin 2) K₀ and the projective linear group PGL(2, K₀) with its quotient map Matrix.ProjGenLinGroup.mk; the discreteness condition itself, stated by valuations of integral representatives rather than by a group topology, is the project's own notion.

Where it is used

The predicate is the standing hypothesis on \rho in the development of the Drinfeld upper half-plane K \setminus K_0 with its Möbius action of \mathrm{PGL}_2(K_0), where it controls the infinite products CerednikDrinfeld.Omega.theta built from cross-ratio factors and hence the automorphy properties of the resulting functions.

References

  1. L. Gerritzen and M. van der Put, Schottky Groups and Mumford Curves, Lecture Notes in Mathematics 817, Springer, 1980
  2. V. G. Drinfeld, Coverings of p-adic symmetric domains, Functional Analysis and its Applications 10 (1976), 107–115
  3. J.-F. Boutot and H. Carayol, Uniformisation p-adique des courbes de Shimura: les théorèmes de Čerednik et de Drinfeld, Astérisque 196–197 (1991), 45–158

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_CerednikDrinfeld_DrinfeldUpperHalfPlane

set_option autoImplicit false

open scoped MatrixGroups

namespace CerednikDrinfeld
namespace Omega

def IsDiscrete {K₀ : Type*} [Field K₀] (K : Type*) [Field K] [Algebra K₀ K]
    {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀]
    {G : Type*} [Group G] (ρ : G →* PGL(2, K₀)) : Prop :=
  ∀ ε : Γ₀, ε ≠ 0 →
    {γ : G | ∃ g : GL (Fin 2) K₀, Matrix.ProjGenLinGroup.mk g = ρ γ ∧
      (∀ i j : Fin 2, Valued.v (algebraMap K₀ K (g i j)) ≤ 1) ∧
      ε ≤ Valued.v (algebraMap K₀ K (Matrix.det (g : Matrix (Fin 2) (Fin 2) K₀)))}.Finite

end Omega
end CerednikDrinfeld

Statements phrased using this module (39)