关于带确界度量的无限乘积圆周空间∏ₙ=1^∞S¹的基本群的验证问询

我正在研究一个带确界度量的无限乘积圆周空间的基本群问题，想请各位帮忙验证我的思路是否正确：

背景设定 #

• 考虑欧氏度量下的单位圆周$S^1 \subseteq \mathbb{C}$，定义集合$X = \prod_{n=1}^\infty S^1$，并赋予确界度量：
  $$d_\infty: X \times X \to [0, 2],\ d_\infty((x_n){n=1}^\infty, (y_n){n=1}^\infty) = \sup_{n=1}^\infty d(x_n, y_n)$$
  显然$(X, d_\infty)$构成一个度量空间。

核心问题 #

这个空间的基本群$\pi_1(X)$是什么？

我的猜想与推理 #

我猜想$\pi_1(X)$等于群$G$，其中$G$的定义为：
$$G = {(a_n){n=1}^\infty \in \prod{n=1}^\infty\mathbb{Z} \mid \exists C \in \mathbb{Z}_{\geq 0},\ \forall n \in \mathbb{N} : |a_n| \leq C}$$

对应的路径我定义为：对于任意$(a_n){n=1}^\infty \in G$，映射$\varphi{(a_n){n=1}^\infty}: S^1 \to X$满足$\varphi{(a_n)_{n=1}^\infty}(z) = (z^{a_n})_{n=1}\infty$。

我得出这个猜想的依据是：

• 若$X$赋予乘积拓扑，它的基本群是$\prod_{n=1}^\infty\mathbb{Z}$；
• 而$G$恰好是$\prod_{n=1}^\infty\mathbb{Z}$的子群，其中元素对应的路径在$X$带确界度量的拓扑下仍然是连续的——这也是我认为$G$就是目标基本群的核心原因。

请问这个结论和推理过程是正确的吗？

备注：内容来源于stack exchange，提问作者Elia Immanuel Auer