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, as FinsetAdeleRing R K S and we show that this is locally compact. The finite S-adele ring has 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.FinsetProd R K S is the DedekindDomain.ProdAdicCompletions R K split into a product along the predicate v ∈ S.
• DedekindDomain.FinsetIntegralAdeles R K S 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.FinsetIntegralAdeles.Subtype R K S is DedekindDomain.FinsetIntegralAdeles R K S as a subtype of DedekindDomain.FinsetProd R K S.
• DedekindDomain.FinsetAdeleRing R K S is the type of all finite S-adeles.

Main results

• DedekindDomain.FinsetAdeleRing.homeomorph_subtype : the finite S-adele ring is homeomorphic to DedekindDomain.FiniteIntegralAdeles.Subtype.
• DedekindDomain.FinsetAdeleRing.algebraMap_inducing : the map sending finite S-adeles to finite adeles is inducing; equivalently, the topology of the finite S-adele ring when viewed as a subspace of the finite adele ring is equal to the topology when viewed as a subspace of ProdAdicCompletions R K.
• DedekindDomain.FinsetAdeleRing.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.FinsetIntegralAdeles and DedekindDomain.FinsetIntegralAdeles.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.FinsetIntegralAdeles.homeomorph.

Tags

finite s-adele ring, dedekind domain

def DedekindDomain.ProdAdicCompletions.FinsetProd (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : Type (max u_1 u_2)

The type DedekindDomain.ProdAdicCompletions split as a product along the predicate v ∈ S.

Equations

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

instance DedekindDomain.ProdAdicCompletions.instTopologicalSpaceFinsetProd (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : TopologicalSpace (DedekindDomain.ProdAdicCompletions.FinsetProd R K S)

Equations

• DedekindDomain.ProdAdicCompletions.instTopologicalSpaceFinsetProd R K S = instTopologicalSpaceProd

instance DedekindDomain.ProdAdicCompletions.instCommRingFinsetProd (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : CommRing (DedekindDomain.ProdAdicCompletions.FinsetProd R K S)

Equations

• DedekindDomain.ProdAdicCompletions.instCommRingFinsetProd R K S = Prod.instCommRing

instance DedekindDomain.ProdAdicCompletions.instInhabitedFinsetProd (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : Inhabited (DedekindDomain.ProdAdicCompletions.FinsetProd R K S)

Equations

• DedekindDomain.ProdAdicCompletions.instInhabitedFinsetProd R K S = instInhabitedProd

def DedekindDomain.FinsetIntegralAdeles (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : Type (max u_1 u_2)

Binary product split along the predicate v ∈ S, whose first element ranges over v-adic completions of K and whose second element ranges over v-adic rings of integers.

Equations

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

def DedekindDomain.FinsetIntegralAdeles.Subtype (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : Type (max 0 u_1 u_2)

The subtype of DedekindDomain.FinsetProd whose second product ranges over v-adic rings of integers.

Equations

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

instance DedekindDomain.FinsetIntegralAdeles.instCoeFinsetProd (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : Coe (DedekindDomain.FinsetIntegralAdeles R K S) (DedekindDomain.ProdAdicCompletions.FinsetProd R K S)

Equations

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

theorem DedekindDomain.FinsetIntegralAdeles.coe_injective (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : Function.Injective Coe.coe

instance DedekindDomain.FinsetIntegralAdeles.instTopologicalSpace (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : TopologicalSpace (DedekindDomain.FinsetIntegralAdeles R K S)

Equations

• DedekindDomain.FinsetIntegralAdeles.instTopologicalSpace R K S = instTopologicalSpaceProd

instance DedekindDomain.FinsetIntegralAdeles.topologicalSpaceSubtype (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : TopologicalSpace (DedekindDomain.FinsetIntegralAdeles.Subtype R K S)

Equations

• DedekindDomain.FinsetIntegralAdeles.topologicalSpaceSubtype R K S = instTopologicalSpaceSubtype

instance DedekindDomain.FinsetIntegralAdeles.instCommRing (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : CommRing (DedekindDomain.FinsetIntegralAdeles R K S)

Equations

• DedekindDomain.FinsetIntegralAdeles.instCommRing R K S = Prod.instCommRing

instance DedekindDomain.FinsetIntegralAdeles.instInhabited (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : Inhabited (DedekindDomain.FinsetIntegralAdeles R K S)

Equations

• DedekindDomain.FinsetIntegralAdeles.instInhabited R K S = instInhabitedProd

def DedekindDomain.FinsetIntegralAdeles.subtype_equiv (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : DedekindDomain.FinsetIntegralAdeles.Subtype R K S ≃ DedekindDomain.FinsetIntegralAdeles R K S

The type equivalence between the two formalisations of Π (v ∈ S), Kᵥ × Π (v ∉ S), Oᵥ.

Equations

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

def DedekindDomain.FinsetIntegralAdeles.subtype_homeomorph (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : DedekindDomain.FinsetIntegralAdeles.Subtype R K S ≃ₜ DedekindDomain.FinsetIntegralAdeles R K S

The homeomorphism between the two formalisations of Π (v ∈ S), Kᵥ × Π (v ∉ S), Oᵥ.

Equations

• DedekindDomain.FinsetIntegralAdeles.subtype_homeomorph R K S = { toEquiv := DedekindDomain.FinsetIntegralAdeles.subtype_equiv R K S, continuous_toFun := ⋯, continuous_invFun := ⋯ }

instance DedekindDomain.FinsetIntegralAdeles.instLocallyCompactSpace (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : LocallyCompactSpace (DedekindDomain.FinsetIntegralAdeles R K S)

Π (v ∈ S), Kᵥ × Π (v ∉ S), Oᵥ is locally compact. Note: instance search is slow because of the same issues for adicCompletionIntegers that we had with RingOfIntegers when it was a subring.

Equations

• ⋯ = ⋯

instance DedekindDomain.FinsetIntegralAdeles.instLocallyCompactSpaceSubtype (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : LocallyCompactSpace (DedekindDomain.FinsetIntegralAdeles.Subtype R K S)

Π (v ∈ S), Kᵥ × Π (v ∉ S), Oᵥ as a subtype is locally compact.

Equations

• ⋯ = ⋯

def DedekindDomain.IsFinsetAdele {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) (x : DedekindDomain.ProdAdicCompletions R K) : Prop

Equations

• DedekindDomain.IsFinsetAdele S x = ∀ v ∉ S, x v ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v

theorem DedekindDomain.IsFinsetAdele.mul {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {S : Finset (IsDedekindDomain.HeightOneSpectrum R)} {x : DedekindDomain.ProdAdicCompletions R K} {y : DedekindDomain.ProdAdicCompletions R K} (hx : DedekindDomain.IsFinsetAdele S x) (hy : DedekindDomain.IsFinsetAdele S y) : DedekindDomain.IsFinsetAdele S (x * y)

theorem DedekindDomain.IsFinsetAdele.one {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {S : Finset (IsDedekindDomain.HeightOneSpectrum R)} : DedekindDomain.IsFinsetAdele S 1

theorem DedekindDomain.IsFinsetAdele.add {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {S : Finset (IsDedekindDomain.HeightOneSpectrum R)} {x : DedekindDomain.ProdAdicCompletions R K} {y : DedekindDomain.ProdAdicCompletions R K} (hx : DedekindDomain.IsFinsetAdele S x) (hy : DedekindDomain.IsFinsetAdele S y) : DedekindDomain.IsFinsetAdele S (x + y)

theorem DedekindDomain.IsFinsetAdele.zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {S : Finset (IsDedekindDomain.HeightOneSpectrum R)} : DedekindDomain.IsFinsetAdele S 0

theorem DedekindDomain.IsFinsetAdele.neg {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {S : Finset (IsDedekindDomain.HeightOneSpectrum R)} {x : DedekindDomain.ProdAdicCompletions R K} (hx : DedekindDomain.IsFinsetAdele S x) : DedekindDomain.IsFinsetAdele S (-x)

def DedekindDomain.FinsetAdeleRing (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : Type (max 0 u_1 u_2)

The finite S-adele ring.

Equations

• DedekindDomain.FinsetAdeleRing R K S = { x : DedekindDomain.ProdAdicCompletions R K // DedekindDomain.IsFinsetAdele S x }

def DedekindDomain.FinsetAdeleRing.subring (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : Subring (DedekindDomain.ProdAdicCompletions R K)

The finite S-adele ring regarded as a subring of the product of local completions of K.

Note that the finite S-adele ring is not a subalgebra of the product of ∏ Kᵥ, but it is a subalgebra of ∏ (v ∈ S), Kᵥ × ∏ (v ∉ S), Oᵥ.

Equations

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

instance DedekindDomain.FinsetAdeleRing.instCommRing (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : CommRing (DedekindDomain.FinsetAdeleRing R K S)

Equations

• DedekindDomain.FinsetAdeleRing.instCommRing R K S = (DedekindDomain.FinsetAdeleRing.subring R K S).toCommRing

instance DedekindDomain.FinsetAdeleRing.instTopologicalSpace (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : TopologicalSpace (DedekindDomain.FinsetAdeleRing R K S)

Equations

• DedekindDomain.FinsetAdeleRing.instTopologicalSpace R K S = inferInstanceAs (TopologicalSpace ↥(DedekindDomain.FinsetAdeleRing.subring R K S))

instance DedekindDomain.FinsetAdeleRing.instTopologicalRing (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : TopologicalRing (DedekindDomain.FinsetAdeleRing R K S)

Equations

• ⋯ = ⋯

theorem DedekindDomain.FinsetAdeleRing.ext (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) {x : DedekindDomain.FinsetAdeleRing R K S} {y : DedekindDomain.FinsetAdeleRing R K S} (h : ↑x = ↑y) : x = y

def DedekindDomain.FinsetAdeleRing.homeomorph_subtype (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : DedekindDomain.FinsetAdeleRing R K S ≃ₜ DedekindDomain.FinsetIntegralAdeles.Subtype R K S

The finite S-adele ring is homeomorphic to Π (v ∈ S), Kᵥ × Π (v ∉ S), Oᵥ.

Equations

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

instance DedekindDomain.FinsetAdeleRing.locallyCompactSpace (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : LocallyCompactSpace (DedekindDomain.FinsetAdeleRing R K S)

The finite S-adele ring is locally compact.

Equations

• ⋯ = ⋯

theorem DedekindDomain.FinsetAdeleRing.isFiniteAdele {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {S : Finset (IsDedekindDomain.HeightOneSpectrum R)} (x : DedekindDomain.FinsetAdeleRing R K S) : (↑x).IsFiniteAdele

A finite S-adele is a finite adele.

theorem DedekindDomain.FinsetAdeleRing.isFinsetAdele_localInclusion {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {S : Finset (IsDedekindDomain.HeightOneSpectrum R)} (v : IsDedekindDomain.HeightOneSpectrum R) {x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v} (hx : x ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) : DedekindDomain.IsFinsetAdele S ↑(DedekindDomain.FiniteAdeleRing.localInclusion K v x)

If x is a v-adic integer, then the local inclusion of x at any place v is a finite S-adele.

theorem DedekindDomain.FinsetAdeleRing.isFinsetAdele_localInclusion_of_mem {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {S : Finset (IsDedekindDomain.HeightOneSpectrum R)} {v : IsDedekindDomain.HeightOneSpectrum R} (x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (h : v ∈ S) : DedekindDomain.IsFinsetAdele S ↑(DedekindDomain.FiniteAdeleRing.localInclusion K v x)

If v ∈ S then the local inclusion of any x in the v-adic completion of K is a finite S-adele.

theorem DedekindDomain.FinsetAdeleRing.isFinsetAdele_support {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x : DedekindDomain.FiniteAdeleRing R K) : DedekindDomain.IsFinsetAdele x.support ↑x

def DedekindDomain.FinsetAdeleRing.ofFiniteAdele_support {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x : DedekindDomain.FiniteAdeleRing R K) : DedekindDomain.FinsetAdeleRing R K x.support

Equations

• DedekindDomain.FinsetAdeleRing.ofFiniteAdele_support x = ⟨↑x, ⋯⟩

instance DedekindDomain.FinsetAdeleRing.instAlgebraFiniteAdeleRing (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : Algebra (DedekindDomain.FinsetAdeleRing R K S) (DedekindDomain.FiniteAdeleRing R K)

Equations

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

theorem DedekindDomain.FinsetAdeleRing.algebraMap_injective (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : Function.Injective ⇑(algebraMap (DedekindDomain.FinsetAdeleRing R K S) (DedekindDomain.FiniteAdeleRing R K))

The map sending finite S-adeles to finite adeles is injective.

theorem DedekindDomain.FinsetAdeleRing.algebraMap_range (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : Set.range ⇑(algebraMap (DedekindDomain.FinsetAdeleRing R K S) (DedekindDomain.FiniteAdeleRing R K)) = {x : DedekindDomain.FiniteAdeleRing R K | DedekindDomain.IsFinsetAdele S ↑x}

theorem DedekindDomain.FinsetAdeleRing.isFinsetAdele_mem_range {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {S : Finset (IsDedekindDomain.HeightOneSpectrum R)} {x : DedekindDomain.FiniteAdeleRing R K} (hx : x ∈ Set.range ⇑(algebraMap (DedekindDomain.FinsetAdeleRing R K S) (DedekindDomain.FiniteAdeleRing R K))) : DedekindDomain.IsFinsetAdele S ↑x

def DedekindDomain.FinsetAdeleRing.ofFiniteAdele_mem_range {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {S : Finset (IsDedekindDomain.HeightOneSpectrum R)} {x : DedekindDomain.FiniteAdeleRing R K} (hx : x ∈ Set.range ⇑(algebraMap (DedekindDomain.FinsetAdeleRing R K S) (DedekindDomain.FiniteAdeleRing R K))) : DedekindDomain.FinsetAdeleRing R K S

Equations

• DedekindDomain.FinsetAdeleRing.ofFiniteAdele_mem_range hx = ⟨↑x, ⋯⟩

theorem DedekindDomain.FinsetAdeleRing.algebraMap_range_mem_nhds {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {S : Finset (IsDedekindDomain.HeightOneSpectrum R)} (x : DedekindDomain.FinsetAdeleRing R K S) : Set.range ⇑(algebraMap (DedekindDomain.FinsetAdeleRing R K S) (DedekindDomain.FiniteAdeleRing R K)) ∈ nhds ((algebraMap (DedekindDomain.FinsetAdeleRing R K S) (DedekindDomain.FiniteAdeleRing R K)) x)

theorem DedekindDomain.FinsetAdeleRing.isOpen_algebraMap_range (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : IsOpen (Set.range ⇑(algebraMap (DedekindDomain.FinsetAdeleRing R K S) (DedekindDomain.FiniteAdeleRing R K)))

The finite S-adele ring is open in the finite adele ring.

theorem DedekindDomain.FinsetAdeleRing.subtype_val_algebraMap (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : Subtype.val = Subtype.val ∘ ⇑(algebraMap (DedekindDomain.FinsetAdeleRing R K S) (DedekindDomain.FiniteAdeleRing R K))

Subtype.val of the finite S-adele ring factors through the embedding into the finite adele ring.

theorem DedekindDomain.FinsetAdeleRing.algebraMap_mk {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {S : Finset (IsDedekindDomain.HeightOneSpectrum R)} {x : DedekindDomain.FiniteAdeleRing R K} (hx : DedekindDomain.IsFinsetAdele S ↑x) : (algebraMap (DedekindDomain.FinsetAdeleRing R K S) (DedekindDomain.FiniteAdeleRing R K)) ⟨↑x, hx⟩ = x

theorem DedekindDomain.FinsetAdeleRing.nhds_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {S : Finset (IsDedekindDomain.HeightOneSpectrum R)} {x : DedekindDomain.FinsetAdeleRing R K S} {U : Set (DedekindDomain.FinsetAdeleRing R K S)} : U ∈ nhds x ↔ ∃ (V : (v : IsDedekindDomain.HeightOneSpectrum R) → Set (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (I : Finset (IsDedekindDomain.HeightOneSpectrum R)), (∀ (v : IsDedekindDomain.HeightOneSpectrum R), V v ∈ nhds (↑x v)) ∧ Subtype.val ⁻¹' (↑I).pi V ⊆ U

Neighbourhoods of the finite S-adele ring.

theorem DedekindDomain.FinsetAdeleRing.algebraMap_image_mem_nhds {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {S : Finset (IsDedekindDomain.HeightOneSpectrum R)} (x : DedekindDomain.FinsetAdeleRing R K S) {U : Set (DedekindDomain.FinsetAdeleRing R K S)} (h : U ∈ nhds x) : ⇑(algebraMap (DedekindDomain.FinsetAdeleRing R K S) (DedekindDomain.FiniteAdeleRing R K)) '' U ∈ nhds ((algebraMap (DedekindDomain.FinsetAdeleRing R K S) (DedekindDomain.FiniteAdeleRing R K)) x)

The embedding of the finite S-adele ring into the finite adele ring preserves neighbourhoods.

theorem DedekindDomain.FinsetAdeleRing.mem_nhds_comap_algebraMap {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {S : Finset (IsDedekindDomain.HeightOneSpectrum R)} (x : DedekindDomain.FinsetAdeleRing R K S) {U : Set (DedekindDomain.FinsetAdeleRing R K S)} (h : U ∈ Filter.comap (⇑(algebraMap (DedekindDomain.FinsetAdeleRing R K S) (DedekindDomain.FiniteAdeleRing R K))) (nhds ((algebraMap (DedekindDomain.FinsetAdeleRing R K S) (DedekindDomain.FiniteAdeleRing R K)) x))) : U ∈ nhds x

The pullback of a neighbourhood in the finite adele ring is a neighbourhood in the finite S-adele ring.

theorem DedekindDomain.FinsetAdeleRing.algebraMap_inducing (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : Inducing ⇑(algebraMap (DedekindDomain.FinsetAdeleRing R K S) (DedekindDomain.FiniteAdeleRing R K))

The topologies of the finite S-adele ring when viewed as a subspace of ProdAdicCompletions R K and as a subspace of the finite adele ring coincide.

theorem DedekindDomain.FiniteAdeleRing.locallyCompactSpace (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : LocallyCompactSpace (DedekindDomain.FiniteAdeleRing R K)

The finite adele ring is locally compact.