Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_Submodule_LocalBox.lean

definition module

Local components of adelic lattices and embedding sets

Fix a \mathbb{Q}-algebra D (a ring with a \mathbb{Q}-algebra structure) and a height-one prime v of \mathcal{O}_{\mathbb{Q}}, with completion \mathbb{Q}_v = v.adicCompletion ℚ and valuation ring \mathbb{Z}_v = v.adicCompletionIntegers ℚ. Two instances record that \mathbb{Q}_v is a \mathbb{Q}-algebra, hence a \mathbb{Q}-module. Submodule.finiteAdeleEvalAlgHom is the \mathbb{Q}-algebra map \mathbb{A}_{\mathbb{Q}}^f \to \mathbb{Q}_v sending an adèle a to its component a_v (evaluation on the restricted product), and Submodule.finiteAdeleEvalAt is its base change D \otimes_{\mathbb{Q}} \mathbb{A}_{\mathbb{Q}}^f \to D \otimes_{\mathbb{Q}} \mathbb{Q}_v, acting on pure tensors by z \otimes a \mapsto z \otimes a_v.

For a \mathbb{Z}-submodule \Lambda \subseteq D, Submodule.localBox is the additive subgroup of D \otimes_{\mathbb{Q}} \mathbb{Q}_v generated by the pure tensors z \otimes c with z \in \Lambda and c \in \mathbb{Z}_v; Submodule.localBoxUnits is the set (not here a subgroup) of units u of D \otimes_{\mathbb{Q}} \mathbb{Q}_v with both u and u^{-1} in that additive subgroup.

In the quaternionic setting B = \mathbb{H}[\mathbb{Q}, a, b] and \alpha \in B: localQuadSubring is the subring of B \otimes_{\mathbb{Q}} \mathbb{Q}_v generated by \alpha \otimes 1 together with all 1 \otimes r, r \in \mathbb{Q}_v; localQuadUnits is the subgroup of units u with u, u^{-1} in that subring; and localEmbeddingSet \Lambda\,\alpha\,v is the set of units \beta such that for every y in that subring, \beta^{-1} y \beta lies in localBox \Lambda\,v if and only if y does — the local optimality condition at v. Three lemmas restate membership in localBoxUnits, localQuadUnits and localEmbeddingSet, and record the formula for finiteAdeleEvalAt on pure tensors and for evaluation of an adèle.

Relation to Mathlib

Mathlib supplies the finite adèle ring as a restricted product, the v-adic completion and its ring of integers; the local lattice localBox, its unit set, the local quadratic subring and the local optimal-embedding set are the project's own notions, mirroring at a single place the finite-adelic Submodule.finiteAdeleBox, QuaternionAlgebra.finiteAdeleQuadSubring and QuaternionAlgebra.embeddingSetOrd.

Where it is used

These local objects give the place-by-place vocabulary for the local–global analysis of optimal embeddings of quadratic orders into orders in a rational quaternion algebra, so that membership in the finite-adelic box, the adelic torus and the adelic embedding set can be tested one completion at a time; this is what underlies the explicit counts of optimal embeddings in definite quaternion orders used in the trace-formula computations of the project.

References

  1. J. Voight, Quaternion Algebras, Graduate Texts in Mathematics 288, Springer, 2021, §§9.4, 30.3–30.5
  2. 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_Submodule_LocalBox.lean

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_Submodule_FiniteAdeleBox
import Definitions.Def_QuaternionAlgebra_Order_FiniteIdele

set_option autoImplicit false

open scoped TensorProduct Pointwise Quaternion
open IsDedekindDomain NumberField

noncomputable section

namespace IsDedekindDomain.HeightOneSpectrum

instance instAlgebraRatAdicCompletion (v : HeightOneSpectrum (𝓞 ℚ)) : Algebra ℚ (v.adicCompletion ℚ) :=
  HeightOneSpectrum.instAlgebraAdicCompletion (𝓞 ℚ) ℚ v

instance instModuleRatAdicCompletion (v : HeightOneSpectrum (𝓞 ℚ)) : Module ℚ (v.adicCompletion ℚ) :=
  Algebra.toModule

end IsDedekindDomain.HeightOneSpectrum

namespace Submodule

variable {D : Type*} [Ring D] [Algebra ℚ D]

variable (D) in

def finiteAdeleEvalAlgHom (v : HeightOneSpectrum (𝓞 ℚ)) :
    FiniteAdeleRing (𝓞 ℚ) ℚ →ₐ[ℚ] v.adicCompletion ℚ :=
  { RestrictedProduct.evalRingHom
      (fun w : HeightOneSpectrum (𝓞 ℚ) => w.adicCompletion ℚ) v with
    commutes' := fun _ => rfl }

variable (D) in

def finiteAdeleEvalAt (v : HeightOneSpectrum (𝓞 ℚ)) :
    D ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ →ₐ[ℚ] D ⊗[ℚ] v.adicCompletion ℚ :=
  Algebra.TensorProduct.map (AlgHom.id ℚ D) (finiteAdeleEvalAlgHom v)

def localBox (Λ : Submodule ℤ D) (v : HeightOneSpectrum (𝓞 ℚ)) :
    AddSubgroup (D ⊗[ℚ] v.adicCompletion ℚ) :=
  AddSubgroup.closure
    {x | ∃ z ∈ Λ, ∃ c : v.adicCompletion ℚ, c ∈ v.adicCompletionIntegers ℚ ∧ x = z ⊗ₜ[ℚ] c}

def localBoxUnits (Λ : Submodule ℤ D) (v : HeightOneSpectrum (𝓞 ℚ)) :
    Set (D ⊗[ℚ] v.adicCompletion ℚ)ˣ :=
  {u | (u : D ⊗[ℚ] v.adicCompletion ℚ) ∈ (localBox Λ v : Set (D ⊗[ℚ] v.adicCompletion ℚ)) ∧
    ((u⁻¹ : (D ⊗[ℚ] v.adicCompletion ℚ)ˣ) : D ⊗[ℚ] v.adicCompletion ℚ)
      ∈ (localBox Λ v : Set (D ⊗[ℚ] v.adicCompletion ℚ))}

@[simp] theorem finiteAdeleEvalAt_tmul (v : HeightOneSpectrum (𝓞 ℚ)) (z : D)
    (a : FiniteAdeleRing (𝓞 ℚ) ℚ) :
    finiteAdeleEvalAt D v (z ⊗ₜ[ℚ] a) = z ⊗ₜ[ℚ] (a v) := rfl

theorem finiteAdeleEvalAlgHom_apply (v : HeightOneSpectrum (𝓞 ℚ)) (a : FiniteAdeleRing (𝓞 ℚ) ℚ) :
    finiteAdeleEvalAlgHom v a = a v := rfl

theorem mem_localBoxUnits_iff (Λ : Submodule ℤ D) (v : HeightOneSpectrum (𝓞 ℚ))
    (u : (D ⊗[ℚ] v.adicCompletion ℚ)ˣ) :
    u ∈ localBoxUnits Λ v ↔
      (u : D ⊗[ℚ] v.adicCompletion ℚ) ∈ (localBox Λ v : Set (D ⊗[ℚ] v.adicCompletion ℚ)) ∧
        ((u⁻¹ : (D ⊗[ℚ] v.adicCompletion ℚ)ˣ) : D ⊗[ℚ] v.adicCompletion ℚ)
          ∈ (localBox Λ v : Set (D ⊗[ℚ] v.adicCompletion ℚ)) :=
  Iff.rfl

end Submodule

namespace QuaternionAlgebra

variable {a b : ℚ}

def localQuadSubring (α : ℍ[ℚ, a, b]) (v : HeightOneSpectrum (𝓞 ℚ)) :
    Subring (ℍ[ℚ, a, b] ⊗[ℚ] v.adicCompletion ℚ) :=
  Subring.closure
    ({α ⊗ₜ[ℚ] (1 : v.adicCompletion ℚ)} ∪
      Set.range (fun r : v.adicCompletion ℚ => (1 : ℍ[ℚ, a, b]) ⊗ₜ[ℚ] r))

def localQuadUnits (α : ℍ[ℚ, a, b]) (v : HeightOneSpectrum (𝓞 ℚ)) :
    Subgroup (ℍ[ℚ, a, b] ⊗[ℚ] v.adicCompletion ℚ)ˣ where
  carrier := {u | (u : ℍ[ℚ, a, b] ⊗[ℚ] v.adicCompletion ℚ) ∈ localQuadSubring α v ∧
    ((u⁻¹ : (ℍ[ℚ, a, b] ⊗[ℚ] v.adicCompletion ℚ)ˣ) : ℍ[ℚ, a, b] ⊗[ℚ] v.adicCompletion ℚ)
      ∈ localQuadSubring α v}
  one_mem' :=
    ⟨by rw [Units.val_one]; exact (localQuadSubring α v).one_mem,
     by rw [inv_one, Units.val_one]; exact (localQuadSubring α v).one_mem⟩
  mul_mem' := fun {x y} hx hy =>
    ⟨by rw [Units.val_mul]; exact (localQuadSubring α v).mul_mem hx.1 hy.1,
     by rw [mul_inv_rev, Units.val_mul]; exact (localQuadSubring α v).mul_mem hy.2 hx.2⟩
  inv_mem' := fun {x} hx => ⟨hx.2, by rw [inv_inv]; exact hx.1⟩

def localEmbeddingSet (Λ : Submodule ℤ ℍ[ℚ, a, b]) (α : ℍ[ℚ, a, b]) (v : HeightOneSpectrum (𝓞 ℚ)) :
    Set (ℍ[ℚ, a, b] ⊗[ℚ] v.adicCompletion ℚ)ˣ :=
  {β | ∀ y ∈ localQuadSubring α v,
    ((β⁻¹ : (ℍ[ℚ, a, b] ⊗[ℚ] v.adicCompletion ℚ)ˣ) : ℍ[ℚ, a, b] ⊗[ℚ] v.adicCompletion ℚ) * y * β
        ∈ (Submodule.localBox Λ v : Set (ℍ[ℚ, a, b] ⊗[ℚ] v.adicCompletion ℚ))
      ↔ y ∈ (Submodule.localBox Λ v : Set (ℍ[ℚ, a, b] ⊗[ℚ] v.adicCompletion ℚ))}

theorem mem_localQuadUnits_iff (α : ℍ[ℚ, a, b]) (v : HeightOneSpectrum (𝓞 ℚ))
    (u : (ℍ[ℚ, a, b] ⊗[ℚ] v.adicCompletion ℚ)ˣ) :
    u ∈ localQuadUnits α v ↔
      (u : ℍ[ℚ, a, b] ⊗[ℚ] v.adicCompletion ℚ) ∈ localQuadSubring α v ∧
        ((u⁻¹ : (ℍ[ℚ, a, b] ⊗[ℚ] v.adicCompletion ℚ)ˣ) : ℍ[ℚ, a, b] ⊗[ℚ] v.adicCompletion ℚ)
          ∈ localQuadSubring α v :=
  Iff.rfl

theorem mem_localEmbeddingSet_iff (Λ : Submodule ℤ ℍ[ℚ, a, b]) (α : ℍ[ℚ, a, b])
    (v : HeightOneSpectrum (𝓞 ℚ)) (β : (ℍ[ℚ, a, b] ⊗[ℚ] v.adicCompletion ℚ)ˣ) :
    β ∈ localEmbeddingSet Λ α v ↔
      ∀ y ∈ localQuadSubring α v,
        ((β⁻¹ : (ℍ[ℚ, a, b] ⊗[ℚ] v.adicCompletion ℚ)ˣ) : ℍ[ℚ, a, b] ⊗[ℚ] v.adicCompletion ℚ) * y * β
            ∈ (Submodule.localBox Λ v : Set (ℍ[ℚ, a, b] ⊗[ℚ] v.adicCompletion ℚ))
          ↔ y ∈ (Submodule.localBox Λ v : Set (ℍ[ℚ, a, b] ⊗[ℚ] v.adicCompletion ℚ)) :=
  Iff.rfl

end QuaternionAlgebra

end

Statements phrased using this module (173)

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