Support in order ideal

Stream: maths

[Aaron Anderson]

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]

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]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Aaron Anderson]

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]

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.

[Adam Topaz]

Of course, I agree.

[Adam Topaz]

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

[Aaron Anderson]

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

[Kevin Buzzard]

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