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.

@[implicit_reducible]

noncomputable 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)

@[implicit_reducible]

noncomputable 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)

@[implicit_reducible]

noncomputable 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)

@[implicit_reducible]

noncomputable 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 = ↑(WithAbs.toAbs (↑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 = ↑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)).symm 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]

noncomputable 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.