Restricted products of sets, groups and rings, and their topology

We define the restricted product of R : ι → Type* of types, relative to a family of subsets A : (i : ι) → Set (R i) and a filter 𝓕 : Filter ι. This is the set of all x : Π i, R i such that the set {j | x j ∈ A j} belongs to 𝓕. We denote it by Πʳ i, [R i, A i]_[𝓕].

The main case of interest, which we shall refer to as the "classical restricted product", is that of 𝓕 = cofinite. Recall that this is the filter of all subsets of ι, which are cofinite in the sense that they have finite complement. Hence, the associated restricted product is the set of all x : Π i, R i such that x j ∈ A j for all but finitely many js. We denote it simply by Πʳ i, [R i, A i].

Another notable case is that of the principal filter 𝓕 = 𝓟 s corresponding to some subset s of ι. The associated restricted product Πʳ i, [R i, A i]_[𝓟 s] is the set of all x : Π i, R i such that x j ∈ A j for all j ∈ s. Put another way, this is just (Π i ∈ s, A i) × (Π i ∉ s, R i), modulo the obvious isomorphism.

We endow these types with the obvious algebraic structures, as well as their natural topology, which we describe below. We also show various compatibility results.

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: the restricted product of a family R of types, relative to a family A of subsets and a filter 𝓕 on the indexing set. This is denoted Πʳ i, [R i, A i]_[𝓕], or simply Πʳ i, [R i, A i] when 𝓕 = cofinite.
• RestrictedProduct.instDFunLike: interpret an element of Πʳ i, [R i, A i]_[𝓕] as an element of Π i, R i using the DFunLike machinery.
• RestrictedProduct.structureMap: the inclusion map from Π i, A i to Πʳ i, [R i, A i]_[𝓕].
• RestrictedProduct.topologicalSpace: the TopologicalSpace instance on Πʳ 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.

Notation

• Πʳ i, [R i, A i]_[𝓕] is RestrictedProduct R A 𝓕.
• Πʳ i, [R i, A i] is RestrictedProduct R A cofinite.

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

Definition and elementary maps

def RestrictedProduct {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) (𝓕 : Filter ι) : Type (max u_1 u_2)

The restricted product of a family R : ι → Type* of types, relative to subsets A : (i : ι) → Set (R i) and the filter 𝓕 : Filter ι, is the set of all x : Π i, R i such that the set {j | x j ∈ A j} belongs to 𝓕. We denote it by Πʳ i, [R i, A i]_[𝓕].

The most common use case is with 𝓕 = cofinite, in which case the restricted product is the set of all x : Π i, R i such that x j ∈ A j for all but finitely many j. We denote it simply by Πʳ i, [R i, A i].

Similarly, if S is a principal filter, the restricted product Πʳ i, [R i, A i]_[𝓟 s] is the set of all x : Π i, R i such that ∀ j ∈ S, x j ∈ A j.

Equations

• RestrictedProduct R A 𝓕 = { x : (i : ι) → R i // ∀ᶠ (i : ι) in 𝓕, x i ∈ A i }

def RestrictedProduct.«termΠʳ_,[_,_]_[_]» : Lean.ParserDescr

Πʳ i, [R i, A i]_[𝓕] is RestrictedProduct R A 𝓕.

Equations

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

def RestrictedProduct.«termΠʳ_,[_,_]_[_]».«delab_app.RestrictedProduct» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

def RestrictedProduct.«termΠʳ_,[_,_]».«delab_app.RestrictedProduct» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

def RestrictedProduct.«termΠʳ_,[_,_]» : Lean.ParserDescr

Πʳ i, [R i, A i] is RestrictedProduct R A cofinite.

Equations

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

instance RestrictedProduct.instDFunLike {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 : Filter ι} : DFunLike (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕) ι R

Equations

• RestrictedProduct.instDFunLike R A = { coe := fun (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕) (i : ι) => ↑x i, coe_injective' := ⋯ }

theorem RestrictedProduct.range_coe {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 : Filter ι} : Set.range DFunLike.coe = {x : (a : ι) → R a | ∀ᶠ (i : ι) in 𝓕, x i ∈ A i}

theorem RestrictedProduct.range_coe_principal {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {S : Set ι} : Set.range DFunLike.coe = S.pi A

def RestrictedProduct.structureMap {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) (𝓕 : Filter ι) (x : (i : ι) → ↑(A i)) : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕

The structure map of the restricted product is the obvious inclusion from Π i, A i into Πʳ i, [R i, A i]_[𝓕].

Equations

• RestrictedProduct.structureMap R A 𝓕 x = ⟨fun (i : ι) => ↑(x i), ⋯⟩

def RestrictedProduct.inclusion {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 𝓖 : Filter ι} (h : 𝓕 ≤ 𝓖) (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓖) : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕

If 𝓕 ≤ 𝓖, the restricted product Πʳ i, [R i, A i]_[𝓖] is naturally included in Πʳ i, [R i, A i]_[𝓕]. This is the corresponding map.

Equations

• RestrictedProduct.inclusion R A h x = ⟨⇑x, ⋯⟩

theorem RestrictedProduct.inclusion_eq_id {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) (𝓕 : Filter ι) : inclusion R A ⋯ = id

theorem RestrictedProduct.exists_inclusion_eq_of_eventually {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 𝓖 : Filter ι} (h : 𝓕 ≤ 𝓖) {x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕} (hx𝓖 : ∀ᶠ (i : ι) in 𝓖, x i ∈ A i) : ∃ (x' : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓖), inclusion R A h x' = x

theorem RestrictedProduct.exists_structureMap_eq_of_forall {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 : Filter ι} {x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕} (hx : ∀ (i : ι), ↑x i ∈ A i) : ∃ (x' : (i : ι) → ↑(A i)), structureMap R A 𝓕 x' = x

theorem RestrictedProduct.range_inclusion {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 𝓖 : Filter ι} (h : 𝓕 ≤ 𝓖) : Set.range (inclusion R A h) = {x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕 | ∀ᶠ (i : ι) in 𝓖, x i ∈ A i}

theorem RestrictedProduct.range_structureMap {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 : Filter ι} : Set.range (structureMap R A 𝓕) = {f : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕 | ∀ (i : ι), ↑f i ∈ A i}

Algebraic instances on restricted products

In this section, we endow the restricted product with its algebraic instances. To avoid any unnecessary coercions, we use subobject classes for the subset B i of each R i.

instance RestrictedProduct.instOneCoeOfOneMemClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → One (R i)] [∀ (i : ι), OneMemClass (S i) (R i)] : One (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instOneCoeOfOneMemClass R = { one := ⟨fun (x : ι) => 1, ⋯⟩ }

instance RestrictedProduct.instZeroCoeOfZeroMemClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → Zero (R i)] [∀ (i : ι), ZeroMemClass (S i) (R i)] : Zero (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instZeroCoeOfZeroMemClass R = { zero := ⟨fun (x : ι) => 0, ⋯⟩ }

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

Equations

• RestrictedProduct.instInvCoeOfInvMemClass R = { inv := fun (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) => ⟨fun (i : ι) => (x i)⁻¹, ⋯⟩ }

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

Equations

• RestrictedProduct.instNegCoeOfNegMemClass R = { neg := fun (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) => ⟨fun (i : ι) => -x i, ⋯⟩ }

instance RestrictedProduct.instMulCoeOfMulMemClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → Mul (R i)] [∀ (i : ι), MulMemClass (S i) (R i)] : Mul (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instMulCoeOfMulMemClass R = { mul := fun (x y : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) => ⟨fun (i : ι) => x i * y i, ⋯⟩ }

instance RestrictedProduct.instAddCoeOfAddMemClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → Add (R i)] [∀ (i : ι), AddMemClass (S i) (R i)] : Add (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instAddCoeOfAddMemClass R = { add := fun (x y : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) => ⟨fun (i : ι) => x i + y i, ⋯⟩ }

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

Equations

• RestrictedProduct.instSMulCoeOfSMulMemClass R = { smul := fun (g : G) (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) => ⟨fun (i : ι) => g • x i, ⋯⟩ }

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

Equations

• RestrictedProduct.instVAddCoeOfVAddMemClass R = { vadd := fun (g : G) (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) => ⟨fun (i : ι) => g +ᵥ x i, ⋯⟩ }

instance RestrictedProduct.instDivCoeOfSubgroupClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → DivInvMonoid (R i)] [∀ (i : ι), SubgroupClass (S i) (R i)] : Div (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instDivCoeOfSubgroupClass R = { div := fun (x y : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) => ⟨fun (i : ι) => x i / y i, ⋯⟩ }

instance RestrictedProduct.instSubCoeOfAddSubgroupClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → SubNegMonoid (R i)] [∀ (i : ι), AddSubgroupClass (S i) (R i)] : Sub (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instSubCoeOfAddSubgroupClass R = { sub := fun (x y : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) => ⟨fun (i : ι) => x i - y i, ⋯⟩ }

instance RestrictedProduct.instPowCoeNatOfSubmonoidClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → Monoid (R i)] [∀ (i : ι), SubmonoidClass (S i) (R i)] : Pow (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) ℕ

Equations

• RestrictedProduct.instPowCoeNatOfSubmonoidClass R = { pow := fun (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) (n : ℕ) => ⟨fun (i : ι) => x i ^ n, ⋯⟩ }

instance RestrictedProduct.instPowCoeIntOfSubgroupClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → DivInvMonoid (R i)] [∀ (i : ι), SubgroupClass (S i) (R i)] : Pow (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) ℤ

Equations

• RestrictedProduct.instPowCoeIntOfSubgroupClass R = { pow := fun (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) (n : ℤ) => ⟨fun (i : ι) => x i ^ n, ⋯⟩ }

instance RestrictedProduct.instNatCastCoeOfAddSubmonoidWithOneClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → AddMonoidWithOne (R i)] [∀ (i : ι), AddSubmonoidWithOneClass (S i) (R i)] : NatCast (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instNatCastCoeOfAddSubmonoidWithOneClass R = { natCast := fun (n : ℕ) => ⟨fun (x : ι) => ↑n, ⋯⟩ }

instance RestrictedProduct.instIntCastCoeOfSubringClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → Ring (R i)] [∀ (i : ι), SubringClass (S i) (R i)] : IntCast (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instIntCastCoeOfSubringClass R = { intCast := fun (n : ℤ) => ⟨fun (x : ι) => ↑n, ⋯⟩ }

instance RestrictedProduct.instAddGroupCoeOfAddSubgroupClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → AddGroup (R i)] [∀ (i : ι), AddSubgroupClass (S i) (R i)] : AddGroup (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instAddGroupCoeOfAddSubgroupClass R = Function.Injective.addGroup (fun (f : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance RestrictedProduct.instGroupCoeOfSubgroupClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → Group (R i)] [∀ (i : ι), SubgroupClass (S i) (R i)] : Group (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instGroupCoeOfSubgroupClass R = Function.Injective.group (fun (f : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance RestrictedProduct.instRingCoeOfSubringClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → Ring (R i)] [∀ (i : ι), SubringClass (S i) (R i)] : Ring (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instRingCoeOfSubringClass R = Function.Injective.ring (fun (f : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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_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)

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.

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)