The topology of a restricted product

General facts about the restricted-product topology, which Mathlib defines as the final topology over the principal stages Πʳ i, [R i, A i]_[𝓟 S]. A set is open if and only if its preimage in every principal stage is open: this is the Prop-valued form of Mathlib's universal property RestrictedProduct.continuous_dom. Inserting a single factor is continuous, the analogue of continuous_mulSingle for Pi types.

The restricted-product topology is finer than the topology induced from the full product Π i, R i, and in general strictly finer. The clearest instance is a family of discrete spaces with reference sets of at most one element: every principal stage indexed by a cofinite set, and hence the restricted product itself, is discrete (discreteTopology_restrictedProduct), whereas the full product of discrete groups with infinitely many nontrivial factors is not. So for discrete groups with trivial reference subgroups, infinitely many of them nontrivial, the coercion to the full product is not inducing (not_isInducing_coe_bot): the restricted-product topology is not the induced one. This is the reason continuity of a map into a restricted product does not follow from continuity of its coordinates.

References

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

theorem TauCeti.isOpen_restrictedProduct_iff {ι : Type u} {R : ι → Type v} {A : (i : ι) → Set (R i)} {𝓕 : Filter ι} [(i : ι) → TopologicalSpace (R i)] {s : Set (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕)} : IsOpen s ↔ ∀ (S : Set ι) (hS : 𝓕 ≤ Filter.principal S), IsOpen (RestrictedProduct.inclusion R A hS ⁻¹' s)

A subset of a restricted product is open if and only if its preimage in every principal stage Πʳ i, [R i, A i]_[𝓟 S] with 𝓕 ≤ 𝓟 S is open.

theorem TauCeti.continuous_restrictedProduct_mulSingle {ι : Type u} {S : ι → Type w} {G : ι → Type v} [(i : ι) → SetLike (S i) (G i)] (B : (i : ι) → S i) [DecidableEq ι] [(i : ι) → One (G i)] [∀ (i : ι), OneMemClass (S i) (G i)] [(i : ι) → TopologicalSpace (G i)] (i : ι) : Continuous (RestrictedProduct.mulSingle B i)

Inserting a single factor into a restricted product is continuous.

theorem TauCeti.discreteTopology_restrictedProduct_principal {ι : Type u} {R : ι → Type v} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] {S : Set ι} (hS : Sᶜ.Finite) (hA : ∀ i ∈ S, (A i).Subsingleton) (hR : ∀ i ∉ S, DiscreteTopology (R i)) : DiscreteTopology (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) (Filter.principal S))

A principal stage Πʳ i, [R i, A i]_[𝓟 S] with S cofinite is discrete when the reference sets A i for i ∈ S have at most one element and the spaces R i for i ∉ S are discrete: on the stage the coordinates in S are determined by the reference sets, and only finitely many coordinates remain free.

theorem TauCeti.discreteTopology_restrictedProduct {ι : Type u} {R : ι → Type v} {A : (i : ι) → Set (R i)} [(i : ι) → TopologicalSpace (R i)] [∀ (i : ι), DiscreteTopology (R i)] (hA : ∀ (i : ι), (A i).Subsingleton) : DiscreteTopology (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) Filter.cofinite)

A restricted product of discrete spaces relative to reference sets with at most one element is discrete: every principal stage indexed by a cofinite set is, and the restricted-product topology is the final topology over these stages.

instance TauCeti.discreteTopology_restrictedProduct_bot {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] [(i : ι) → TopologicalSpace (G i)] [∀ (i : ι), DiscreteTopology (G i)] : DiscreteTopology (RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑⊥) Filter.cofinite)

A restricted product of discrete groups relative to the trivial reference subgroups is discrete.

theorem TauCeti.not_isInducing_coe_bot {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] [(i : ι) → TopologicalSpace (G i)] [∀ (i : ι), DiscreteTopology (G i)] (hG : {i : ι | Nontrivial (G i)}.Infinite) : ¬Topology.IsInducing DFunLike.coe

For discrete groups with trivial reference subgroups, infinitely many of them nontrivial, the restricted product does not carry the topology induced from the full product: the restricted product is discrete, but every neighbourhood of 1 in the full product contains an element supported at a single index with nontrivial group. The restricted-product topology is therefore strictly finer than the induced one in general, and continuity of a map into a restricted product does not follow from continuity of its coordinates.