transfinite compositions

Stream: maths

[Reid Barton]

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]

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]

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]

But this seems a bit awkward.

[Reid Barton]

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

[Johannes Hölzl]

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?

[Reid Barton]

Hmm, interesting

[Reid Barton]

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]

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

[Reid Barton]

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

[Reid Barton]

Ah, I found the source.

[Johannes Hölzl]

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

[Johannes Hölzl]

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]

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