Zulip Chat Archive

Stream: maths

Topic: ordinals


view this post on Zulip Reid Barton (Oct 04 2018 at 18:00):

If I am interested in sequences indexed by {ααγ}\{\,\alpha \mid \alpha \le \gamma\,\} for varying ordinals γ\gamma, is it likely to be more convenient to just work with sequences indexed by arbitrary well-ordered sets?
The problem I found is that if you just write down { \a // \a \le \g }, it lives in the wrong universe.

view this post on Zulip Reid Barton (Oct 04 2018 at 18:05):

I think the alternative is to use quot.out to turn an ordinal into a well-ordered set of that order type, where in math I'd just use the set of smaller ordinals.

view this post on Zulip Reid Barton (Oct 04 2018 at 18:08):

But if I use quot.out then I basically get an arbitrary well-ordered set anyways, so I might as well just work with an arbitrary well-ordered set from the start, I guess.

view this post on Zulip Johannes Hölzl (Oct 04 2018 at 18:09):

Oh yes, I would expect that its far easier assume that γ is a type with well-order. And use the elements of the type as indices.

view this post on Zulip Kenny Lau (Oct 04 2018 at 18:10):

I wrote some code a month ago

view this post on Zulip Reid Barton (Oct 04 2018 at 18:10):

And if I use the variable name γ, then everyone is happy :)

view this post on Zulip Kenny Lau (Oct 04 2018 at 18:11):

I uploaded them here.

view this post on Zulip Reid Barton (Oct 04 2018 at 18:11):

Oh interesting, will take a look

view this post on Zulip Reid Barton (Oct 04 2018 at 18:15):

I'm going to need to take colimits indexed by these partially ordered sets of ordinals less than γ\gamma--that's why I need the type to live in the correct universe

view this post on Zulip Reid Barton (Oct 04 2018 at 18:16):

I think the ZFC stuff would also leave me in the wrong universe, though maybe I could prove once and for all that categories which admit small colimits also admit colimits by "categories in ZFC", or something like that...

view this post on Zulip Mario Carneiro (Oct 04 2018 at 18:58):

You can measure the cofinality of any preorder, I think. Maybe it's easier to work without even using well orders

view this post on Zulip Mario Carneiro (Oct 04 2018 at 18:59):

but yes, you almost certainly want to reason about ordered types rather than ordinals directly


Last updated: May 12 2021 at 08:14 UTC