Exercise 4.15 (Scott 1981, PRG-19, Lecture IV) — a maximal (and a least) fixed

point

(For set theorists.) Let f : |𝒟| → |𝒟| be a monotone function on the elements of a domain. Then f has a maximal fixed point — a fixed point that cannot be extended to a larger one — and (consequently) a least fixed point.

Maximal fixed point (Zorn). Consider the set S = {x ∣ x ⊑ f(x)} of post-fixed points. It is non-empty (⊥ ∈ S) and every chain C ⊆ S has an upper bound in S: its union ⊔C (Exercise 1.24's chainUnion, Scott's "use 2.11 to remark ⊔C ∈ |𝒟|") is again post-fixed, since each x ∈ C has x ⊑ f(x) ⊑ f(⊔C). By Zorn's Lemma (zorn_le₀) S has a maximal element m. Then m is a fixed point: m ⊑ f(m) (it is in S) and f(m) ⊑ m (because f(m) ∈ S too, by monotonicity, and m is maximal). It is maximal among fixed points (exists_maximal_fixedPoint).

Least fixed point. Having produced some fixed point m, we have f(m) ⊑ m, so Exercise 4.13(1) (the monotone-only intersection construction monoFix) applies and yields the least fixed point fix(f) = ⋂{x ∣ f(x) ⊑ x} ⊑ m (exists_least_fixedPoint).

This is the explicitly classical exercise (Zorn ⟹ Classical.choice), exactly like Exercise 1.24; the chainUnion construction itself is choice-free.

theorem Domain.Neighborhood.NeighborhoodSystem.chainUnion_le {α : Type u_1} {V : NeighborhoodSystem α} (C : Set V.Element) (hne : C.Nonempty) (hchain : IsChain (fun (x1 x2 : V.Element) => x1 ≤ x2) C) {y : V.Element} (hy : ∀ x ∈ C, x ≤ y) : V.chainUnion C hne hchain ≤ y

chainUnion C is the least upper bound of the chain: an upper bound y of every member dominates it.

theorem Domain.Neighborhood.NeighborhoodSystem.exists_maximal_fixedPoint {α : Type u_1} {V : NeighborhoodSystem α} (f : V.Element → V.Element) (hf : Monotone f) : ∃ (m : V.Element), f m = m ∧ ∀ (y : V.Element), f y = y → m ≤ y → y ≤ m

Exercise 4.15 (Scott 1981, PRG-19). A monotone f : |𝒟| → |𝒟| has a maximal fixed point: some m with f(m) = m that admits no strictly larger fixed point.

theorem Domain.Neighborhood.NeighborhoodSystem.exists_least_fixedPoint {α : Type u_1} {V : NeighborhoodSystem α} (f : V.Element → V.Element) (hf : Monotone f) : ∃ (b : V.Element), f b = b ∧ ∀ (y : V.Element), f y = y → b ≤ y

Exercise 4.15 (Scott 1981, PRG-19). A monotone f : |𝒟| → |𝒟| has a least fixed point. (Having a maximal fixed point m gives a pre-fixed point f(m) ⊑ m; Exercise 4.13(1)'s monoFix then constructs the least fixed point ⋂{x ∣ f(x) ⊑ x}.)