## Stream: maths

### Topic: transfinite compositions

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


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

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

#### Reid Barton (Sep 17 2018 at 21:46):

But this seems a bit awkward.

#### Reid Barton (Sep 17 2018 at 21:47):

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

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

Hmm, interesting

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

#### Reid Barton (Sep 17 2018 at 21:53):

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

#### Reid Barton (Sep 17 2018 at 21:54):

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

#### Reid Barton (Sep 17 2018 at 21:57):

Ah, I found the source.

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

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

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