The infinite 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.

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.

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

Tags

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

noncomputable 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 = ↑(WithAbs.toAbs (↑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]

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

theorem NumberField.InfiniteAdeleRing.denseRange_algebraMap (K : Type u_1) [Field K] [NumberField K] : DenseRange ⇑(algebraMap K (InfiniteAdeleRing K))

Weak approximation for the infinite adele ring

The number field $K$ is dense in the infinite adele ring $\prod_v K_v$.

@[implicit_reducible]

noncomputable instance NumberField.InfiniteAdeleRing.instNorm (K : Type u_1) [Field K] [NumberField K] : Norm (InfiniteAdeleRing K)

The norm on the infinite adele ring is given by the product of the normalized norms across infinite places. The normalized norm is the real norm at real places and the square of the complex norm at complex places.

Equations

• NumberField.InfiniteAdeleRing.instNorm K = { norm := fun (x : NumberField.InfiniteAdeleRing K) => ∏ v : NumberField.InfinitePlace K, ‖x v‖ ^ v.mult }

theorem NumberField.InfiniteAdeleRing.norm_def {K : Type u_1} [Field K] [NumberField K] (x : InfiniteAdeleRing K) : ‖x‖ = ∏ v : InfinitePlace K, ‖x v‖ ^ v.mult

theorem NumberField.InfiniteAdeleRing.norm_eq_zero_of_not_isUnit {K : Type u_1} [Field K] [NumberField K] {x : InfiniteAdeleRing K} (hx : ¬IsUnit x) : ‖x‖ = 0

theorem NumberField.InfiniteAdeleRing.coe_norm_eq_abs_norm {K : Type u_1} [Field K] [NumberField K] (x : K) : ‖(algebraMap K (InfiniteAdeleRing K)) x‖ = ↑|(Algebra.norm ℚ) x|

The product formula for the infinite adele ring. This is the adelic version of NumberField.InfinitePlace.prod_eq_abs_norm.