Zulip Chat Archive

Stream: maths

Topic: transfinite compositions


view this post on Zulip Reid Barton (Sep 17 2018 at 21:34):

Suppose P is a complete lattice. I can define an increasing sequence of finite length in P either as a subtype of a function type or as an inductive type, as shown below.

import order.complete_lattice
open lattice
variables {P : Type} [complete_lattice P]

def seq1 (n : ) : Type := {f : fin (n+1)  P //  i j, i  j  f i  f j}
inductive seq2 (a : P) : P    Type
| nil : seq2 a 0
| cons : Π b b' n, seq2 b n  b  b'  seq2 b' (n+1)

view this post on Zulip Reid Barton (Sep 17 2018 at 21:35):

The first one generalizes easily to any ordinal (or any well-ordered set). Is there a way to generalize the second?
I mention that P is a complete lattice because I'm happy to assume (if it helps) that at each limit stage, the value of the sequence is equal to the sup of all the previous values.

view this post on Zulip Reid Barton (Sep 17 2018 at 21:46):

The only way I can think to handle limit ordinal stages is to ask for an increasing sequence of every smaller ordinal length, such that for any α ≤ β, the sequence of length α is a prefix of the sequence of length β

view this post on Zulip Reid Barton (Sep 17 2018 at 21:46):

But this seems a bit awkward.

view this post on Zulip Reid Barton (Sep 17 2018 at 21:47):

(What I'm really trying to do is model https://ncatlab.org/nlab/show/transfinite+composition)

view this post on Zulip Johannes Hölzl (Sep 17 2018 at 21:50):

I'm not sure if this is what you're looking for. The following is used in Isabelle to model transfinite recursion:

inductive_set iterates :: "('a ⇒ 'a) ⇒ 'a set" for f :: "'a ⇒ 'a" where
| step: "x ∈ iterates f ⟹ f x ∈ iterates f"
| Sup: "chain (≤) M ⟹ ∀x∈M. x ∈ iterates f ⟹ Sup M ∈ iterates f"

Maybe you can use a similar approach?

view this post on Zulip Reid Barton (Sep 17 2018 at 21:51):

Hmm, interesting

view this post on Zulip Reid Barton (Sep 17 2018 at 21:52):

Indeed we basically always construct such transfinite compositions by iterating some construction at successor stages, and taking a sup/colimit at limit stages

view this post on Zulip Reid Barton (Sep 17 2018 at 21:53):

What kind of thing is M there? a subset of 'a?

view this post on Zulip Reid Barton (Sep 17 2018 at 21:54):

and chain (≤) means it's totally ordered?

view this post on Zulip Reid Barton (Sep 17 2018 at 21:57):

Ah, I found the source.

view this post on Zulip Johannes Hölzl (Sep 17 2018 at 21:57):

Yes, M is a subset of 'a and chain (≤) M says that M is totally ordered

view this post on Zulip Johannes Hölzl (Sep 17 2018 at 22:00):

the interesting part is that iterates is a chain in itself, so it contains its supremum, which is the fixed point of f. In this theory 'a is a chain complete partial order (i.e. all non-empty chains have a supremum)

view this post on Zulip Reid Barton (Sep 17 2018 at 23:15):

One thing that occurs to me is that my finite sequences are themselves partially ordered by "extends", and the finite prefixes of a countable sequence form a chain


Last updated: May 12 2021 at 07:17 UTC