Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_CerednikDrinfeld_DrinfeldUpperHalfPlane.lean

definition module

Drinfeld upper half-plane and Manin–Drinfeld theta products

For a field extension K_0 \to K the module installs the Möbius action of \mathrm{GL}_2(K_0) on \mathbb P^1(K) = OnePoint K, obtained by pushing matrices forward along algebraMap K₀ K and using Mathlib's action of \mathrm{GL}_2(K) on OnePoint K; since scalar matrices act trivially (scalar_smul_eq), this descends to an action of \mathrm{PGL}_2(K_0) (pglAction, with gl_smul_def, mk_smul_eq recording the two compatibilities). On the affine chart, moebius is the usual expression (az+b)/(cz+d) with entries mapped into K, toAffine retracts OnePoint K to K by sending \infty to 0, and pmoebius is the resulting total function K \to K, z \mapsto toAffine of g \cdot z, for g \in \mathrm{PGL}_2(K_0).

The upper half-plane is defined as the complement of the image of K_0 in K: \Omega = K \setminus \mathrm{algebraMap}(K_0), i.e. the z \in K with \mathrm{algebraMap}\,x \neq z for all x \in K_0 (mem_upperHalfPlane_iff). The accompanying lemmas show that for z \in \Omega the denominator cz+d never vanishes (moebius_denom_ne_zero_of_mem), that \mathrm{PGL}_2(K_0) therefore acts on \Omega by honest fractional linear maps compatibly with the projective action (pmoebius_mk, coe_pmoebius_of_mem), that \Omega is stable (pmoebius_mem_upperHalfPlane), and that pmoebius is unital and multiplicative on \Omega (pmoebius_one, pmoebius_mul).

For a group G and a homomorphism \rho \colon G \to \mathrm{PGL}_2(K_0), crossRatio z z₀ x y is ((z-x)(z_0-y))/((z-y)(z_0-x)); thetaFactor is its value at x = \rho(\gamma)a, y = \rho(\gamma)b, and theta is the unrestricted product \prod'_{\gamma \in G} of these factors, a total function taking the conventional value 1 where the family is not multipliable; ThetaMultipliable names the multipliability of that family. IsAutomorphicWithMultiplier ρ Ω f c asserts f(\rho(\gamma)z) = c(\gamma)f(z) for all \gamma \in G and z \in \Omega, with c \colon G \to K^\times a homomorphism; IsInvariant is the case c = 1. Finally period ρ a z₀ α β is \Theta_\rho(a, \rho(\alpha)a; z_0; \rho(\beta)z_0).

Relation to Mathlib

Mathlib supplies OnePoint, the fractional linear action of \mathrm{GL}_2 on it, and Matrix.ProjGenLinGroup (\mathrm{PGL}_2); the actions here are those pulled back along algebraMap K₀ K, and theta uses Mathlib's unrestricted product ∏'. The non-archimedean upper half-plane and the cross-ratio theta products are the project's own notions.

Where it is used

These definitions underlie the Cherednik–Drinfeld side of the argument, where K is a completed algebraic closure at a place above r and K_0 its subfield of \mathbb Q_r-rational points: \Omega is the space uniformising the relevant Shimura curve, and the theta products with their multipliers provide the periods of the corresponding p-adic Schottky group.

References

  1. Yu. I. Manin and V. G. Drinfeld, Periods of p-adic Schottky groups, J. reine angew. Math. 262/263 (1973), 239–247
  2. L. Gerritzen and M. van der Put, Schottky Groups and Mumford Curves, Lecture Notes in Mathematics 817, Springer, 1980

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

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib

set_option autoImplicit false

open scoped MatrixGroups Topology

namespace CerednikDrinfeld
namespace Omega

section Moebius

variable (K₀ : Type*) [Field K₀] (K : Type*) [Field K] [Algebra K₀ K]

noncomputable scoped instance (priority := low) glAction [DecidableEq K] : MulAction (GL (Fin 2) K₀) (OnePoint K) :=
  MulAction.compHom (OnePoint K) (Matrix.GeneralLinearGroup.map (algebraMap K₀ K))

theorem gl_smul_def [DecidableEq K] (g : GL (Fin 2) K₀) (x : OnePoint K) :
    g • x = (Matrix.GeneralLinearGroup.map (algebraMap K₀ K) g) • x := rfl

theorem scalar_smul_eq [DecidableEq K] (u : K₀ˣ) (x : OnePoint K) :
    (Matrix.GeneralLinearGroup.scalar (Fin 2) u : GL (Fin 2) K₀) • x = x := by
  have h10 : (Matrix.GeneralLinearGroup.map (algebraMap K₀ K)
      (Matrix.GeneralLinearGroup.scalar (Fin 2) u : GL (Fin 2) K₀)) 1 0 = 0 := by
    rw [Matrix.GeneralLinearGroup.map_apply]
    simp [Matrix.GeneralLinearGroup.scalar]
  have h00 : (Matrix.GeneralLinearGroup.map (algebraMap K₀ K)
      (Matrix.GeneralLinearGroup.scalar (Fin 2) u : GL (Fin 2) K₀)) 0 0 = algebraMap K₀ K (u : K₀) := by
    rw [Matrix.GeneralLinearGroup.map_apply]
    simp [Matrix.GeneralLinearGroup.scalar]
  have h11 : (Matrix.GeneralLinearGroup.map (algebraMap K₀ K)
      (Matrix.GeneralLinearGroup.scalar (Fin 2) u : GL (Fin 2) K₀)) 1 1 = algebraMap K₀ K (u : K₀) := by
    rw [Matrix.GeneralLinearGroup.map_apply]
    simp [Matrix.GeneralLinearGroup.scalar]
  have h01 : (Matrix.GeneralLinearGroup.map (algebraMap K₀ K)
      (Matrix.GeneralLinearGroup.scalar (Fin 2) u : GL (Fin 2) K₀)) 0 1 = 0 := by
    rw [Matrix.GeneralLinearGroup.map_apply]
    simp [Matrix.GeneralLinearGroup.scalar]
  have hu : algebraMap K₀ K (u : K₀) ≠ 0 := by
    simp
  induction x using OnePoint.rec with
  | infty => rw [gl_smul_def, OnePoint.smul_infty_eq_ite, if_pos h10]
  | coe k =>
    rw [gl_smul_def, OnePoint.smul_some_eq_ite, h10, h11, h00, h01, zero_mul, zero_add, if_neg hu, add_zero,
      mul_div_cancel_left₀ _ hu]

noncomputable scoped instance (priority := low) pglAction [DecidableEq K] : MulAction PGL(2, K₀) (OnePoint K) :=
  Matrix.ProjGenLinGroup.mulActionOfGL (fun u x => scalar_smul_eq K₀ K u x)

theorem mk_smul_eq [DecidableEq K] (g : GL (Fin 2) K₀) (x : OnePoint K) :
    Matrix.ProjGenLinGroup.mk g • x = g • x :=
  Matrix.ProjGenLinGroup.mk_smul _ g x

def moebius (g : GL (Fin 2) K₀) (z : K) : K :=
  (algebraMap K₀ K (g 0 0) * z + algebraMap K₀ K (g 0 1)) / (algebraMap K₀ K (g 1 0) * z + algebraMap K₀ K (g 1 1))

variable {K} in

def toAffine (x : OnePoint K) : K := OnePoint.elim x 0 id

@[simp] theorem toAffine_coe (z : K) : toAffine (z : OnePoint K) = z := rfl
@[simp] theorem toAffine_infty : toAffine (OnePoint.infty : OnePoint K) = 0 := rfl

variable {K} in

noncomputable def pmoebius [DecidableEq K] (g : PGL(2, K₀)) (z : K) : K := toAffine (g • (z : OnePoint K))

variable {K} in
theorem pmoebius_mk [DecidableEq K] (g : GL (Fin 2) K₀) (z : K)
    (hz : algebraMap K₀ K (g 1 0) * z + algebraMap K₀ K (g 1 1) ≠ 0) :
    pmoebius K₀ (Matrix.ProjGenLinGroup.mk g) z = moebius K₀ K g z := by
  rw [pmoebius, mk_smul_eq, gl_smul_def, OnePoint.smul_some_eq_ite]
  simp only [Matrix.GeneralLinearGroup.map_apply] at *
  rw [if_neg (by simpa using hz)]
  rfl

end Moebius

def upperHalfPlane (K₀ : Type*) [Field K₀] (K : Type*) [Field K] [Algebra K₀ K] : Set K :=
  (Set.range (algebraMap K₀ K))ᶜ

theorem mem_upperHalfPlane_iff (K₀ : Type*) [Field K₀] {K : Type*} [Field K] [Algebra K₀ K] (z : K) :
    z ∈ upperHalfPlane K₀ K ↔ ∀ x : K₀, algebraMap K₀ K x ≠ z := by
  simp [upperHalfPlane]

section OmegaAction

variable (K₀ : Type*) [Field K₀] {K : Type*} [Field K] [Algebra K₀ K]

theorem moebius_denom_ne_zero_of_mem {z : K} (hz : z ∈ upperHalfPlane K₀ K) (g : GL (Fin 2) K₀) :
    algebraMap K₀ K (g 1 0) * z + algebraMap K₀ K (g 1 1) ≠ 0 := by
  rw [mem_upperHalfPlane_iff] at hz
  intro h
  by_cases hc : g 1 0 = 0
  · have hd : g 1 1 ≠ 0 := by
      intro hd
      apply g.det_ne_zero
      rw [Matrix.det_fin_two]
      simp [hc, hd]
    rw [hc, map_zero, zero_mul, zero_add] at h
    exact hd ((algebraMap K₀ K).injective (by rw [h, map_zero]))
  · have hc' : algebraMap K₀ K (g 1 0) ≠ 0 := by
      intro h'; exact hc ((algebraMap K₀ K).injective (by rw [h', map_zero]))
    apply hz (-(g 1 1) / g 1 0)
    rw [map_div₀, map_neg, div_eq_iff hc', eq_comm, ← sub_eq_zero]
    rw [← h]; ring

variable [DecidableEq K]

theorem coe_pmoebius_of_mem {z : K} (hz : z ∈ upperHalfPlane K₀ K) (g : PGL(2, K₀)) :
    ((pmoebius K₀ g z : K) : OnePoint K) = g • (z : OnePoint K) := by
  induction g using Matrix.ProjGenLinGroup.induction_on with
  | _ g =>
    rw [pmoebius, mk_smul_eq, gl_smul_def, OnePoint.smul_some_eq_ite]
    simp only [Matrix.GeneralLinearGroup.map_apply]
    rw [if_neg (moebius_denom_ne_zero_of_mem K₀ hz g)]
    rfl

theorem pmoebius_mem_upperHalfPlane {z : K} (hz : z ∈ upperHalfPlane K₀ K) (g : PGL(2, K₀)) :
    pmoebius K₀ g z ∈ upperHalfPlane K₀ K := by
  induction g using Matrix.ProjGenLinGroup.induction_on with
  | _ g =>
    have hden := moebius_denom_ne_zero_of_mem K₀ hz g
    rw [pmoebius_mk K₀ g z hden, mem_upperHalfPlane_iff]
    rw [mem_upperHalfPlane_iff] at hz
    intro t ht
    rw [moebius, eq_div_iff hden] at ht

    have key : algebraMap K₀ K (g 0 0 - t * g 1 0) * z = algebraMap K₀ K (t * g 1 1 - g 0 1) := by
      rw [map_sub, map_sub, map_mul, map_mul]
      linear_combination -ht
    by_cases h0 : g 0 0 - t * g 1 0 = 0
    · have h1 : t * g 1 1 - g 0 1 = 0 := by
        have := key
        rw [h0, map_zero, zero_mul] at this
        exact ((algebraMap K₀ K).injective (by rw [← this, map_zero])).symm
      apply g.det_ne_zero
      rw [Matrix.det_fin_two]
      have ha : g 0 0 = t * g 1 0 := sub_eq_zero.mp h0
      have hb : g 0 1 = t * g 1 1 := (sub_eq_zero.mp h1).symm
      show g 0 0 * g 1 1 - g 0 1 * g 1 0 = 0
      rw [ha, hb]; ring
    · apply hz ((t * g 1 1 - g 0 1) / (g 0 0 - t * g 1 0))
      have h0' : algebraMap K₀ K (g 0 0 - t * g 1 0) ≠ 0 := by
        intro h'; exact h0 ((algebraMap K₀ K).injective (by rw [h', map_zero]))
      rw [map_div₀, div_eq_iff h0', ← key, mul_comm]

@[simp] theorem pmoebius_one (z : K) : pmoebius K₀ (1 : PGL(2, K₀)) z = z := by
  rw [pmoebius, one_smul, toAffine_coe]

theorem pmoebius_mul {z : K} (hz : z ∈ upperHalfPlane K₀ K) (g h : PGL(2, K₀)) :
    pmoebius K₀ (g * h) z = pmoebius K₀ g (pmoebius K₀ h z) := by
  rw [pmoebius, pmoebius, mul_smul, coe_pmoebius_of_mem K₀ hz h]

end OmegaAction

section Theta

variable {K₀ : Type*} [Field K₀] {K : Type*} [Field K] [Algebra K₀ K] {G : Type*} [Group G]

def crossRatio (z z₀ x y : K) : K := ((z - x) * (z₀ - y)) / ((z - y) * (z₀ - x))

noncomputable def thetaFactor [DecidableEq K] (ρ : G →* PGL(2, K₀)) (a b z₀ z : K) (γ : G) : K :=
  crossRatio z z₀ (pmoebius K₀ (ρ γ) a) (pmoebius K₀ (ρ γ) b)

noncomputable def theta [DecidableEq K] [TopologicalSpace K] (ρ : G →* PGL(2, K₀)) (a b z₀ : K) (z : K) : K :=
  ∏' γ : G, thetaFactor ρ a b z₀ z γ

def ThetaMultipliable [DecidableEq K] [TopologicalSpace K] (ρ : G →* PGL(2, K₀)) (a b z₀ z : K) : Prop :=
  Multipliable (thetaFactor ρ a b z₀ z)

def IsAutomorphicWithMultiplier [DecidableEq K] (ρ : G →* PGL(2, K₀)) (Ω : Set K) (f : K → K) (c : G →* Kˣ) : Prop :=
  ∀ γ : G, ∀ z ∈ Ω, f (pmoebius K₀ (ρ γ) z) = (c γ : K) * f z

def IsInvariant [DecidableEq K] (ρ : G →* PGL(2, K₀)) (Ω : Set K) (f : K → K) : Prop :=
  IsAutomorphicWithMultiplier ρ Ω f 1

noncomputable def period [DecidableEq K] [TopologicalSpace K] (ρ : G →* PGL(2, K₀)) (a z₀ : K) (α β : G) : K :=
  theta ρ a (pmoebius K₀ (ρ α) a) z₀ (pmoebius K₀ (ρ β) z₀)

end Theta

end Omega
end CerednikDrinfeld

Statements phrased using this module (25)