Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_Submodule_FiniteAdeleBox.lean

definition module

Finite adelic box of a lattice; idelic translates and stabiliser

Throughout, D is a ring equipped with a \mathbb{Q}-algebra structure (not assumed commutative), \Lambda is a \mathbb{Z}-submodule of D, and \widehat{D} = D \otimes_{\mathbb{Q}} \mathbb{A} with \mathbb{A} Mathlib's finite adele ring FiniteAdeleRing (π“ž β„š) β„š of \mathbb{Q}. Five constructions are made. Submodule.finiteAdeleBox Ξ› is the additive subgroup of \widehat{D} generated by the pure tensors z \otimes a with z \in \Lambda and a a finite adele that is integral at every place, i.e. a_v lies in v.adicCompletionIntegers β„š for every v in the height-one spectrum of \mathbb{Z}; write \widehat{\Lambda} for it. Submodule.ofFiniteIdele Ξ› g, for a unit g of \widehat{D}, is the \mathbb{Z}-submodule of D obtained by pulling back the image of \widehat{\Lambda} under left multiplication by g along z \mapsto z \otimes 1; thus its elements are exactly those z \in D with z \otimes 1 \in g\widehat{\Lambda}. Submodule.conjByFiniteIdele Ξ› g is the analogous pullback for the two-sided translate, left multiplication by g followed by right multiplication by g^{-1}: its elements are the z \in D with z \otimes 1 \in g\widehat{\Lambda}g^{-1}. Submodule.finiteIdeleStabilizer Ξ› is the stabiliser, inside \widehat{D}^{\times} acting by multiplication on subsets of \widehat{D}, of the underlying set of \widehat{\Lambda}, so a unit u belongs to it precisely when u \cdot \widehat{\Lambda} = \widehat{\Lambda} as sets. Submodule.finiteIdeleDiagonal D is the group homomorphism D^{\times} \to \widehat{D}^{\times} induced by z \mapsto z \otimes 1. Four further results record these descriptions: the value of the diagonal map on a unit d is d \otimes 1, and the membership criteria for ofFiniteIdele, conjByFiniteIdele and finiteIdeleStabilizer are stated as the stated equivalences, each holding by definition. No topology on \widehat{D} enters; everything here is a purely algebraic construction.

Relation to Mathlib

Mathlib supplies the finite adele ring of a Dedekind domain with its fraction field and the local integers HeightOneSpectrum.adicCompletionIntegers; the adelic completion \widehat{\Lambda} of a \mathbb{Z}-submodule of a \mathbb{Q}-algebra, its idelic translates, the associated stabiliser and the diagonal embedding of units are the project's own definitions, placed in the Submodule namespace.

Where it is used

These are the lattice-theoretic underpinnings of the adelic description of orders and right ideals in a quaternion algebra: for \Lambda an order, \widehat{\Lambda} is a subring of \widehat{D}, ofFiniteIdele produces the locally principal lattice attached to an idele g, conjByFiniteIdele its left order, and finiteIdeleStabilizer together with finiteIdeleDiagonal cut out the double cosets used to index quaternionic automorphic forms.

References

  1. M.-F. Vignéras, Arithmétique des algèbres de quaternions, Lecture Notes in Mathematics 800, Springer, 1980
  2. J. Voight, Quaternion Algebras, Graduate Texts in Mathematics 288, Springer, 2021

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

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib

set_option autoImplicit false

open scoped TensorProduct Pointwise
open IsDedekindDomain NumberField

noncomputable section

namespace Submodule

variable {D : Type*} [Ring D] [Algebra β„š D]

def finiteAdeleBox (Ξ› : Submodule β„€ D) : AddSubgroup (D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š) :=
  AddSubgroup.closure
    {x | βˆƒ z ∈ Ξ›, βˆƒ a : FiniteAdeleRing (π“ž β„š) β„š,
      (βˆ€ v : HeightOneSpectrum (π“ž β„š), a v ∈ v.adicCompletionIntegers β„š) ∧ x = z βŠ—β‚œ[β„š] a}

def ofFiniteIdele (Ξ› : Submodule β„€ D) (g : (D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š)Λ£) : Submodule β„€ D :=
  (AddSubgroup.toIntSubmodule
      ((finiteAdeleBox Ξ›).map
        (AddMonoidHom.mulLeft (g : D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š)))).comap
    ((Algebra.TensorProduct.includeLeft :
        D →ₐ[β„š] D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š).toLinearMap.restrictScalars β„€)

def finiteIdeleStabilizer (Ξ› : Submodule β„€ D) : Subgroup (D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š)Λ£ :=
  MulAction.stabilizer (D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š)Λ£
    ((finiteAdeleBox Ξ› : AddSubgroup (D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š)) :
      Set (D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š))

def conjByFiniteIdele (Ξ› : Submodule β„€ D) (g : (D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š)Λ£) :
    Submodule β„€ D :=
  (AddSubgroup.toIntSubmodule
      ((finiteAdeleBox Ξ›).map
        ((AddMonoidHom.mulRight ((g⁻¹ : (D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š)Λ£) :
            D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š)).comp
          (AddMonoidHom.mulLeft (g : D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š))))).comap
    ((Algebra.TensorProduct.includeLeft :
        D →ₐ[β„š] D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š).toLinearMap.restrictScalars β„€)

variable (D) in

def finiteIdeleDiagonal : DΛ£ β†’* (D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š)Λ£ :=
  Units.map (Algebra.TensorProduct.includeLeftRingHom :
    D β†’+* D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š).toMonoidHom

@[simp] theorem val_finiteIdeleDiagonal_apply (d : DΛ£) :
    ((finiteIdeleDiagonal D d : (D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š)Λ£) :
      D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š) = (d : D) βŠ—β‚œ[β„š] (1 : FiniteAdeleRing (π“ž β„š) β„š) := rfl

theorem mem_ofFiniteIdele_iff (Ξ› : Submodule β„€ D) (g : (D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š)Λ£)
    (z : D) :
    z ∈ ofFiniteIdele Ξ› g ↔
      z βŠ—β‚œ[β„š] (1 : FiniteAdeleRing (π“ž β„š) β„š) ∈
        (finiteAdeleBox Ξ›).map (AddMonoidHom.mulLeft (g : D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š)) :=
  Iff.rfl

theorem mem_conjByFiniteIdele_iff (Ξ› : Submodule β„€ D) (g : (D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š)Λ£)
    (z : D) :
    z ∈ conjByFiniteIdele Ξ› g ↔
      z βŠ—β‚œ[β„š] (1 : FiniteAdeleRing (π“ž β„š) β„š) ∈
        (finiteAdeleBox Ξ›).map
          ((AddMonoidHom.mulRight ((g⁻¹ : (D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š)Λ£) :
              D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š)).comp
            (AddMonoidHom.mulLeft (g : D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š))) :=
  Iff.rfl

theorem mem_finiteIdeleStabilizer_iff (Ξ› : Submodule β„€ D) (u : (D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š)Λ£) :
    u ∈ finiteIdeleStabilizer Ξ› ↔
      u β€’ ((finiteAdeleBox Ξ› : AddSubgroup (D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š)) :
          Set (D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š))
        = ((finiteAdeleBox Ξ› : AddSubgroup (D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š)) :
          Set (D βŠ—[β„š] FiniteAdeleRing (π“ž β„š) β„š)) :=
  Iff.rfl

end Submodule

end

Statements phrased using this module (56)