Lecture VI — Theorem 6.9 (Scott 1981, PRG-19): homomorphisms out of a fixed

point

THEOREM 6.9. If the functor T is continuous on maps (Definition 6.8) and if D ≅ T(D), so in particular D is a T-algebra, then for any T-algebra k : T(E) → E there is a homomorphism h : D → E.

Scott's proof. Let i : T(D) → D be the isomorphism making D a T-algebra and j : D → T(D) its inverse. A homomorphism h : D → E must satisfy h ∘ i = k ∘ T(h), equivalently the fixed-point equation

h = k ∘ T(h) ∘ j.

The operator λh. k ∘ T(h) ∘ j on the strict function space (D →⊥ E) is approximable: the inner λh. T(h) is approximable precisely by Definition 6.8 (ContinuousOnMaps), and post- and pre-composition with the fixed maps k, j is approximable too. Hence by the Lecture IV fixed-point theory (Theorem 4.1, fixElement) it has a least fixed point h, the desired homomorphism.

What the formalization does

We work over Scott's strict function space (D →⊥ E) = strictFun D.sys E.sys (Exercise 5.10), exactly matching Definition 6.8.

• homOpComp — the strict composite g ↦ k ∘ g ∘ j as a StrictMap. Strictness of the composite uses that j is strict (any isomorphism of domains preserves ⊥, isStrict_of_comp_eq_id) and k is strict (a morphism of Scott's strict category; carried as a hypothesis), so T(h) ∘ j and then k ∘ (T(h) ∘ j) stay strict.
• homOp — the post/pre-composition map (T(D) →⊥ T(E)) → (D →⊥ E), g ↦ k ∘ g ∘ j, built by Exercise 2.8's ofMono. Its decisive action lemma homOp_apply_filter says homOp(f̂) = (k ∘ f ∘ j)^ for every strict f; it is proved by reducing (through the strict representation strictFunEquiv) to single step neighbourhoods [X, Z], where the "finite factoring" is just N := [Y₁, Y₂].
• The operator is Op = homOp ∘ Φ, where Φ is Definition 6.8's witness that λf. T(f) is approximable. Its fixElement represents the strict map h; the fixed-point equation (toElementMap_fixElement) unwinds — via Φ's defining property and homOp_apply_filter — to h = k ∘ T(h) ∘ j, which rearranges (using j ∘ i = I) to the homomorphism square h ∘ i = k ∘ T(h).

The conclusion is Nonempty {g : AlgHom ⟨D, i⟩ B // IsStrict g.hom} — Scott's existence statement, recording that the homomorphism is itself a strict map (it is toStrictMap of the fixed point), which the uniqueness half of Theorem 6.14 consumes. Extracting Φ from the Prop-valued ContinuousOnMaps is done by Exists.elim while proving a Prop, so it stays choice-free (#print axioms ⊆ {propext, Quot.sound}).

General helper lemmas (strictness and monotonicity of composition).

theorem Domain.Neighborhood.isStrict_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {a : ApproximableMap V₁ V₂} {b : ApproximableMap V₀ V₁} (ha : Exercise510.IsStrict a) (hb : Exercise510.IsStrict b) : Exercise510.IsStrict (a.comp b)

The composite of strict maps is strict: (a ∘ b)(⊥) = a(b(⊥)) = a(⊥) = ⊥.

theorem Domain.Neighborhood.isStrict_of_comp_eq_id {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {a : ApproximableMap V₁ V₀} {b : ApproximableMap V₀ V₁} (h : a.comp b = ApproximableMap.idMap V₀) : Exercise510.IsStrict a

If a ∘ b = I then a is strict: any (split) iso preserves ⊥.

theorem Domain.Neighborhood.comp_mono_gen {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {a a' : ApproximableMap V₁ V₂} {b b' : ApproximableMap V₀ V₁} (ha : a ≤ a') (hb : b ≤ b') : a.comp b ≤ a'.comp b'

Composition is monotone in both arguments (general arities).

theorem Domain.Neighborhood.toStrictMap_mono {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {φ φ' : (Exercise510.strictFun V₀ V₁).Element} (h : φ ≤ φ') : Exercise510.toStrictMap φ ≤ Exercise510.toStrictMap φ'

toStrictMap is monotone.

theorem Domain.Neighborhood.toStrictFilter_mono {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {f f' : Exercise510.StrictMap V₀ V₁} (h : f ≤ f') : Exercise510.toStrictFilter f ≤ Exercise510.toStrictFilter f'

toStrictFilter is monotone.

theorem Domain.Neighborhood.toStrictFilter_toStrictMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (φ : (Exercise510.strictFun V₀ V₁).Element) : Exercise510.toStrictFilter (Exercise510.toStrictMap φ) = φ

toStrictFilter ∘ toStrictMap = id (the left inverse of the strict-function-space representation; the mirror of toStrictMap_toStrictFilter).

The post/pre-composition operator on strict function spaces.

def Domain.Neighborhood.homOpComp (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) (g : Exercise510.StrictMap (T.obj D).sys (T.obj E).sys) : Exercise510.StrictMap D.sys E.sys

The strict composite g ↦ k ∘ g ∘ j : (T(D) →⊥ T(E)) → (D →⊥ E).

Equations

• Domain.Neighborhood.homOpComp T D E j k hj hk g = ⟨k.comp ((↑g).comp j), ⋯⟩

theorem Domain.Neighborhood.homOpComp_mono (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) {g g' : Exercise510.StrictMap (T.obj D).sys (T.obj E).sys} (hgg : g ≤ g') : homOpComp T D E j k hj hk g ≤ homOpComp T D E j k hj hk g'

def Domain.Neighborhood.homOp (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 (T.obj D).sys (T.obj E).sys) (Exercise510.strictFun D.sys E.sys)

The operator λg. k ∘ g ∘ j as an approximable map between the strict function spaces, built by Exercise 2.8 (ofMono) from its values on finite elements.

Equations

• One or more equations did not get rendered due to their size.

theorem Domain.Neighborhood.homOp_rel (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) {N : Set (Exercise510.StrictMap (T.obj D).sys (T.obj E).sys)} {M : Set (Exercise510.StrictMap D.sys E.sys)} : (homOp T D E j k hj hk).rel N M ↔ ∃ (hN : (Exercise510.strictFun (T.obj D).sys (T.obj E).sys).mem N), (Exercise510.toStrictFilter (homOpComp T D E j k hj hk (Exercise510.toStrictMap ((Exercise510.strictFun (T.obj D).sys (T.obj E).sys).principal hN)))).mem M

theorem Domain.Neighborhood.homOp_apply_filter (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) (g : Exercise510.StrictMap (T.obj D).sys (T.obj E).sys) : (homOp T D E j k hj hk).toElementMap (Exercise510.toStrictFilter g) = Exercise510.toStrictFilter (homOpComp T D E j k hj hk g)

Action lemma. homOp realizes the composite g ↦ k ∘ g ∘ j on filters of strict maps: homOp(ĝ) = (k ∘ g ∘ j)^. Proved by reducing to single step neighbourhoods through the strict representation.

Theorem 6.9.

theorem Domain.Neighborhood.nonempty_algHom_of_continuousOnMaps (T : Endofunctor DomainObj) (hT : ContinuousOnMaps T) {D : DomainObj} (iso : Iso (T.obj D) D) (B : TAlgebra T) (hk : Exercise510.IsStrict B.str) : Nonempty { g : AlgHom { carrier := D, str := iso.hom } B // Exercise510.IsStrict g.hom }

Theorem 6.9 (Scott 1981, PRG-19). If T is continuous on maps and D ≅ T(D) (so D is a T-algebra via i : T(D) → D), then for any T-algebra B = (E, k) with k strict there is a homomorphism D → E. The homomorphism is the least fixed point of λh. k ∘ T(h) ∘ j.