Section 5

Stream: condensed mathematics

[Filippo A. E. Nuccio]

I can't understand the definition of the Smith space $W$ in section 5 of analytic.pdf (in the "translation" of the extension of Corollary 5.4 to the condensed setting). I ended up figuring that there might be a typo, and actually $W=W_1$, although I still

• Can't figure out why there is no well-defined map $W\rightarrow\mathbb{R}$ giving by summing all $x_i$ (if $W=W_1=\bigcup_c c\cdot K$ where $K$ are the sequences in $[-1,1]$ absolutely summing to $\le 1$, it seems well-defined to me);

Then I wondered whether the issue might be that this well-defined map is non-continuous, and fell in the rabbit-hole of asking myself

• If $\ell^1$ is a subspace of $W$ (or of $W_1$ if they differ), and we want to pull-back via the inclusion $\ell^1\hookrightarrow W$, in which category are we pulling-back? If in "locally convex v.s.", then is this inclusion continue?

Has anyone thought about this?

[Johan Commelin]

@Filippo A. E. Nuccio Is this related to the Lean stuff you are working on, or just general curiousity?

[Filippo A. E. Nuccio]

No, it is related to general curiosity, trying to understand how things work.

[Filippo A. E. Nuccio]

But I will leave it for another time and go back to my laurent series!

[Johan Commelin]

We can still try to understand what is going on. I just wanted to understand the context. Because if this came up in relation to the Lean stuff, then I was surprised... I didn't expect a connection there.

[Johan Commelin]

I need to do some admin before I can look at this, though

[Filippo A. E. Nuccio]

Yes, I understood where your question came from. But don't worry, it is not very urgent.

[Filippo A. E. Nuccio]

I will probably do Lean and forget about this for today, at any rate.

[Filippo A. E. Nuccio]

(but of course, if you will have an idea, I will be more than happy :smile: )

[Peter Scholze]

@Filippo A. E. Nuccio Yes, $W=W_1$, that is a typo. Everything in sight is supposed to be considered as condensed $\mathbb R$-vector spaces, in particular the pullback. And the problem is that the map $W\to \mathbb R$ summing all $x_i$ is not continuous. Namely, any open subset of $W_{\leq 1}$ contains the basis vector $(0,\ldots,0,1,0,\ldots)$ (with $1$ in place $i$) for sufficiently large $i$.

[Filippo A. E. Nuccio]

Oh, thanks, I see. So, in particular, the inclusion $\ell^1\hookrightarrow W=W_1$ is continuous? Because otherwise I don't see how it would give rise to a morphism of condensed $\mathbb{R}$-v.s. along which I can pull-back.