Lecture VI — Theorem 6.16 (Scott 1981, PRG-19): an initial algebra embeds in

every solution

THEOREM 6.16. If on the category of domains and strict approximable maps the functor T is continuous on maps, and if D is an initial T-algebra, then for any system E ≅ T(E) we have D ⊴ E.

Scott's proof. By Theorem 6.9 there is a homomorphism h : D → E and (running 6.9 the other way) a homomorphism g : E → D. The composite g ∘ h : D → D is a homomorphism of the initial algebra D, hence equals I_D by uniqueness. By Lemma 6.15 it remains to show h ∘ g ⊑ I_E.

Writing i : T(D) → D, j : D → T(D) for D's isomorphism (Lambek, Proposition 6.7) and u : T(E) → E, v : E → T(E) for E's, the proof of 6.9 produces h and g as the least fixed points of h = u ∘ T(h) ∘ j and g = i ∘ T(g) ∘ v. Setting h₀ = ⊥, g₀ = ⊥ and hₙ₊₁ = u ∘ T(hₙ) ∘ j, gₙ₊₁ = i ∘ T(gₙ) ∘ v, one computes hₙ₊₁ ∘ gₙ₊₁ = u ∘ T(hₙ ∘ gₙ) ∘ v (using j ∘ i = I_{T(D)}), so kₙ := hₙ ∘ gₙ is the approximant chain of the operator k ↦ u ∘ T(k) ∘ v. Therefore h ∘ g = ⊔ₙ (hₙ ∘ gₙ) is its least fixed point, and since I_E is a fixed point of that operator, h ∘ g ⊑ I_E.

What the formalization does

Everything reuses Theorem 6.9's operator (homOp T D E j k) ∘ Φ on Scott's strict function space (D →⊥ E) (Exercise 5.10). The per-step computation is isolated as opStep. The three approximant chains H, G, K (for h, g, k) and the ladder identity H n ∘ G n = K n give h ∘ g = k (the least fixed point of u ∘ T(·) ∘ v), which is ⊑ I_E because I_E is a fixed point. Lemma 6.15 (trianglelefteq_of_projectionPair) then closes D ⊴ E.

General helpers.

theorem Domain.Neighborhood.opStep (T : Endofunctor DomainObj) (D E : DomainObj) (j : ApproximableMap D.sys (T.obj D).sys) (k : ApproximableMap (T.obj E).sys E.sys) (hj : Exercise510.IsStrict j) (hk : Exercise510.IsStrict k) (Φ : ApproximableMap (Exercise510.strictFun D.sys E.sys) (Exercise510.strictFun (T.obj D).sys (T.obj E).sys)) (hΦ : ∀ (f : Exercise510.StrictMap D.sys E.sys), ↑(Exercise510.toStrictMap (Φ.toElementMap (Exercise510.toStrictFilter f))) = T.map ↑f) (x : (Exercise510.strictFun D.sys E.sys).Element) : ↑(Exercise510.toStrictMap (((homOp T D E j k hj hk).comp Φ).toElementMap x)) = k.comp (ApproximableMap.comp (T.map ↑(Exercise510.toStrictMap x)) j)

The per-step computation of Theorem 6.9's operator. For the operator Op = (k ∘ · ∘ j) ∘ Φ on the strict function space, Op(x) is the strict map k ∘ T(toStrictMap x) ∘ j. This is the content of homOp_apply_filter plus the defining property hΦ of the Definition 6.8 witness Φ.

theorem Domain.Neighborhood.botStrict_rel {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {X : Set α} {Y : Set β} : (↑(Exercise510.toStrictMap (Exercise510.strictFun V₀ V₁).bot)).rel X Y ↔ V₀.mem X ∧ Y = V₁.master

The strict map represented by ⊥ of the strict function space relates X to Y exactly when X is a neighbourhood and Y is the master output: it is the constant-⊥ (least) strict map.

Theorem 6.16.

theorem Domain.Neighborhood.trianglelefteq_of_isInitial (T : Endofunctor DomainObj) (hT : ContinuousOnMaps T) (Dalg : TAlgebra T) (hinit : IsInitial Dalg) (E : DomainObj) (isoE : Iso (T.obj E) E) : Dalg.carrier.sys ⊴ E.sys

Theorem 6.16 (Scott 1981, PRG-19). If T is continuous on maps and D is an initial T-algebra, then for any system E ≅ T(E) we have D ⊴ E: the initial algebra embeds as a subdomain of every solution of the domain equation.