Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_IsDedekindDomain_FiniteUnitIdeles.lean

definition module

Unit ideles of a Dedekind domain's finite adele ring

The standing context is a Dedekind domain R with fraction field K (an R-algebra that is a fraction ring of R), so that Mathlib's restricted product \mathbb{A}_{K,f} = FiniteAdeleRing R K over the height-one primes v of R is available, together with the valuation rings v.adicCompletionIntegers K = \mathcal{O}_v \subseteq K_v inside the completions.

The module defines unitIdeles R K, a subgroup of the unit group (\mathbb{A}_{K,f})^{\times} of the finite adele ring, namely the set of units \delta such that, for every height-one prime v of R, the v-component of \delta lies in \mathcal{O}_v and, for every v, the v-component of the inverse unit \delta^{-1} also lies in \mathcal{O}_v. Since the v-component of \delta^{-1} is the inverse of the v-component of \delta, this is exactly the subgroup \widehat{R}^{\times} = \prod_v \mathcal{O}_v^{\times} of ideles that are integral units at every finite place; the two-sided integrality condition is the formulation used, so that membership is stated purely by conditions inside the rings \mathcal{O}_v rather than by invertibility there. The subgroup axioms are verified componentwise: the identity idele and its inverse are integral at each v, products of ideles satisfying both conditions satisfy them again, and the two conditions are interchanged by passing to the inverse.

The accompanying lemma mem_unitIdeles_iff records, for a unit \delta of the finite adele ring, that membership in unitIdeles R K is equivalent to precisely that conjunction of the two families of integrality conditions on \delta and on \delta^{-1}; it holds by definition and exists to make the unfolding available to users of the definition.

Relation to Mathlib

Mathlib supplies the finite adele ring IsDedekindDomain.FiniteAdeleRing and the local integer rings IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, but no named subgroup of integral unit ideles (nor a named subring of integral adeles) for this restricted product; unitIdeles is the project's own definition, placed in the IsDedekindDomain.FiniteAdeleRing namespace.

Where it is used

This subgroup is the vocabulary for the idelic description of the ideal class group: together with the image of K^{\times} under the diagonal embedding (available directly as the range of the induced map on units), it is used in the project's presentation of \operatorname{Cl}(R) as the quotient of (\mathbb{A}_{K,f})^{\times} by the subgroup generated by the principal ideles and the unit ideles.

References

  1. J. Neukirch, Algebraic Number Theory, Grundlehren der mathematischen Wissenschaften 322, Springer, 1999, Chapter VI
  2. J. W. S. Cassels and A. Fröhlich (eds.), Algebraic Number Theory, Academic Press, 1967

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

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib

set_option autoImplicit false

namespace IsDedekindDomain.FiniteAdeleRing

variable (R : Type*) [CommRing R] [IsDedekindDomain R] (K : Type*) [Field K] [Algebra R K] [IsFractionRing R K]

def unitIdeles : Subgroup (FiniteAdeleRing R K)ˣ where
  carrier := {δ | (∀ v : HeightOneSpectrum R, (δ : FiniteAdeleRing R K) v ∈ v.adicCompletionIntegers K) ∧
    ∀ v : HeightOneSpectrum R, ((δ⁻¹ : (FiniteAdeleRing R K)ˣ) : FiniteAdeleRing R K) v ∈ v.adicCompletionIntegers K}
  one_mem' := ⟨fun v => by rw [Units.val_one]; exact one_mem _,
              fun v => by rw [inv_one, Units.val_one]; exact one_mem _⟩
  mul_mem' := by
    rintro x y ⟨hx1, hx2⟩ ⟨hy1, hy2⟩
    exact ⟨fun v => by rw [Units.val_mul]; exact mul_mem (hx1 v) (hy1 v),
           fun v => by rw [mul_inv, Units.val_mul]; exact mul_mem (hx2 v) (hy2 v)⟩
  inv_mem' := by
    rintro x ⟨hx1, hx2⟩
    exact ⟨hx2, fun v => by rw [inv_inv]; exact hx1 v⟩

variable {R K} in
theorem mem_unitIdeles_iff (δ : (FiniteAdeleRing R K)ˣ) :
    δ ∈ unitIdeles R K ↔
      (∀ v : HeightOneSpectrum R, (δ : FiniteAdeleRing R K) v ∈ v.adicCompletionIntegers K) ∧
        ∀ v : HeightOneSpectrum R,
          ((δ⁻¹ : (FiniteAdeleRing R K)ˣ) : FiniteAdeleRing R K) v ∈ v.adicCompletionIntegers K :=
  Iff.rfl

end IsDedekindDomain.FiniteAdeleRing

Statements phrased using this module (6)