# Blueprint for the Liquid Tensor Experiment

## 1.3 Spaces of convergent power series

We will now construct the central example of profinitely filtered pseudo-normed groups with $$r'$$-action of $$T^{-1}$$.

Definition 1.3.1
#

Let $$r' {\gt} 0$$ be a real number, and let $$S$$ be a finite set. Denote by $$\overline{\mathcal L}_{r'}(S)$$ the set

$\left\{ \left( \sum _{n \ge 1} a_{n,s} T^n \in T\mathbb {Z}[[T]]\right)_{s \in S} \, \middle \vert \, \sum _{n \ge 1, s \in S} |a_{n,s}| (r')^n {\lt} \infty \right\} .$

Note that $$\overline{\mathcal L}_{r'}(S)$$ is naturally a pseudo-normed group with filtration given by

$\overline{\mathcal L}_{r'}(S)_{\le c} = \left\{ \left( \sum _{n \ge 1} a_{n,s} T^n \right)_{s \in S} \middle \vert \sum _{n \ge 1, s \in S} |a_{n,s}| (r')^n \le c \right\} .$

Lemma 1.3.2
#

Let $$r' {\gt} 0$$ and $$c \ge 0$$ be real numbers, and let $$S$$ be a finite set. The space $$\overline{\mathcal L}_{r'}(S)_{\le c}$$ is the profinite limit of the finite sets

$\overline{\mathcal L}_{r'}(S)_{\le c, \le N} = \left\{ \left( \sum _{n \ge 1} a_{n,s} T^n \right)_{s \in S} \middle \vert \sum _{1 \le n \le N, s \in S} |a_{n,s}| (r')^n \le c \right\}$

This endows $$\overline{\mathcal L}_{r'}(S)_{\le c}$$ with the profinite topology. In particular, it is a profinitely filtered pseudo-normed group.

Proof

Formalised, but omitted from this text.

For the remainder of this subsection, let $$r' {\gt} 0, c \ge 0$$ be real numbers, and let $$S$$ be a finite set.

Definition 1.3.3
#

There is a natural action of $$T^{-1}$$ on $$\overline{\mathcal L}_{r'}(S)$$, via

$T^{-1} \cdot \left( \sum _{n \ge 1} a_{n,s} T^n \right)_{s \in S} = \left( \sum _{n \ge 1} a_{n+1,s} T^n \right)_{s \in S}.$

Lemma 1.3.4
#

The natural action of $$T^{-1}$$ on $$\overline{\mathcal L}_{r'}(S)$$ restricts to continuous maps

$T^{-1} \cdot \_ \colon \overline{\mathcal L}_r(S)_{\le c} \longrightarrow \overline{\mathcal L}_r(S)_{\le c/r'}.$

In particular, $$\overline{\mathcal L}_{r'}(S)$$ has an $$r'$$-action of $$T^{-1}$$.

Proof

Formalised, but omitted from this text.