Blueprint for the Liquid Tensor Experiment: Spaces of convergent power series

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.