Restricted products of topological spaces, topological groups and rings

We endow a restricted product of topological spaces with a natural topology, which we describe below. We also show various compatibility results when we change filters, and extend the construction of restricted products of algebraic structures to the topological setting.

In particular, with the theory of adeles in mind, we show that if each R i is a locally compact topological ring with open subring A i, and if all but finitely many of the A is are also compact, then Πʳ i, [R i, A i] is a locally compact topological ring.

Main definitions

• RestrictedProduct.topologicalSpace: the TopologicalSpace instance on the restricted product Πʳ i, [R i, A i]_[𝓕].

Topology on the restricted product

The topology on the restricted product Πʳ i, [R i, A i]_[𝓕] is defined in the following way:

1. If 𝓕 is some principal filter 𝓟 s, recall that Πʳ i, [R i, A i]_[𝓟 s] is canonically identified with (Π i ∈ s, A i) × (Π i ∉ s, R i). We endow it with the product topology, which is also the topology induced from the full product Π i, R i.
2. In general, we note that 𝓕 is the infimum of the principal filters coarser than 𝓕. We then endow Πʳ i, [R i, A i]_[𝓕] with the inductive limit / final topology associated to the inclusion maps Πʳ i, [R i, A i]_[𝓟 s] → Πʳ i, [R i, A i]_[𝓕] where 𝓕 ≤ 𝓟 s.

In particular:

• On the classical restricted product, with respect to the cofinite filter, this corresponds to taking the inductive limit of the Πʳ i, [R i, A i]_[𝓟 s] over all cofinite sets s : Set ι.
• If 𝓕 = 𝓟 s is a principal filter, this second step clearly does not change the topology, since s belongs to the indexing set of the inductive limit.

Taking advantage of that second remark, we do not actually declare an instance specific to principal filters. Instead, we provide directly the general instance (corresponding to step 2 above) as RestrictedProduct.topologicalSpace. We then prove that, for a principal filter, the map to the full product is an inducing (RestrictedProduct.isEmbedding_coe_of_principal), and that the topology for a general 𝓕 is indeed the expected inductive limit (RestrictedProduct.topologicalSpace_eq_iSup).

Main statements

• RestrictedProduct.isEmbedding_coe_of_principal: for any set S, Πʳ i, [R i, A i]_[𝓟 S] is endowed with the subset topology coming from Π i, R i.

• RestrictedProduct.topologicalSpace_eq_iSup: the topology on Πʳ i, [R i, A i]_[𝓕] is the inductive limit / final topology associated to the natural maps Πʳ i, [R i, A i]_[𝓟 S] → Πʳ i, [R i, A i]_[𝓕], where 𝓕 ≤ 𝓟 S.

• RestrictedProduct.continuous_dom: a map from Πʳ i, [R i, A i]_[𝓕] is continuous if and only if its restriction to each Πʳ i, [R i, A i]_[𝓟 s] (with 𝓕 ≤ 𝓟 s) is continuous.

• RestrictedProduct.continuous_dom_prod_left: assume that each A i is an open subset of R i. Then, for any topological space Y, a map from Y × Πʳ i, [R i, A i] is continuous if and only if its restriction to each Y × Πʳ i, [R i, A i]_[𝓟 S] (with S cofinite) is continuous.

• RestrictedProduct.isTopologicalGroup: if each R i is a topological group and each A i is an open subgroup of R i, then Πʳ i, [R i, A i] is a topological group.

• RestrictedProduct.isTopologicalRing: if each R i is a topological ring and each A i is an open subring of R i, then Πʳ i, [R i, A i] is a topological ring.

• RestrictedProduct.continuousSMul: if some topological monoid G acts on each M i, and each A i is stable for that action, then the natural action of G on Πʳ i, [M i, A i] is also continuous. In particular, if each M i is a topological R-module and each A i is an open sub-R-module of M i, then Πʳ i, [M i, A i] is a topological R-module.

• RestrictedProduct.weaklyLocallyCompactSpace_of_cofinite: if each R i is weakly locally compact, each A i is open, and all but finitely many A is are also compact, then the restricted product Πʳ i, [R i, A i] is weakly locally compact.

• RestrictedProduct.locallyCompactSpace_of_group: assume that each R i is a locally compact group with A i an open subgroup. Assume also that all but finitely many A is are compact. Then the restricted product Πʳ i, [R i, A i] is a locally compact group.

Implementation details

Outside of principal filters and the cofinite filter, the topology we define on the restricted product does not seem well-behaved. While declaring a single instance is practical, it may conflict with more interesting topologies in some other cases. Thus, future contributions should not restrain from specializing these instances to principal and cofinite filters if necessary.

Tags

restricted product, adeles, ideles

Topology on the restricted product

The topology on the restricted product Πʳ i, [R i, A i]_[𝓕] is defined in the following way:

1. If 𝓕 is some principal filter 𝓟 s, recall that Πʳ i, [R i, A i]_[𝓟 s] is canonically identified with (Π i ∈ s, A i) × (Π i ∉ s, R i). We endow it with the product topology, which is also the topology induced from the full product Π i, R i.
2. In general, we note that 𝓕 is the infimum of the principal filters coarser than 𝓕. We then endow Πʳ i, [R i, A i]_[𝓕] with the inductive limit / final topology associated to the inclusion maps Πʳ i, [R i, A i]_[𝓟 s] → Πʳ i, [R i, A i]_[𝓕] where 𝓕 ≤ 𝓟 s.

In particular:

• On the classical restricted product, with respect to the cofinite filter, this corresponds to taking the inductive limit of the Πʳ i, [R i, A i]_[𝓟 s] over all cofinite sets s : Set ι.
• If 𝓕 = 𝓟 s is a principal filter, this second step clearly does not change the topology, since s belongs to the indexing set of the inductive limit.

Taking advantage of that second remark, we do not actually declare an instance specific to principal filters. Instead, we provide directly the general instance (corresponding to step 2 above) as RestrictedProduct.topologicalSpace. We then prove that, for a principal filter, the map to the full product is an inducing (RestrictedProduct.isEmbedding_coe_of_principal), and that the topology for a general 𝓕 is indeed the expected inductive limit (RestrictedProduct.topologicalSpace_eq_iSup).

Note: outside of these two cases, this topology on the restricted product does not seem well-behaved. While declaring a single instance is practical, it may conflict with more interesting topologies in some other cases. Thus, future contributions should not restrain from specializing these instances to principal and cofinite filters if necessary.

Definition of the topology

instance RestrictedProduct.topologicalSpace {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) (𝓕 : Filter ι) [(i : ι) → TopologicalSpace (R i)] : TopologicalSpace (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕)

Equations

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

theorem RestrictedProduct.continuous_coe {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} {𝓕 : Filter ι} [(i : ι) → TopologicalSpace (R i)] : Continuous DFunLike.coe

theorem RestrictedProduct.continuous_eval {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} {𝓕 : Filter ι} [(i : ι) → TopologicalSpace (R i)] (i : ι) : Continuous fun (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕) => x i

theorem RestrictedProduct.continuous_inclusion {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} {𝓕 : Filter ι} [(i : ι) → TopologicalSpace (R i)] {𝓖 : Filter ι} (h : 𝓕 ≤ 𝓖) : Continuous (inclusion R A h)

instance RestrictedProduct.instT0Space {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} {𝓕 : Filter ι} [(i : ι) → TopologicalSpace (R i)] [∀ (i : ι), T0Space (R i)] : T0Space (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕)

instance RestrictedProduct.instT1Space {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} {𝓕 : Filter ι} [(i : ι) → TopologicalSpace (R i)] [∀ (i : ι), T1Space (R i)] : T1Space (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕)

instance RestrictedProduct.instT2Space {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} {𝓕 : Filter ι} [(i : ι) → TopologicalSpace (R i)] [∀ (i : ι), T2Space (R i)] : T2Space (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕)

Topological facts in the principal case

theorem RestrictedProduct.topologicalSpace_eq_of_principal {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] {S : Set ι} : topologicalSpace R A (Filter.principal S) = TopologicalSpace.induced DFunLike.coe inferInstance

theorem RestrictedProduct.topologicalSpace_eq_of_top {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] : topologicalSpace R A ⊤ = TopologicalSpace.induced DFunLike.coe inferInstance

theorem RestrictedProduct.topologicalSpace_eq_of_bot {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] : topologicalSpace R A ⊥ = TopologicalSpace.induced DFunLike.coe inferInstance

theorem RestrictedProduct.isEmbedding_coe_of_principal {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] {S : Set ι} : Topology.IsEmbedding DFunLike.coe

theorem RestrictedProduct.isEmbedding_coe_of_top {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] : Topology.IsEmbedding DFunLike.coe

theorem RestrictedProduct.isEmbedding_coe_of_bot {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] : Topology.IsEmbedding DFunLike.coe

theorem RestrictedProduct.continuous_rng_of_principal {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] {S : Set ι} {X : Type u_3} [TopologicalSpace X] {f : X → RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) (Filter.principal S)} : Continuous f ↔ Continuous (DFunLike.coe ∘ f)

theorem RestrictedProduct.continuous_rng_of_top {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] {X : Type u_3} [TopologicalSpace X] {f : X → RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) ⊤} : Continuous f ↔ Continuous (DFunLike.coe ∘ f)

theorem RestrictedProduct.continuous_rng_of_bot {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] {X : Type u_3} [TopologicalSpace X] {f : X → RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) ⊥} : Continuous f ↔ Continuous (DFunLike.coe ∘ f)

theorem RestrictedProduct.continuous_rng_of_principal_iff_forall {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] {S : Set ι} {X : Type u_3} [TopologicalSpace X] {f : X → RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) (Filter.principal S)} : Continuous f ↔ ∀ (i : ι), Continuous ((fun (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) (Filter.principal S)) => x i) ∘ f)

def RestrictedProduct.homeoTop {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] : ((i : ι) → ↑(A i)) ≃ₜ RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) ⊤

The obvious bijection between Πʳ i, [R i, A i]_[⊤] and Π i, A i is a homeomorphism.

Equations

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

def RestrictedProduct.homeoBot {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] : ((i : ι) → R i) ≃ₜ RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) ⊥

The obvious bijection between Πʳ i, [R i, A i]_[⊥] and Π i, R i is a homeomorphism.

Equations

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

theorem RestrictedProduct.weaklyLocallyCompactSpace_of_principal {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] {S : Set ι} [∀ (i : ι), WeaklyLocallyCompactSpace (R i)] (hS : Filter.cofinite ≤ Filter.principal S) (hAcompact : ∀ i ∈ S, IsCompact (A i)) : WeaklyLocallyCompactSpace (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) (Filter.principal S))

Assume that S is a subset of ι with finite complement, that each R i is weakly locally compact, and that A i is compact for all i ∈ S. Then the restricted product Πʳ i, [R i, A i]_[𝓟 S] is locally compact.

Note: we spell "S has finite complement" as cofinite ≤ 𝓟 S.

instance RestrictedProduct.instWeaklyLocallyCompactSpacePrincipalOfFactLeFilterCofiniteOfCompactSpaceElem {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] {S : Set ι} [∀ (i : ι), WeaklyLocallyCompactSpace (R i)] [hS : Fact (Filter.cofinite ≤ Filter.principal S)] [hAcompact : ∀ (i : ι), CompactSpace ↑(A i)] : WeaklyLocallyCompactSpace (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) (Filter.principal S))

Topological facts in the general case

theorem RestrictedProduct.topologicalSpace_eq_iSup {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} (𝓕 : Filter ι) [(i : ι) → TopologicalSpace (R i)] : topologicalSpace R A 𝓕 = ⨆ (S : Set ι), ⨆ (hS : 𝓕 ≤ Filter.principal S), TopologicalSpace.coinduced (inclusion R A hS) (topologicalSpace R A (Filter.principal S))

theorem RestrictedProduct.continuous_dom {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} {𝓕 : Filter ι} [(i : ι) → TopologicalSpace (R i)] {X : Type u_3} [TopologicalSpace X] {f : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕 → X} : Continuous f ↔ ∀ (S : Set ι) (hS : 𝓕 ≤ Filter.principal S), Continuous (f ∘ inclusion R A hS)

The universal property of the topology on the restricted product: a map from Πʳ i, [R i, A i]_[𝓕] is continuous iff its restriction to each Πʳ i, [R i, A i]_[𝓟 s] (with 𝓕 ≤ 𝓟 s) is continuous.

See also RestrictedProduct.continuous_dom_prod_left.

theorem RestrictedProduct.isEmbedding_inclusion_principal {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} {𝓕 : Filter ι} [(i : ι) → TopologicalSpace (R i)] {S : Set ι} (hS : 𝓕 ≤ Filter.principal S) : Topology.IsEmbedding (inclusion R A hS)

theorem RestrictedProduct.isEmbedding_inclusion_top {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} {𝓕 : Filter ι} [(i : ι) → TopologicalSpace (R i)] : Topology.IsEmbedding (inclusion R A ⋯)

theorem RestrictedProduct.isEmbedding_structureMap {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} {𝓕 : Filter ι} [(i : ι) → TopologicalSpace (R i)] : Topology.IsEmbedding (structureMap R A 𝓕)

Π i, A i has the subset topology from the restricted product.

Topological facts in the case where 𝓕 = cofinite and all A is are open

The classical restricted product, associated to the cofinite filter, satisfies more topological properties when each A i is an open subset of R i. The key fact is that each Πʳ i, [R i, A i]_[𝓟 S] (with S cofinite) then embeds as an open subset in Πʳ i, [R i, A i].

This allows us to prove a "universal property with parameters", expressing that for any arbitrary topolgical space X (of "parameters"), the product X × Πʳ i, [R i, A i] is still the inductive limit of the X × Πʳ i, [R i, A i]_[𝓟 S] for S cofinite.

This fact, which is not true for a general inductive limit, will allow us to prove continuity of functions of two variables (e.g algebraic operations), which would otherwise be inaccessible.

theorem RestrictedProduct.isOpen_forall_imp_mem_of_principal {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] (hAopen : ∀ (i : ι), IsOpen (A i)) {S : Set ι} (hS : Filter.cofinite ≤ Filter.principal S) {p : ι → Prop} : IsOpen {f : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) (Filter.principal S) | ∀ (i : ι), p i → ↑f i ∈ A i}

theorem RestrictedProduct.isOpen_forall_mem_of_principal {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] (hAopen : ∀ (i : ι), IsOpen (A i)) {S : Set ι} (hS : Filter.cofinite ≤ Filter.principal S) : IsOpen {f : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) (Filter.principal S) | ∀ (i : ι), ↑f i ∈ A i}

theorem RestrictedProduct.isOpen_forall_imp_mem {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] (hAopen : ∀ (i : ι), IsOpen (A i)) {p : ι → Prop} : IsOpen {f : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) Filter.cofinite | ∀ (i : ι), p i → ↑f i ∈ A i}

theorem RestrictedProduct.isOpen_forall_mem {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] (hAopen : ∀ (i : ι), IsOpen (A i)) : IsOpen {f : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) Filter.cofinite | ∀ (i : ι), ↑f i ∈ A i}

theorem RestrictedProduct.isOpenEmbedding_inclusion_principal {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] (hAopen : ∀ (i : ι), IsOpen (A i)) {S : Set ι} (hS : Filter.cofinite ≤ Filter.principal S) : Topology.IsOpenEmbedding (inclusion R A hS)

theorem RestrictedProduct.isOpenEmbedding_structureMap {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] (hAopen : ∀ (i : ι), IsOpen (A i)) : Topology.IsOpenEmbedding (structureMap R A Filter.cofinite)

Π i, A i is homeomorphic to an open subset of the restricted product.

theorem RestrictedProduct.nhds_eq_map_inclusion {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] (hAopen : ∀ (i : ι), IsOpen (A i)) {S : Set ι} (hS : Filter.cofinite ≤ Filter.principal S) (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) (Filter.principal S)) : nhds (inclusion R A hS x) = Filter.map (inclusion R A hS) (nhds x)

theorem RestrictedProduct.nhds_eq_map_structureMap {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] (hAopen : ∀ (i : ι), IsOpen (A i)) (x : (i : ι) → ↑(A i)) : nhds (structureMap R A Filter.cofinite x) = Filter.map (structureMap R A Filter.cofinite) (nhds x)

theorem RestrictedProduct.weaklyLocallyCompactSpace_of_cofinite {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] (hAopen : ∀ (i : ι), IsOpen (A i)) [∀ (i : ι), WeaklyLocallyCompactSpace (R i)] (hAcompact : ∀ᶠ (i : ι) in Filter.cofinite, IsCompact (A i)) : WeaklyLocallyCompactSpace (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) Filter.cofinite)

If each R i is weakly locally compact, each A i is open, and all but finitely many A is are also compact, then the restricted product Πʳ i, [R i, A i] is weakly locally compact.

instance RestrictedProduct.instWeaklyLocallyCompactSpaceCofiniteOfFactForallIsOpenOfCompactSpaceElem {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] [hAopen : Fact (∀ (i : ι), IsOpen (A i))] [∀ (i : ι), WeaklyLocallyCompactSpace (R i)] [hAcompact : ∀ (i : ι), CompactSpace ↑(A i)] : WeaklyLocallyCompactSpace (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) Filter.cofinite)

theorem RestrictedProduct.continuous_dom_prod_right {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] (hAopen : ∀ (i : ι), IsOpen (A i)) {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] {f : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) Filter.cofinite × Y → X} : Continuous f ↔ ∀ (S : Set ι) (hS : Filter.cofinite ≤ Filter.principal S), Continuous (f ∘ Prod.map (inclusion R A hS) id)

The universal property with parameters of the topology on the restricted product: for any topological space Y of "parameters", a map from (Πʳ i, [R i, A i]) × Y is continuous iff its restriction to each (Πʳ i, [R i, A i]_[𝓟 S]) × Y (with S cofinite) is continuous.

theorem RestrictedProduct.continuous_dom_prod_left {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] (hAopen : ∀ (i : ι), IsOpen (A i)) {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] {f : Y × RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) Filter.cofinite → X} : Continuous f ↔ ∀ (S : Set ι) (hS : Filter.cofinite ≤ Filter.principal S), Continuous (f ∘ Prod.map id (inclusion R A hS))

The universal property with parameters of the topology on the restricted product: for any topological space Y of "parameters", a map from Y × Πʳ i, [R i, A i] is continuous iff its restriction to each Y × Πʳ i, [R i, A i]_[𝓟 S] (with S cofinite) is continuous.

theorem RestrictedProduct.continuous_dom_prod {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] (hAopen : ∀ (i : ι), IsOpen (A i)) {R' : ι → Type u_3} {A' : (i : ι) → Set (R' i)} [(i : ι) → TopologicalSpace (R' i)] (hAopen' : ∀ (i : ι), IsOpen (A' i)) {X : Type u_4} [TopologicalSpace X] {f : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) Filter.cofinite × RestrictedProduct (fun (i : ι) => R' i) (fun (i : ι) => A' i) Filter.cofinite → X} : Continuous f ↔ ∀ (S : Set ι) (hS : Filter.cofinite ≤ Filter.principal S), Continuous (f ∘ Prod.map (inclusion R A hS) (inclusion R' A' hS))

A map from Πʳ i, [R i, A i] × Πʳ i, [R' i, A' i] is continuous iff its restriction to each Πʳ i, [R i, A i]_[𝓟 S] × Πʳ i, [R' i, A' i]_[𝓟 S] (with S cofinite) is continuous.

This is the key result for continuity of multiplication and addition.

theorem RestrictedProduct.continuous_dom_pi {ι : Type u_1} {n : Type u_3} [Fintype n] {X : Type u_4} [TopologicalSpace X] {A : n → ι → Type u_5} [(j : n) → (i : ι) → TopologicalSpace (A j i)] {C : (j : n) → (i : ι) → Set (A j i)} (hCopen : ∀ (j : n) (i : ι), IsOpen (C j i)) {f : ((j : n) → RestrictedProduct (fun (i : ι) => A j i) (fun (i : ι) => C j i) Filter.cofinite) → X} : Continuous f ↔ ∀ (S : Set ι) (hS : Filter.cofinite ≤ Filter.principal S), Continuous (f ∘ Pi.map fun (x : n) => inclusion (A x) (C x) hS)

A finitary (instead of binary) version of continuous_dom_prod.

Compatibility properties between algebra and topology

instance RestrictedProduct.instContinuousInvCoe {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} {𝓕 : Filter ι} [(i : ι) → TopologicalSpace (R i)] [(i : ι) → Inv (R i)] [∀ (i : ι), InvMemClass (S i) (R i)] [∀ (i : ι), ContinuousInv (R i)] : ContinuousInv (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

instance RestrictedProduct.instContinuousNegCoe {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} {𝓕 : Filter ι} [(i : ι) → TopologicalSpace (R i)] [(i : ι) → Neg (R i)] [∀ (i : ι), NegMemClass (S i) (R i)] [∀ (i : ι), ContinuousNeg (R i)] : ContinuousNeg (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

instance RestrictedProduct.instContinuousConstSMulCoe {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} {𝓕 : Filter ι} [(i : ι) → TopologicalSpace (R i)] {G : Type u_4} [(i : ι) → SMul G (R i)] [∀ (i : ι), SMulMemClass (S i) G (R i)] [∀ (i : ι), ContinuousConstSMul G (R i)] : ContinuousConstSMul G (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

instance RestrictedProduct.instContinuousConstVAddCoe {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} {𝓕 : Filter ι} [(i : ι) → TopologicalSpace (R i)] {G : Type u_4} [(i : ι) → VAdd G (R i)] [∀ (i : ι), VAddMemClass (S i) G (R i)] [∀ (i : ι), ContinuousConstVAdd G (R i)] : ContinuousConstVAdd G (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

instance RestrictedProduct.instContinuousMulCoePrincipal {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} {T : Set ι} [(i : ι) → TopologicalSpace (R i)] [(i : ι) → Mul (R i)] [∀ (i : ι), MulMemClass (S i) (R i)] [∀ (i : ι), ContinuousMul (R i)] : ContinuousMul (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) (Filter.principal T))

instance RestrictedProduct.instContinuousAddCoePrincipal {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} {T : Set ι} [(i : ι) → TopologicalSpace (R i)] [(i : ι) → Add (R i)] [∀ (i : ι), AddMemClass (S i) (R i)] [∀ (i : ι), ContinuousAdd (R i)] : ContinuousAdd (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) (Filter.principal T))

instance RestrictedProduct.instContinuousSMulCoePrincipal {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} {T : Set ι} [(i : ι) → TopologicalSpace (R i)] {G : Type u_4} [TopologicalSpace G] [(i : ι) → SMul G (R i)] [∀ (i : ι), SMulMemClass (S i) G (R i)] [∀ (i : ι), ContinuousSMul G (R i)] : ContinuousSMul G (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) (Filter.principal T))

instance RestrictedProduct.instContinuousVAddCoePrincipal {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} {T : Set ι} [(i : ι) → TopologicalSpace (R i)] {G : Type u_4} [TopologicalSpace G] [(i : ι) → VAdd G (R i)] [∀ (i : ι), VAddMemClass (S i) G (R i)] [∀ (i : ι), ContinuousVAdd G (R i)] : ContinuousVAdd G (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) (Filter.principal T))

instance RestrictedProduct.instIsTopologicalGroupCoePrincipal {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} {T : Set ι} [(i : ι) → TopologicalSpace (R i)] [(i : ι) → Group (R i)] [∀ (i : ι), SubgroupClass (S i) (R i)] [∀ (i : ι), IsTopologicalGroup (R i)] : IsTopologicalGroup (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) (Filter.principal T))

instance RestrictedProduct.instIsTopologicalAddGroupCoePrincipal {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} {T : Set ι} [(i : ι) → TopologicalSpace (R i)] [(i : ι) → AddGroup (R i)] [∀ (i : ι), AddSubgroupClass (S i) (R i)] [∀ (i : ι), IsTopologicalAddGroup (R i)] : IsTopologicalAddGroup (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) (Filter.principal T))

instance RestrictedProduct.instIsTopologicalRingCoePrincipal {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} {T : Set ι} [(i : ι) → TopologicalSpace (R i)] [(i : ι) → Ring (R i)] [∀ (i : ι), SubringClass (S i) (R i)] [∀ (i : ι), IsTopologicalRing (R i)] : IsTopologicalRing (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) (Filter.principal T))

theorem RestrictedProduct.nhds_zero_eq_map_ofPre {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} {T : Set ι} [(i : ι) → TopologicalSpace (R i)] [(i : ι) → Zero (R i)] [∀ (i : ι), ZeroMemClass (S i) (R i)] (hBopen : ∀ (i : ι), IsOpen ↑(B i)) (hT : Filter.cofinite ≤ Filter.principal T) : nhds (inclusion R (fun (i : ι) => ↑(B i)) hT 0) = Filter.map (inclusion R (fun (i : ι) => ↑(B i)) hT) (nhds 0)

theorem RestrictedProduct.nhds_zero_eq_map_structureMap {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → TopologicalSpace (R i)] [(i : ι) → Zero (R i)] [∀ (i : ι), ZeroMemClass (S i) (R i)] (hBopen : ∀ (i : ι), IsOpen ↑(B i)) : nhds (structureMap R (fun (i : ι) => ↑(B i)) Filter.cofinite 0) = Filter.map (structureMap R (fun (i : ι) => ↑(B i)) Filter.cofinite) (nhds 0)

instance RestrictedProduct.instContinuousMulCoeCofinite {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → TopologicalSpace (R i)] [hBopen : Fact (∀ (i : ι), IsOpen ↑(B i))] [(i : ι) → Mul (R i)] [∀ (i : ι), MulMemClass (S i) (R i)] [∀ (i : ι), ContinuousMul (R i)] : ContinuousMul (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) Filter.cofinite)

instance RestrictedProduct.instContinuousAddCoeCofinite {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → TopologicalSpace (R i)] [hBopen : Fact (∀ (i : ι), IsOpen ↑(B i))] [(i : ι) → Add (R i)] [∀ (i : ι), AddMemClass (S i) (R i)] [∀ (i : ι), ContinuousAdd (R i)] : ContinuousAdd (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) Filter.cofinite)

instance RestrictedProduct.continuousSMul {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → TopologicalSpace (R i)] [hBopen : Fact (∀ (i : ι), IsOpen ↑(B i))] {G : Type u_4} [TopologicalSpace G] [(i : ι) → SMul G (R i)] [∀ (i : ι), SMulMemClass (S i) G (R i)] [∀ (i : ι), ContinuousSMul G (R i)] : ContinuousSMul G (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) Filter.cofinite)

instance RestrictedProduct.continuousVAdd {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → TopologicalSpace (R i)] [hBopen : Fact (∀ (i : ι), IsOpen ↑(B i))] {G : Type u_4} [TopologicalSpace G] [(i : ι) → VAdd G (R i)] [∀ (i : ι), VAddMemClass (S i) G (R i)] [∀ (i : ι), ContinuousVAdd G (R i)] : ContinuousVAdd G (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) Filter.cofinite)

instance RestrictedProduct.isTopologicalGroup {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → TopologicalSpace (R i)] [hBopen : Fact (∀ (i : ι), IsOpen ↑(B i))] [(i : ι) → Group (R i)] [∀ (i : ι), SubgroupClass (S i) (R i)] [∀ (i : ι), IsTopologicalGroup (R i)] : IsTopologicalGroup (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) Filter.cofinite)

instance RestrictedProduct.isTopologicalAddGroup {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → TopologicalSpace (R i)] [hBopen : Fact (∀ (i : ι), IsOpen ↑(B i))] [(i : ι) → AddGroup (R i)] [∀ (i : ι), AddSubgroupClass (S i) (R i)] [∀ (i : ι), IsTopologicalAddGroup (R i)] : IsTopologicalAddGroup (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) Filter.cofinite)

instance RestrictedProduct.isTopologicalRing {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → TopologicalSpace (R i)] [hBopen : Fact (∀ (i : ι), IsOpen ↑(B i))] [(i : ι) → Ring (R i)] [∀ (i : ι), SubringClass (S i) (R i)] [∀ (i : ι), IsTopologicalRing (R i)] : IsTopologicalRing (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) Filter.cofinite)

theorem RestrictedProduct.locallyCompactSpace_of_group {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → TopologicalSpace (R i)] [hBopen : Fact (∀ (i : ι), IsOpen ↑(B i))] [(i : ι) → Group (R i)] [∀ (i : ι), SubgroupClass (S i) (R i)] [∀ (i : ι), IsTopologicalGroup (R i)] [∀ (i : ι), LocallyCompactSpace (R i)] (hBcompact : ∀ᶠ (i : ι) in Filter.cofinite, IsCompact ↑(B i)) : LocallyCompactSpace (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) Filter.cofinite)

Assume that each R i is a locally compact group with A i an open subgroup. Assume also that all but finitely many A is are compact. Then the restricted product Πʳ i, [R i, A i] is a locally compact group.

theorem RestrictedProduct.locallyCompactSpace_of_addGroup {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → TopologicalSpace (R i)] [hBopen : Fact (∀ (i : ι), IsOpen ↑(B i))] [(i : ι) → AddGroup (R i)] [∀ (i : ι), AddSubgroupClass (S i) (R i)] [∀ (i : ι), IsTopologicalAddGroup (R i)] [∀ (i : ι), LocallyCompactSpace (R i)] (hBcompact : ∀ᶠ (i : ι) in Filter.cofinite, IsCompact ↑(B i)) : LocallyCompactSpace (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) Filter.cofinite)

Assume that each R i is a locally compact additive group with A i an open subgroup. Assume also that all but finitely many A is are compact. Then the restricted product Πʳ i, [R i, A i] is a locally compact additive group.

instance RestrictedProduct.instLocallyCompactSpaceCoeCofiniteOfSubgroupClassOfIsTopologicalGroupOfCompactSpaceSubtypeMem {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → TopologicalSpace (R i)] [hBopen : Fact (∀ (i : ι), IsOpen ↑(B i))] [(i : ι) → Group (R i)] [∀ (i : ι), SubgroupClass (S i) (R i)] [∀ (i : ι), IsTopologicalGroup (R i)] [hAcompact : ∀ (i : ι), CompactSpace ↥(B i)] : LocallyCompactSpace (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) Filter.cofinite)

instance RestrictedProduct.instLocallyCompactSpaceCoeCofiniteOfAddSubgroupClassOfIsTopologicalAddGroupOfCompactSpaceSubtypeMem {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → TopologicalSpace (R i)] [hBopen : Fact (∀ (i : ι), IsOpen ↑(B i))] [(i : ι) → AddGroup (R i)] [∀ (i : ι), AddSubgroupClass (S i) (R i)] [∀ (i : ι), IsTopologicalAddGroup (R i)] [hAcompact : ∀ (i : ι), CompactSpace ↥(B i)] : LocallyCompactSpace (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) Filter.cofinite)

theorem RestrictedProduct.map_continuous {ι₁ : Type u_3} {ι₂ : Type u_4} (R₁ : ι₁ → Type u_5) (R₂ : ι₂ → Type u_6) [(i : ι₁) → TopologicalSpace (R₁ i)] [(i : ι₂) → TopologicalSpace (R₂ i)] {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} {A₁ : (i : ι₁) → Set (R₁ i)} {A₂ : (i : ι₂) → Set (R₂ i)} (f : ι₂ → ι₁) (hf : Filter.Tendsto f 𝓕₂ 𝓕₁) (φ : (j : ι₂) → R₁ (f j) → R₂ j) (hφ : ∀ᶠ (j : ι₂) in 𝓕₂, Set.MapsTo (φ j) (A₁ (f j)) (A₂ j)) (φ_cont : ∀ (j : ι₂), Continuous (φ j)) : Continuous (map R₁ R₂ f hf φ hφ)