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