The adele ring of a number field

This file contains the formalisation of the adele ring of a number field as the direct product of the infinite adele ring and the finite adele ring.

Main definitions

• NumberField.AdeleRing K is the adele ring of a number field K.
• NumberField.AdeleRing.principalSubgroup K is the subgroup of principal adeles (x)ᵥ.

References

• J.W.S. Cassels, A. Fröhlich, Algebraic Number Theory

Tags

adele ring, number field

The adele ring

def NumberField.AdeleRing (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Type (max u_2 u_2 u_1)

AdeleRing (𝓞 K) K is the adele ring of a number field K.

More generally AdeleRing R K can be used if K is the field of fractions of the Dedekind domain R. This enables use of rings like AdeleRing ℤ ℚ, which in practice are easier to work with than AdeleRing (𝓞 ℚ) ℚ.

Note that this definition does not give the correct answer in the function field case.

Equations

• NumberField.AdeleRing R K = (NumberField.InfiniteAdeleRing K × IsDedekindDomain.FiniteAdeleRing R K)

instance NumberField.AdeleRing.instCommRing (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : CommRing (AdeleRing R K)

Equations

• NumberField.AdeleRing.instCommRing R K = Prod.instCommRing

instance NumberField.AdeleRing.instInhabited (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Inhabited (AdeleRing R K)

Equations

• NumberField.AdeleRing.instInhabited R K = { default := 0 }

instance NumberField.AdeleRing.instTopologicalSpace (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : TopologicalSpace (AdeleRing R K)

Equations

• NumberField.AdeleRing.instTopologicalSpace R K = instTopologicalSpaceProd

instance NumberField.AdeleRing.instIsTopologicalRing (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : IsTopologicalRing (AdeleRing R K)

instance NumberField.AdeleRing.instAlgebra (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Algebra K (AdeleRing R K)

Equations

• NumberField.AdeleRing.instAlgebra R K = Prod.algebra K (NumberField.InfiniteAdeleRing K) (IsDedekindDomain.FiniteAdeleRing R K)

@[simp]

theorem NumberField.AdeleRing.algebraMap_fst_apply (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (x : K) (v : InfinitePlace K) : ((algebraMap K (AdeleRing R K)) x).1 v = ↑x

@[simp]

theorem NumberField.AdeleRing.algebraMap_snd_apply (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (x : K) (v : IsDedekindDomain.HeightOneSpectrum R) : ((algebraMap K (AdeleRing R K)) x).2 v = ↑x

theorem NumberField.AdeleRing.algebraMap_injective (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [NumberField K] : Function.Injective ⇑(algebraMap K (AdeleRing R K))

@[reducible, inline]

abbrev NumberField.AdeleRing.principalSubgroup (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : AddSubgroup (AdeleRing R K)

The subgroup of principal adeles (x)ᵥ where x ∈ K.

Equations

• NumberField.AdeleRing.principalSubgroup R K = (algebraMap K (NumberField.AdeleRing R K)).range.toAddSubgroup