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][cassels1967algebraic]

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.

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)

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)

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)

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)

@[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.