Continuity of maps into a restricted product

The topology of a restricted product Πʳ i, [R i, A i] is the final topology over its principal stages Πʳ i, [R i, A i]_[𝓟 T], T cofinite, and is in general strictly finer than the topology induced from the full product Π i, R i. Continuity of a map into a restricted product therefore does not follow from continuity of its coordinates. This file gives continuity and convergence criteria for maps controlled by one principal stage, and a stagewise continuity criterion using the universal property of the restricted product.

• continuous_restrictedProduct_iff_of_forall_mem: a map whose values all lie in one principal stage of the filter is continuous exactly when it is continuous into the full product.
• tendsto_restrictedProduct_iff_of_eventually_mem: for a family eventually in one principal stage, convergence to any point is equivalent to coordinatewise convergence.
• continuous_restrictedProduct_of_apply_eq_of_isOpen: for a finite set S of indices, a map recombining an arbitrary family of coordinates on S with a restricted-product element away from S is continuous, provided the reference sets away from S are open. Its domain is a product with a restricted-product factor, so the openness hypothesis is that of Mathlib's universal property with parameters, RestrictedProduct.continuous_dom_prod_left, and it is asked only at the indices outside S. This is the topological input for the inverse of the decomposition of a restricted product into the plain product over a finite set of indices times the restricted product away from it. The openness hypothesis cannot be dropped: see not_continuous_restrictedProduct_of_apply_eq_rat_bot.

References

• N. Bourbaki, General Topology.
• A. Weil, Basic Number Theory.

theorem TauCeti.continuous_restrictedProduct_iff_of_forall_mem {ι : Type u} {R : ι → Type v} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] {X : Type u_1} [TopologicalSpace X] {𝓕 : Filter ι} {f : X → RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕} {T : Set ι} (hT : 𝓕 ≤ Filter.principal T) (hf : ∀ (x : X), ∀ i ∈ T, (f x) i ∈ A i) : Continuous f ↔ Continuous fun (x : X) => ⇑(f x)

A map into a restricted product whose values all lie in a principal stage T of the filter is continuous exactly when it is continuous as a map into the full product Π i, R i.

theorem TauCeti.tendsto_restrictedProduct_iff_of_eventually_mem {ι : Type u} {R : ι → Type v} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] {X : Type u_1} {l : Filter X} {𝓕 : Filter ι} {f : X → RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕} {x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕} {T : Set ι} (hT : 𝓕 ≤ Filter.principal T) (hf : ∀ᶠ (a : X) in l, ∀ i ∈ T, (f a) i ∈ A i) : Filter.Tendsto f l (nhds x) ↔ ∀ (i : ι), Filter.Tendsto (fun (a : X) => (f a) i) l (nhds (x i))

For a family eventually lying in one principal stage of the filter, convergence in the restricted product to any point is equivalent to convergence of every coordinate. No openness assumption on the reference sets is needed.

theorem TauCeti.continuous_restrictedProduct_of_apply_eq_of_isOpen {ι : Type u} {R : ι → Type v} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] {S : Set ι} (hS : S.Finite) (hA : ∀ i ∉ S, IsOpen (A i)) {f : ((i : ↑S) → R ↑i) × RestrictedProduct (fun (j : { j : ι // j ∉ S }) => R ↑j) (fun (j : { j : ι // j ∉ S }) => A ↑j) Filter.cofinite → RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) Filter.cofinite} (hmem : ∀ (p : ((i : ↑S) → R ↑i) × RestrictedProduct (fun (j : { j : ι // j ∉ S }) => R ↑j) (fun (j : { j : ι // j ∉ S }) => A ↑j) Filter.cofinite) (i : ↑S), (f p) ↑i = p.1 i) (hnotMem : ∀ (p : ((i : ↑S) → R ↑i) × RestrictedProduct (fun (j : { j : ι // j ∉ S }) => R ↑j) (fun (j : { j : ι // j ∉ S }) => A ↑j) Filter.cofinite) (j : { j : ι // j ∉ S }), (f p) ↑j = p.2 j) : Continuous f

For a finite set S of indices, a map that recombines a family of coordinates on S with a restricted-product element away from S into an element of the full restricted product is continuous when the reference sets away from S are open. The map is pinned by its two coordinate formulas: on S it returns the given coordinate, and away from S it returns the coordinate of the given restricted-product element.