Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_QuaternionAlgebra_Order_FiniteIdele.lean

definition module

Adelic quadratic subring, embedding set and embedding class sets

Throughout, a,b\in\mathbb{Q}, B=\mathbb{H}[\mathbb{Q},a,b] is the corresponding quaternion algebra, and the ambient ring is B\otimes_{\mathbb{Q}}\mathbb{A}, where \mathbb{A} is the finite adele ring of \mathbb{Q}. For an element \alpha\in B, finiteAdeleQuadSubring α is the subring of B\otimes_{\mathbb{Q}}\mathbb{A} generated by \alpha\otimes 1 together with all elements 1\otimes r, r\in\mathbb{A}; for quadratic \alpha this is the adelisation \mathbb{Q}(\alpha)\otimes\mathbb{A}. finiteIdeleQuadUnits α is the subgroup of (B\otimes_{\mathbb{Q}}\mathbb{A})^{\times} consisting of those units whose value and whose inverse's value both lie in that subring, and quadUnitsDiagonal α is its intersection with the image of the diagonal map B^{\times}\to(B\otimes_{\mathbb{Q}}\mathbb{A})^{\times}, d\mapsto d\otimes 1 (the project's Submodule.finiteIdeleDiagonal).

For a \mathbb{Z}-submodule \Lambda\subseteq B, recall that Submodule.finiteAdeleBox Λ is the additive subgroup of B\otimes_{\mathbb{Q}}\mathbb{A} generated by the elementary tensors z\otimes a with z\in\Lambda and a an adele integral at every finite place, and that Submodule.finiteIdeleStabilizer Λ is the stabiliser of this set under the action of (B\otimes_{\mathbb{Q}}\mathbb{A})^{\times}. Then embeddingSetOrd Λ α is the set of units \beta such that for every y in finiteAdeleQuadSubring α one has \beta^{-1}y\beta in the box if and only if y is, i.e. \widehat{K}\cap\beta\widehat{\Lambda}\beta^{-1}=\widehat{K}\cap\widehat{\Lambda}. Finally, IdelicEmbeddingClassSet Λ α is the subtype of the double coset quotient of (B\otimes_{\mathbb{Q}}\mathbb{A})^{\times} by quadUnitsDiagonal α on the left and Submodule.finiteIdeleStabilizer Λ on the right consisting of those classes admitting a representative in embeddingSetOrd Λ α; and EmbeddingClassFibre Λ α β is the subtype of the same quotient consisting of classes with a representative x in the embedding set whose double coset for the full diagonal image of B^{\times} and Submodule.finiteIdeleStabilizer Λ coincides with that of \beta, i.e. the fibre over the class of \beta of the natural map to B^{\times}\backslash(B\otimes\mathbb{A})^{\times}/\widehat{\Lambda}^{\times}. All six definitions are made for an arbitrary element \alpha and an arbitrary \mathbb{Z}-submodule \Lambda; no quadraticity or order condition is built in. Everything is purely algebraic: no topology and no choice of basis or of local splittings enters.

Relation to Mathlib

Mathlib provides the finite adele ring, subring closures, unit groups and double coset quotients; the adelic quadratic subring, its unit groups, the embedding set and the two class-set subtypes are the project's own notions, built on these together with the project's Submodule.finiteAdeleBox, Submodule.finiteIdeleStabilizer and Submodule.finiteIdeleDiagonal.

Where it is used

These objects give the idelic, double-coset formulation of optimal embeddings of quadratic orders into an order \Lambda of a rational quaternion algebra, the form in which embedding numbers are counted and compared with class numbers in the project's development of quaternionic orders.

References

  1. J. Voight, Quaternion Algebras, Graduate Texts in Mathematics 288, Springer, 2021, Chapter 30
  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_QuaternionAlgebra_Order_FiniteIdele.lean

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_Submodule_FiniteAdeleBox
import Definitions.Def_QuaternionAlgebra_Order

set_option autoImplicit false

open scoped TensorProduct Pointwise Quaternion
open IsDedekindDomain NumberField

noncomputable section

namespace QuaternionAlgebra

variable {a b : ℚ}

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

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

def quadUnitsDiagonal (α : ℍ[ℚ, a, b]) : Subgroup (ℍ[ℚ, a, b] ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)ˣ :=
  (Submodule.finiteIdeleDiagonal ℍ[ℚ, a, b]).range ⊓ finiteIdeleQuadUnits α

def embeddingSetOrd (Λ : Submodule ℤ ℍ[ℚ, a, b]) (α : ℍ[ℚ, a, b]) :
    Set (ℍ[ℚ, a, b] ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)ˣ :=
  {β | ∀ y ∈ finiteAdeleQuadSubring α,
    ((β⁻¹ : (ℍ[ℚ, a, b] ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)ˣ) : ℍ[ℚ, a, b] ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ) * y * β
        ∈ (Submodule.finiteAdeleBox Λ : Set (ℍ[ℚ, a, b] ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ))
      ↔ y ∈ (Submodule.finiteAdeleBox Λ : Set (ℍ[ℚ, a, b] ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ))}

def IdelicEmbeddingClassSet (Λ : Submodule ℤ ℍ[ℚ, a, b]) (α : ℍ[ℚ, a, b]) : Type :=
  {q : DoubleCoset.Quotient
      ((quadUnitsDiagonal α : Subgroup (ℍ[ℚ, a, b] ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)ˣ) : Set (ℍ[ℚ, a, b] ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)ˣ)
      ((Submodule.finiteIdeleStabilizer Λ : Subgroup (ℍ[ℚ, a, b] ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)ˣ) : Set (ℍ[ℚ, a, b] ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)ˣ) //
    ∃ x ∈ embeddingSetOrd Λ α,
      DoubleCoset.mk (quadUnitsDiagonal α) (Submodule.finiteIdeleStabilizer Λ) x = q}

def EmbeddingClassFibre (Λ : Submodule ℤ ℍ[ℚ, a, b]) (α : ℍ[ℚ, a, b])
    (β : (ℍ[ℚ, a, b] ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)ˣ) : Type :=
  {q : DoubleCoset.Quotient
      ((quadUnitsDiagonal α : Subgroup (ℍ[ℚ, a, b] ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)ˣ) : Set (ℍ[ℚ, a, b] ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)ˣ)
      ((Submodule.finiteIdeleStabilizer Λ : Subgroup (ℍ[ℚ, a, b] ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)ˣ) : Set (ℍ[ℚ, a, b] ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)ˣ) //
    ∃ x ∈ embeddingSetOrd Λ α,
      DoubleCoset.mk (quadUnitsDiagonal α) (Submodule.finiteIdeleStabilizer Λ) x = q ∧
      (DoubleCoset.mk (Submodule.finiteIdeleDiagonal ℍ[ℚ, a, b]).range
          (Submodule.finiteIdeleStabilizer Λ) x :
        DoubleCoset.Quotient
          (((Submodule.finiteIdeleDiagonal ℍ[ℚ, a, b]).range : Subgroup (ℍ[ℚ, a, b] ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)ˣ) : Set (ℍ[ℚ, a, b] ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)ˣ)
          ((Submodule.finiteIdeleStabilizer Λ : Subgroup (ℍ[ℚ, a, b] ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)ˣ) : Set (ℍ[ℚ, a, b] ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)ˣ))
        = DoubleCoset.mk (Submodule.finiteIdeleDiagonal ℍ[ℚ, a, b]).range
          (Submodule.finiteIdeleStabilizer Λ) β}

end QuaternionAlgebra

end

Statements phrased using this module (3)