## Stream: maths

### Topic: Support in order ideal

#### 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.

#### 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.

#### Aaron Anderson (Sep 01 2020 at 21:54):

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

#### Adam Topaz (Sep 01 2020 at 21:55):

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

#### Adam Topaz (Sep 01 2020 at 21:55):

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

#### 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.

#### Aaron Anderson (Sep 01 2020 at 22:01):

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.

#### Adam Topaz (Sep 01 2020 at 22:02):

Of course, I agree.

#### Adam Topaz (Sep 01 2020 at 22:02):

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

#### Aaron Anderson (Sep 01 2020 at 22:04):

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

#### 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