Finite S-adele ring #

Let R be a Dedekind domain of Krull dimension 1, K its field of fractions and S a finite set of finite places v of K. In this file we define the finite S-adele ring, whose carrier is the set of all elements in ProdAdicCompletions R K which are in the v-adic ring of integers outside of S, and we show that this is locally compact. The finite S-adele ring affords an open embedding into the regular finite adele ring and, moreover, cover the finite adele ring. This allows us to show that the finite adele ring is also locally compact.

Main definitions #

DedekindDomain.SProdAdicCompletions R K S is the DedekindDomain.ProdAdicCompletions R K split into a product along the predicate v ∈ S.
DedekindDomain.SProdAdicCompletionIntegers is the direct product whose left type is the product of the v-adic completions of K over all v ∈ S and whose right type is the product of the v-adic ring of integers over all v ∉ S.
DedekindDomain.SProdAdicCompletionIntegers_subtype is the subtype of DedekindDomain.SProdAdicCompletions R K S analogous to DedekindDomain.SProdAdicCompletionIntegers.
DedekindDomain.finiteSAdeleRing is the subring of ProdAdicCompletions R K of all finite S-adeles.
DedekindDomain.FiniteSAdeleRing.toFiniteAdeleRing is the map embedding the finite S-adele ring into the finite adele ring.
DedekindDomain.FiniteSAdeleRing.topologicalSpace is the topological space of the finite S-adele ring, viewed as a subspace of the finite adele ring; this is shown to be equivalent to the topology when viewed as a subspace of ProdAdicCompletions R K (that these topologies coincide is an important part of what allows us to show that the finite S-adele ring is locally compact).

Main results #

DedekindDomain.FiniteSAdeleRing.toFiniteAdeleRing_openEmbedding : the map sending finite S-adeles to finite adeles is an open embedding; this is crucial so that when we can push the S-adeles to an open covering of the finite adele ring.
DedekindDomain.FiniteSAdeleRing.generatingSet_eq : the generating set of the subspace topology of the finite S-adele ring when viewed as a subspace of the finite adele ring is equal to the generating set of the subspace topology when viewed as a subspace of ProdAdicCompletions R K and so these two topologies coincide.
DedekindDomain.FiniteSAdeleRing.homeomorph_piSubtypeProd : the finite S-adele ring is homeomorphic to DedekindDomain.SProdAdicCompletionIntegers_subtype.
DedekindDomain.FiniteSAdeleRing.locallyCompactSpace : the finite S-adele ring is locally compact.
DedekindDomain.FiniteAdeleRing.locallyCompactSpace : the finite adele ring is locally compact.

Implementation notes #

There are two formalisations of the object Π (v ∈ S), Kᵥ × Π (v ∉ S), Oᵥ. These are DedekindDomain.SProdAdicCompletionIntegers and DedekindDomain.SProdAdicCompletionIntegers_subtype, where the former is viewed as a type and the latter as a subtype of Π (v ∈ S), Kᵥ × Π (v ∉ S), Kᵥ. The reason for this is that the former is easily shown to be locally compact (its fst is a finite product of locally compact spaces and its snd is an infinite product of compact spaces), but it is much easier to show that the latter is homeomorphic to the finite S-adele ring, because we can just descend the natural homeomorphism on parent types. Thus we need to show that these two formalisations are also homeomorphic, which is found in DedekindDomain.SProdAdicCompletionIntegers.homeomorph.

Tags #

finite s-adele ring, dedekind domain