lil fixpoint lemma

fixpoint.txt

Suppose ℂ is a ω-cocomplete category: it has colimits of any
diagram that is a functor ω → ℂ. Suppose ℂ has an initial object ⊥.
Suppose F is a functor ℂ → ℂ that preserves all ω-colimits.

Let U : ω → ℂ be the diagram

       !      F!       F²
    ⊥ → F(⊥) → F²(⊥) → ⋯

Lemma: If we have a map m : FA → A, then we can construct a map colim U → A.
Proof: By the UMP of the colimit, it suffices to find fₙ that make

      ⊥ → F(⊥) → F²(⊥) → ⋯
    f₀↓  f₁↓    f₂↓
      A === A ===== A ===== ⋯

commute. Check that the inductive definition
    f₀ = !
    fₙ₊₁ = m ∘ F(fₙ)
works. ∎

(iirc this ought to be first bit of demonstrating that colim U is the carrier of the initial F-algebra)

Corollary: Suppose we have a functor S : ω → ℂ and a map
    ϕ : colim (F ∘ S) → (colim S).
Then there exists a map
    (colim U) → (colim S)
Proof:
Since F preserve colimits, we can transform ϕ into a map
    F(colim S) → (colim S)
Apply lemma with A := colim S.

Bringing this down to earth:

Claim: If fₙ : P → P are monotone ω-continuous maps from an ω-CPO to itself,
       and aᵢ is a fair scheduling of the naturals, then
       supₜ (⋃ₙ fₙ)ᵗ (⊥) ≤ supₜ (f_{aₜ} ∘ ⋯ f_{a₀}) (⊥)
Proof:
Let ℂ be P. Let F be ⋃ₙ fₙ. Let S(t) = (f_{aₜ} ∘ ⋯ f_{a₀}) (⊥)
Then the thing we're trying to do is obtain a morphism (colim U) → (colim S).
U is "running all the rules concurrently, repeatedly"
S is "running all the rules chaotically, but fairly"
F preserves ω-colimits because fₙ are ω-continuous.
The remaining proof obligation is ϕ. We must show
    colim (F ∘ S) → (colim S)
so it suffices to use the UMP of the colimit on the left and show
    ∀n. F(S(n)) ≤ supₜ (f_{aₜ} ∘ ⋯ f_{a₀}) (⊥)
i.e.
    ∀s. F((f_{aₛ} ∘ ⋯ f_{a₀})(t)) ≤ supₜ (f_{aₜ} ∘ ⋯ f_{a₀}) (⊥)
i.e. all we need is
    ∀s,n. fₙ((f_{aₛ} ∘ ⋯ f_{a₀})(t)) ≤ supₜ (f_{aₜ} ∘ ⋯ f_{a₀}) (⊥)
But this is just seeing that, if we're at stage s, and we hit our
result with fₙ, there is *some* future stage t that exceeds fₙ applied
to step s. This follows from fairness. ∎