Infinite adele ring

This file formalises the definition of the infinite adele ring of a number field K as the product of completions of K over its infinite places. The definition of the completions are formalised in AdeleRingLocallyCompact.NumberTheory.NumberField.Completion.

We show that the infinite adele ring is locally compact and that it is isomorphic to the space ℝ ^ r₁ × ℂ ^ r₂ used in Mathlib.NumberTheory.NumberField.mixedEmbedding.

Main definitions

• NumberField.InfiniteAdeleRing of a number field K is defined as the product of the completions of K over its Archimedean 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.
• NumberField.InfiniteAdeleRing.mixedEmbedding_eq_algebraMap_comp : applying the ring isomorphism of equiv_mixedSpace to a globally embedded (x)ᵥ in the infinite adele ring, where x ∈ K, is the same as applying the embedding K → ℝ ^ r₁ × ℂ ^ r₂ given by NumberField.mixedEmbedding to x.

References

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

Tags

infinite adele ring, number field

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 (NumberField.InfiniteAdeleRing K)

Equations

• NumberField.InfiniteAdeleRing.instCommRing K = Pi.commRing

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

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

• NumberField.InfiniteAdeleRing.instTopologicalSpace K = Pi.topologicalSpace

instance NumberField.InfiniteAdeleRing.instTopologicalRing (K : Type u_1) [Field K] : TopologicalRing (NumberField.InfiniteAdeleRing K)

Equations

• ⋯ = ⋯

instance NumberField.InfiniteAdeleRing.instAlgebra (K : Type u_1) [Field K] : Algebra K (NumberField.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] (v : NumberField.InfinitePlace K) (x : K) : (algebraMap K (NumberField.InfiniteAdeleRing K)) x v = ↑(WithAbs ↑v) x

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

The infinite adele ring is locally compact.

Equations

• ⋯ = ⋯

def NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace (K : Type u_1) [Field K] : NumberField.InfiniteAdeleRing K ≃+* ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)

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 : NumberField.InfiniteAdeleRing K) : (NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace K) x = (fun (v : { w : NumberField.InfinitePlace K // w.IsReal }) => (NumberField.InfinitePlace.Completion.ringEquiv_real_of_isReal ⋯) (x ↑v), fun (v : { w : NumberField.InfinitePlace K // w.IsComplex }) => (NumberField.InfinitePlace.Completion.ringEquiv_complex_of_isComplex ⋯) (x ↑v))

theorem NumberField.InfiniteAdeleRing.mixedEmbedding_eq_algebraMap_comp (K : Type u_1) [Field K] {x : K} : (NumberField.mixedEmbedding K) x = (NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace K) ((algebraMap K (NumberField.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.