Exercise 5.9 (Scott 1981, PRG-19, Lecture V)

Suppose f, g : 𝒟 → 𝒟 are approximable and f ∘ g = g ∘ f. Then:

• f and g have a least common fixed point x = f(x) = g(x) (commuting_least_common_fixed);
• if in addition f(⊥) = g(⊥), then fix(f) = fix(g) (fixElement_eq_of_commuting_bot);
• in particular fix(f) = fix(f²) (fixElement_iterTwice).

Construction. Let a = fix(f). Commutation makes g(a) a fixed point of f (f(g(a)) = g(f(a)) = g(a)), so a ⊑ g(a), and Exercise 4.7 produces the least fixed point of g above a, namely x = ⊔ₙ gⁿ(a). Each gⁿ(a) is again a fixed point of f (induction + commutation), and f preserves the directed union, so f(x) = x: x is a common fixed point. Any common fixed point w satisfies a = fix(f) ⊑ w and g(w) ⊑ w, so x ⊑ w by Exercise 4.7's leastness.

For the second part, commutation gives g(fⁿ(⊥)) = fⁿ⁺¹(⊥) once g(⊥) = f(⊥), so g(fix f) = ⊔ₙ fⁿ⁺¹(⊥) = fix f; symmetrically f(fix g) = fix g, whence fix f = fix g by leastness.

All maps and elements are choice-free; the equalities use only the order on |𝒟|.

theorem Domain.Neighborhood.ApproximableMap.commute_apply {α : Type u_1} {V : NeighborhoodSystem α} {f g : ApproximableMap V V} (hcomm : f.comp g = g.comp f) (x : V.Element) : f.toElementMap (g.toElementMap x) = g.toElementMap (f.toElementMap x)

Commutation f ∘ g = g ∘ f read elementwise: f(g(x)) = g(f(x)).

theorem Domain.Neighborhood.ApproximableMap.commuting_least_common_fixed {α : Type u_1} {V : NeighborhoodSystem α} {f g : ApproximableMap V V} (hcomm : f.comp g = g.comp f) : ∃ (x : V.Element), f.toElementMap x = x ∧ g.toElementMap x = x ∧ ∀ (w : V.Element), f.toElementMap w = w → g.toElementMap w = w → x ≤ w

Exercise 5.9 (Scott 1981, PRG-19). Commuting approximable maps have a least common fixed point x = f(x) = g(x).

theorem Domain.Neighborhood.ApproximableMap.iterElem_succ {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) (n : ℕ) : f.iterElem (n + 1) = f.toElementMap (f.iterElem n)

f.iterElem (n+1) = f(fⁿ(⊥)).

theorem Domain.Neighborhood.ApproximableMap.iterElem_zero' {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) : f.iterElem 0 = V.bot

theorem Domain.Neighborhood.ApproximableMap.fixElement_eq_of_commuting_bot {α : Type u_1} {V : NeighborhoodSystem α} {f g : ApproximableMap V V} (hcomm : f.comp g = g.comp f) (hbot : f.toElementMap V.bot = g.toElementMap V.bot) : f.fixElement = g.fixElement

Exercise 5.9 (Scott 1981, PRG-19). If f, g commute and f(⊥) = g(⊥), then fix(f) = fix(g).

theorem Domain.Neighborhood.ApproximableMap.iterElem_le_fixElement {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) (n : ℕ) : f.iterElem n ≤ f.fixElement

fⁿ(⊥) ⊑ fix(f).

theorem Domain.Neighborhood.ApproximableMap.comp_self_iterElem {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) (n : ℕ) : (f.comp f).iterElem n = f.iterElem (2 * n)

(f²)ⁿ(⊥) = f^{2n}(⊥).

theorem Domain.Neighborhood.ApproximableMap.fixElement_iterTwice {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) : f.fixElement = (f.comp f).fixElement

Exercise 5.9 (Scott 1981, PRG-19). In particular fix(f) = fix(f²): the f²-chain f^{2n}(⊥) is cofinal in the f-chain fⁿ(⊥), so the two least fixed points coincide.