The adele ring of a number field

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

Main definitions

• NumberField.InfiniteAdeleRing of a number field K is defined as the product of the completions of K over its infinite places.
• NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace is the ring isomorphism between the infinite adele ring of K and ℝ ^ r₁ × ℂ ^ r₂, where (r₁, r₂) is the signature of K.
• NumberField.AdeleRing K is the adele ring of a number field K.
• NumberField.AdeleRing.principalSubgroup K is the subgroup of principal adeles (x)ᵥ.

Main results

• NumberField.InfiniteAdeleRing.locallyCompactSpace : the infinite adele ring is a locally compact space.

References

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

Tags

infinite adele ring, adele ring, number field

The infinite adele ring

The infinite adele ring is the finite product of completions of a number field over its infinite places. See NumberField.InfinitePlace for the definition of an infinite place and NumberField.InfinitePlace.Completion for the associated completion.

def NumberField.InfiniteAdeleRing (K : Type u_1) [Field K] : Type u_1

The infinite adele ring of a number field.

Equations

• NumberField.InfiniteAdeleRing K = ((v : NumberField.InfinitePlace K) → v.Completion)

instance NumberField.InfiniteAdeleRing.instCommRing (K : Type u_1) [Field K] : CommRing (InfiniteAdeleRing K)

Equations

• NumberField.InfiniteAdeleRing.instCommRing K = Pi.commRing

instance NumberField.InfiniteAdeleRing.instInhabited (K : Type u_1) [Field K] : Inhabited (InfiniteAdeleRing K)

Equations

• NumberField.InfiniteAdeleRing.instInhabited K = { default := 0 }

instance NumberField.InfiniteAdeleRing.instNontrivial (K : Type u_1) [Field K] [NumberField K] : Nontrivial (InfiniteAdeleRing K)

instance NumberField.InfiniteAdeleRing.instTopologicalSpace (K : Type u_1) [Field K] : TopologicalSpace (InfiniteAdeleRing K)

Equations

• NumberField.InfiniteAdeleRing.instTopologicalSpace K = Pi.topologicalSpace

instance NumberField.InfiniteAdeleRing.instIsTopologicalRing (K : Type u_1) [Field K] : IsTopologicalRing (InfiniteAdeleRing K)

instance NumberField.InfiniteAdeleRing.instAlgebra (K : Type u_1) [Field K] : Algebra K (InfiniteAdeleRing K)

Equations

• NumberField.InfiniteAdeleRing.instAlgebra K = Pi.algebra (NumberField.InfinitePlace K) NumberField.InfinitePlace.Completion

@[simp]

theorem NumberField.InfiniteAdeleRing.algebraMap_apply (K : Type u_1) [Field K] (x : K) (v : InfinitePlace K) : (algebraMap K (InfiniteAdeleRing K)) x v = ↑x

instance NumberField.InfiniteAdeleRing.locallyCompactSpace (K : Type u_1) [Field K] [NumberField K] : LocallyCompactSpace (InfiniteAdeleRing K)

The infinite adele ring is locally compact.

@[reducible, inline]

abbrev NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace (K : Type u_1) [Field K] : InfiniteAdeleRing K ≃+* mixedEmbedding.mixedSpace K

The ring isomorphism between the infinite adele ring of a number field and the space ℝ ^ r₁ × ℂ ^ r₂, where (r₁, r₂) is the signature of the number field.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace_apply (K : Type u_1) [Field K] (x : InfiniteAdeleRing K) : (ringEquiv_mixedSpace K) x = (fun (v : { w : InfinitePlace K // w.IsReal }) => (InfinitePlace.Completion.extensionEmbeddingOfIsReal ⋯) (x ↑v), fun (v : { w : InfinitePlace K // w.IsComplex }) => (InfinitePlace.Completion.extensionEmbedding ↑v) (x ↑v))

theorem NumberField.InfiniteAdeleRing.mixedEmbedding_eq_algebraMap_comp (K : Type u_1) [Field K] {x : K} : (mixedEmbedding K) x = (ringEquiv_mixedSpace K) ((algebraMap K (InfiniteAdeleRing K)) x)

Transfers the embedding of x ↦ (x)ᵥ of the number field K into its infinite adele ring to the mixed embedding x ↦ (φᵢ(x))ᵢ of K into the space ℝ ^ r₁ × ℂ ^ r₂, where (r₁, r₂) is the signature of K and φᵢ are the complex embeddings of K.

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