Zulip Chat Archive

Stream: condensed mathematics

Topic: condensed rings of laurent series


Johan Commelin (Jul 22 2021 at 06:44):

We need to formalize the definition of Z((T))r(S)\Z((T))_r(S) and Z((T))r(S)c\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 (Aug 26 2021 at 19:13):

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 (Aug 26 2021 at 20:16):

@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 (Aug 26 2021 at 22:01):

The coefficients are continuous functions on S

Adam Topaz (Aug 26 2021 at 22:01):

That's right

Adam Topaz (Aug 26 2021 at 22:02):

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


Last updated: Dec 20 2023 at 11:08 UTC