Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_CerednikDrinfeld_CosetGraphAtPrime.lean

definition module

Coset graph of a quaternionic order at one place

Fix rationals a,b and work with the quaternion algebra \mathbb H=\mathbb H[\mathbb Q,a,b]. For a finite place v of \mathbb Q, Loc a b v is the base change \mathbb H\otimes_{\mathbb Q}\mathbb Q_v, where \mathbb Q_v is the v-adic completion; toLoc v is the induced map on unit groups \mathbb H^\times\to(\mathbb H\otimes\mathbb Q_v)^\times coming from x\mapsto x\otimes 1, and scalarUnits v is the image of (\mathbb Q_v)^\times under c\mapsto 1\otimes c. Given a \mathbb Z-submodule R\subseteq\mathbb H, level R v is the subgroup of (\mathbb H\otimes\mathbb Q_v)^\times generated by scalarUnits v together with the set Submodule.localBoxUnits R v of units u for which both u and u^{-1} lie in the additive group generated by the elements z\otimes c with z\in R and c in the valuation ring of \mathbb Q_v. The vertex set Vert R v is the coset space (\mathbb H\otimes\mathbb Q_v)^\times/\,level R v. For a chosen n_v\in(\mathbb H\otimes\mathbb Q_v)^\times, graph R v nv is the simple graph on Vert R v in which distinct classes x,y are adjacent exactly when, in one of the two orders, x=[g] and y=[gkn_v] for some g and some k in level R v; symmetry and looplessness are carried as fields.

The group awayUnits R v is the subgroup of \mathbb H^\times of those \gamma whose image under toLoc w lies in the subgroup generated by Submodule.localBoxUnits R w, for every finite place w\neq v. Left translation through toLoc v makes \mathbb H^\times, and hence awayUnits R v, act on Vert R v; actionKer R v is the kernel of the resulting permutation representation, a normal subgroup, and ProjAwayUnits R v is the quotient, which therefore acts faithfully on Vert R v. Two compatibility lemmas identify the actions on representatives, and the final instance records that ProjAwayUnits R v preserves adjacency, i.e. satisfies the project's class CerednikDrinfeld.Mumford.GraphAction for graph R v nv.

Relation to Mathlib

Built on Mathlib's quaternion algebras, adic completions at height-one primes, unit groups, group quotients and SimpleGraph; Mathlib has no Bruhat–Tits tree or quaternionic coset graph, and the adjacency-preservation class GraphAction is the project's own.

Where it is used

These are the combinatorial data on which the Čerednik–Drinfeld side of the argument is organised: for R_v a maximal order at v and n_v in the normaliser of an Iwahori subgroup, graph R v nv plays the role of the Bruhat–Tits tree of \mathbb{Q}_v and ProjAwayUnits R v the role of the image of the v-away unit group in \mathrm{PGL}_2(\mathbb{Q}_v). The quotient of darts and vertices by this action supplies the degeneracy datum feeding the Mumford period construction and its comparison with quaternionic class sets.

References

  1. J.-P. Serre, Trees, Springer, 1980
  2. 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
  3. M. F. Vignéras, Arithmétique des algèbres de quaternions, Lecture Notes in Mathematics 800, 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_CosetGraphAtPrime.lean

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_Submodule_LocalBox
import Definitions.Def_CerednikDrinfeld_MumfordPeriod

set_option autoImplicit false

open scoped TensorProduct Quaternion
open IsDedekindDomain NumberField

noncomputable section

namespace CerednikDrinfeld.CosetGraph

variable {a b : ℚ}

abbrev Loc (a b : ℚ) (v : HeightOneSpectrum (𝓞 ℚ)) : Type := ℍ[ℚ, a, b] ⊗[ℚ] v.adicCompletion ℚ

def toLoc (v : HeightOneSpectrum (𝓞 ℚ)) : (ℍ[ℚ, a, b])ˣ →* (Loc a b v)ˣ :=
  Units.map (Algebra.TensorProduct.includeLeft : ℍ[ℚ, a, b] →ₐ[ℚ] Loc a b v).toRingHom.toMonoidHom

def scalarUnits (v : HeightOneSpectrum (𝓞 ℚ)) : Subgroup (Loc a b v)ˣ :=
  (Units.map (Algebra.TensorProduct.includeRight : v.adicCompletion ℚ →ₐ[ℚ] Loc a b v).toRingHom.toMonoidHom).range

def level (R : Submodule ℤ ℍ[ℚ, a, b]) (v : HeightOneSpectrum (𝓞 ℚ)) : Subgroup (Loc a b v)ˣ :=
  Subgroup.closure (Submodule.localBoxUnits R v) ⊔ scalarUnits v

abbrev Vert (R : Submodule ℤ ℍ[ℚ, a, b]) (v : HeightOneSpectrum (𝓞 ℚ)) : Type := (Loc a b v)ˣ ⧸ level R v

def graph (R : Submodule ℤ ℍ[ℚ, a, b]) (v : HeightOneSpectrum (𝓞 ℚ)) (nv : (Loc a b v)ˣ) : SimpleGraph (Vert R v) where
  Adj x y := x ≠ y ∧ ∃ g : (Loc a b v)ˣ, ∃ k ∈ level R v,
    (x = (g : Vert R v) ∧ y = ((g * k * nv : (Loc a b v)ˣ) : Vert R v)) ∨
      (y = (g : Vert R v) ∧ x = ((g * k * nv : (Loc a b v)ˣ) : Vert R v))
  symm := ⟨by
    rintro x y ⟨hne, g, k, hk, h⟩
    exact ⟨hne.symm, g, k, hk, h.symm⟩⟩
  loopless := ⟨fun _ h => h.1 rfl⟩

def awayUnits (R : Submodule ℤ ℍ[ℚ, a, b]) (v : HeightOneSpectrum (𝓞 ℚ)) : Subgroup (ℍ[ℚ, a, b])ˣ :=
  ⨅ (w : HeightOneSpectrum (𝓞 ℚ)) (_ : w ≠ v), (Subgroup.closure (Submodule.localBoxUnits R w)).comap (toLoc w)

instance vertMulAction (R : Submodule ℤ ℍ[ℚ, a, b]) (v : HeightOneSpectrum (𝓞 ℚ)) :
    MulAction (ℍ[ℚ, a, b])ˣ (Vert R v) :=
  MulAction.compHom (Vert R v) (toLoc (a := a) (b := b) v)

theorem smul_vert_mk (R : Submodule ℤ ℍ[ℚ, a, b]) (v : HeightOneSpectrum (𝓞 ℚ)) (γ : (ℍ[ℚ, a, b])ˣ) (g : (Loc a b v)ˣ) :
    γ • ((g : (Loc a b v)ˣ) : Vert R v) = ((toLoc v γ * g : (Loc a b v)ˣ) : Vert R v) := rfl

instance awayVertMulAction (R : Submodule ℤ ℍ[ℚ, a, b]) (v : HeightOneSpectrum (𝓞 ℚ)) :
    MulAction (awayUnits R v) (Vert R v) := inferInstance

def actionKer (R : Submodule ℤ ℍ[ℚ, a, b]) (v : HeightOneSpectrum (𝓞 ℚ)) : Subgroup (awayUnits R v) :=
  (MulAction.toPermHom (awayUnits R v) (Vert R v)).ker

instance actionKer_normal (R : Submodule ℤ ℍ[ℚ, a, b]) (v : HeightOneSpectrum (𝓞 ℚ)) : (actionKer R v).Normal :=
  MonoidHom.normal_ker _

abbrev ProjAwayUnits (R : Submodule ℤ ℍ[ℚ, a, b]) (v : HeightOneSpectrum (𝓞 ℚ)) : Type :=
  (awayUnits R v) ⧸ actionKer R v

instance projVertMulAction (R : Submodule ℤ ℍ[ℚ, a, b]) (v : HeightOneSpectrum (𝓞 ℚ)) :
    MulAction (ProjAwayUnits R v) (Vert R v) :=
  MulAction.compHom (Vert R v) (QuotientGroup.kerLift (MulAction.toPermHom (awayUnits R v) (Vert R v)))

theorem mk_smul_vert (R : Submodule ℤ ℍ[ℚ, a, b]) (v : HeightOneSpectrum (𝓞 ℚ)) (γ : awayUnits R v) (x : Vert R v) :
    (QuotientGroup.mk γ : ProjAwayUnits R v) • x = γ • x := rfl

theorem coe_smul_vert_mk (R : Submodule ℤ ℍ[ℚ, a, b]) (v : HeightOneSpectrum (𝓞 ℚ)) (γ : awayUnits R v)
    (g : (Loc a b v)ˣ) :
    γ • ((g : (Loc a b v)ˣ) : Vert R v) = ((toLoc v (γ : (ℍ[ℚ, a, b])ˣ) * g : (Loc a b v)ˣ) : Vert R v) := rfl

instance projGraphAction (R : Submodule ℤ ℍ[ℚ, a, b]) (v : HeightOneSpectrum (𝓞 ℚ)) (nv : (Loc a b v)ˣ) :
    Mumford.GraphAction (ProjAwayUnits R v) (graph R v nv) where
  smul_adj := by
    intro q x y hxy
    induction q using QuotientGroup.induction_on with
    | H γ =>
      rw [mk_smul_vert, mk_smul_vert]
      obtain ⟨hne, g, k, hk, h⟩ := hxy
      refine ⟨fun e => hne (smul_left_cancel γ e), toLoc v (γ : (ℍ[ℚ, a, b])ˣ) * g, k, hk, ?_⟩
      rcases h with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩
      · left; exact ⟨coe_smul_vert_mk R v γ g, by rw [coe_smul_vert_mk, mul_assoc, mul_assoc, mul_assoc]⟩
      · right; exact ⟨coe_smul_vert_mk R v γ g, by rw [coe_smul_vert_mk, mul_assoc, mul_assoc, mul_assoc]⟩

end CerednikDrinfeld.CosetGraph

end

Statements phrased using this module (312)

… and 162 more statements (search for the module name to find them).