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ölich, 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 (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] (x : K) (v : NumberField.InfinitePlace 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

• ⋯ = ⋯

@[reducible, inline]

abbrev NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace (K : Type u_1) [Field K] : NumberField.InfiniteAdeleRing K ≃+* NumberField.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 : NumberField.InfiniteAdeleRing K) : (NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace K) x = (fun (v : { w : NumberField.InfinitePlace K // w.IsReal }) => (NumberField.InfinitePlace.Completion.extensionEmbedding_of_isReal ⋯) (x ↑v), fun (v : { w : NumberField.InfinitePlace K // w.IsComplex }) => (NumberField.InfinitePlace.Completion.extensionEmbedding ↑v) (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.

The adele ring

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

The adele ring of a number field.

Equations

• NumberField.AdeleRing K = (NumberField.InfiniteAdeleRing K × DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K)

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

Equations

• NumberField.AdeleRing.instCommRing K = Prod.instCommRing

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

Equations

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

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

Equations

• NumberField.AdeleRing.instTopologicalSpace K = instTopologicalSpaceProd

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

Equations

• ⋯ = ⋯

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

Equations

• NumberField.AdeleRing.instAlgebra K = Prod.algebra K (NumberField.InfiniteAdeleRing K) (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K)

@[simp]

theorem NumberField.AdeleRing.algebraMap_fst_apply (K : Type u_1) [Field K] [NumberField K] (x : K) (v : NumberField.InfinitePlace K) : ((algebraMap K (NumberField.AdeleRing K)) x).1 v = ↑(WithAbs ↑v) x

@[simp]

theorem NumberField.AdeleRing.algebraMap_snd_apply (K : Type u_1) [Field K] [NumberField K] (x : K) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : (fun (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => ↑((algebraMap K (NumberField.AdeleRing K)) x).2 v) v = ↑K x

theorem NumberField.AdeleRing.algebraMap_injective (K : Type u_1) [Field K] [NumberField K] : Function.Injective ⇑(algebraMap K (NumberField.AdeleRing K))

@[reducible, inline]

abbrev NumberField.AdeleRing.principalSubgroup (K : Type u_1) [Field K] [NumberField K] : AddSubgroup (NumberField.AdeleRing K)

The subgroup of principal adeles (x)ᵥ where x ∈ K.

Equations

• NumberField.AdeleRing.principalSubgroup K = (algebraMap K (NumberField.AdeleRing K)).range.toAddSubgroup