Zulip Chat Archive

Stream: maths

Topic: Support in order ideal


view this post on Zulip Aaron Anderson (Sep 01 2020 at 21:52):

I was thinking about how to formalize Hahn series, starting by defining the underlying type, which are functions from a linear order with well-founded support.

view this post on Zulip Aaron Anderson (Sep 01 2020 at 21:54):

I realized that that construction, very similar to finsupp, would involve proving a lot of the same properties as constructing functions of compact support: namely that well-founded subsets of an order, or subsets of compact subsets of a topological space, form an order ideal.

view this post on Zulip Aaron Anderson (Sep 01 2020 at 21:54):

At least, this is enough to define addition and pointwise multiplication (but not Hahn series multiplication).

view this post on Zulip Adam Topaz (Sep 01 2020 at 21:55):

Another approach would be to use some universal property :) (It's the spherical completion, or something.)

view this post on Zulip Adam Topaz (Sep 01 2020 at 21:55):

And define it as a quotient of some giant inductive type.

view this post on Zulip Aaron Anderson (Sep 01 2020 at 21:57):

Anyway, I'm wondering if it's worth formalizing the abstract idea of functions-with-support-in-some-ideal, or if these are the only two interesting cases (we're probably not refactoring finsupp around this idea) and the analogy should just be carried out by copy-paste.

view this post on Zulip Aaron Anderson (Sep 01 2020 at 22:01):

Adam Topaz said:

And define it as a quotient of some giant inductive type.

I'd much rather have a definition with hands-on data that is at least analogous to finsupp, considering the pervasiveness of finsupp.

view this post on Zulip Adam Topaz (Sep 01 2020 at 22:02):

Of course, I agree.

view this post on Zulip Adam Topaz (Sep 01 2020 at 22:02):

If you ever want to actually use series, this is necessary :)

view this post on Zulip Aaron Anderson (Sep 01 2020 at 22:04):

Once that's in, we can go to town on universal properties and abstractions :)

view this post on Zulip Kevin Buzzard (Sep 02 2020 at 06:31):

Something related to Hahn series come up in the theory of valuations, but not seriously enough that we need to formalise them in the perfectoid project. I'll try to dig up the reference, it was early in Wedhorn's notes


Last updated: May 09 2021 at 11:09 UTC