condensed rings of laurent series

Stream: condensed mathematics

[Johan Commelin]

We need to formalize the definition of $\Z((T))_r(S)$ and $\Z((T))_r(S)_{\le c}$ on the bottom half of p36 of Analytic.pdf. For now, I would formalize them just as types. The former should get a comm_ring instance. We can turn it into a functor (and condensed ring) later.

[Aaron Anderson]

Am I correct in reading that this is just a subring of the ring of Laurent series over a ring of continuous functions?

[Johan Commelin]

@Aaron Anderson It is indeed a subring of converging Laurent series. I don't know what you mean by "over a ring of ctu functions"

[Adam Topaz]

The coefficients are continuous functions on S

[Adam Topaz]

That's right

[Adam Topaz]

But to relate it to the other defs, we probably want to do the colimit of the limit trick.