Restricted products with non-open reference subgroups

Mathlib makes a restricted product of topological groups a topological group only when every reference subgroup is open (RestrictedProduct.isTopologicalGroup, under Fact (∀ i, IsOpen (A i))). This file shows that the hypothesis cannot be dropped: the restricted product Πʳ n : ℕ, [Multiplicative ℚ, ⊥] of copies of ℚ, with the topology of ℚ ⊆ ℝ and the trivial reference subgroup in every factor, does not have continuous multiplication. Additively it is the space of finitely supported rational sequences with the final topology over the finite-dimensional stages, and a final topology need not be compatible with products. That a strict inductive limit of topological groups need not be a topological group in the inductive-limit topology is classical; see Tatsuuma, Shimomura and Hirai.

The witness is the set W = {x | ∀ n ≥ 1, |x n| < |x 0 - √2 / (n + 1)|}, written additively. It is open, because on each stage only finitely many coordinates are free and the right-hand sides never vanish at a rational x 0, and it contains 0. But every neighbourhood of 0 contains t • e₀ for all rational t of small absolute value and s • eₙ for all rational s of small absolute value, and for n large and t rational close to √2 / (n + 1) the sum t • e₀ + s • eₙ escapes W.

Multiplication on this space factors through the inverse of the splitting restrictedProductSum of the restricted product over ℕ ⊕ ℕ into two restricted products, followed by the coordinatewise product of the two halves, which is continuous for every family. So that inverse is not continuous for this family either (not_continuous_restrictedProductSum_symm), although continuous_restrictedProductSum_symm makes it continuous once the reference subgroups are open; openness is a fact about the topology, not a limitation of that proof.

The same set W shows that recombining a coordinate at 0 with an element of the restricted product over the indices n ≠ 0 is not continuous (not_continuous_restrictedProduct_of_apply_eq_rat_bot): here the open neighbourhoods of 0 come from the plain product over {0} and from the restricted product away from 0, and the same choice of t and s escapes W. The inverse of the decomposition awayDecomposition of a restricted product into the product over a finite set of indices times the restricted product away from it is such a map, so it is not continuous when the reference subgroups away from that set are not open (not_continuous_awayDecomposition_symm); compare continuous_awayDecomposition_symm and continuous_restrictedProduct_of_apply_eq_of_isOpen.

The openness of the witness is checked stage by stage with isOpen_restrictedProduct_iff, and the neighbourhood argument uses continuous_restrictedProduct_mulSingle.

References

• N. Bourbaki, General Topology.
• N. Tatsuuma, H. Shimomura, T. Hirai, On group topologies and unitary representations of inductive limits of topological groups and the case of the group of diffeomorphisms, J. Math. Kyoto Univ. 38 (1998), 551–578.
• A. Weil, Basic Number Theory.

theorem TauCeti.not_continuousMul_restrictedProduct_rat_bot : ¬ContinuousMul (RestrictedProduct (fun (x : ℕ) => Multiplicative ℚ) (fun (x : ℕ) => ↑⊥) Filter.cofinite)

Multiplication on the restricted product Πʳ n : ℕ, [Multiplicative ℚ, ⊥] is not continuous: with the topology of ℚ ⊆ ℝ on each factor and the trivial, non-open, reference subgroup at every index, the restricted-product topology is not compatible with the group structure.

theorem TauCeti.not_isTopologicalGroup_restrictedProduct_rat_bot : ¬IsTopologicalGroup (RestrictedProduct (fun (x : ℕ) => Multiplicative ℚ) (fun (x : ℕ) => ↑⊥) Filter.cofinite)

The restricted product Πʳ n : ℕ, [Multiplicative ℚ, ⊥] is not a topological group: the hypothesis Fact (∀ i, IsOpen (A i)) of Mathlib's RestrictedProduct.isTopologicalGroup cannot be dropped.

theorem TauCeti.not_continuous_restrictedProductSum_symm : ¬Continuous ⇑(restrictedProductSum (fun (x : ℕ ⊕ ℕ) => ⊥) ⋯ ⋯).symm

The inverse of the splitting restrictedProductSum of a restricted product over a sum of index types is not continuous in general: for Πʳ k : ℕ ⊕ ℕ, [Multiplicative ℚ, ⊥], with the trivial, non-open, reference subgroup at every index, it is a discontinuous bijection. The openness hypothesis of continuous_restrictedProductSum_symm therefore cannot be dropped.

theorem TauCeti.not_continuous_restrictedProduct_of_apply_eq_rat_bot {f : ((↑{0} → Multiplicative ℚ) × RestrictedProductGroupAway {0} fun (x : ℕ) => ⊥) → RestrictedProductGroup fun (x : ℕ) => ⊥} (hmem : ∀ (p : (↑{0} → Multiplicative ℚ) × RestrictedProductGroupAway {0} fun (x : ℕ) => ⊥) (i : ↑{0}), (f p) ↑i = p.1 i) (hnotMem : ∀ (p : (↑{0} → Multiplicative ℚ) × RestrictedProductGroupAway {0} fun (x : ℕ) => ⊥) (j : { j : ℕ // j ∉ {0} }), (f p) ↑j = p.2 j) : ¬Continuous f

Recombining a coordinate at the index 0 with an element of the restricted product away from 0 is not continuous for Πʳ n : ℕ, [Multiplicative ℚ, ⊥]: every map (Π i : {0}, Multiplicative ℚ) × Πʳ n : {n // n ∉ {0}}, [Multiplicative ℚ, ⊥] → Πʳ n : ℕ, [Multiplicative ℚ, ⊥] that returns the coordinate of its first component on {0} and the coordinates of its second component away from {0} is discontinuous. So the openness hypothesis of continuous_restrictedProduct_of_apply_eq_of_isOpen on the reference subgroups away from the finite set cannot be dropped, and neither can the corresponding hypothesis for the inverse of the decomposition of a restricted product into the product over a finite set of indices times the restricted product away from it.

theorem TauCeti.not_continuous_awayDecomposition_symm : ¬Continuous ⇑(awayDecomposition {0} ⋯ fun (x : ℕ) => ⊥).symm

The inverse of the decomposition awayDecomposition of a restricted product along a finite set of indices is not continuous in general: for Πʳ n : ℕ, [Multiplicative ℚ, ⊥] and S = {0}, with the trivial, non-open, reference subgroup at every index, it is a discontinuous bijection. The openness hypothesis of continuous_awayDecomposition_symm on the reference subgroups away from S therefore cannot be dropped.