Lecture VI — Definition 6.8 (Scott 1981, PRG-19): functors continuous on maps

DEFINITION 6.8. On the category of domains and strict approximable maps a functor T is continuous on maps if for any systems D and E the induced mapping λf. T(f) : (D →⊥ E) → (T(D) →⊥ T(E)) is approximable.

This is the continuity condition that powers Theorem 6.9 (existence of homomorphisms out of a fixed point D ≅ T(D)): the homomorphism equation h = k ∘ T(h) ∘ j is a fixed-point equation for the map λh. k ∘ T(h) ∘ j, and it has a solution precisely because λh. T(h) — hence the whole operator — is itself an approximable (so continuous) self-map of a function-space domain.

What the formalization uses

• The category and the functor. T is an Endofunctor DomainObj (Definition 6.3): an action T.obj on domains and T.map on the morphisms (here approximable maps, Theorem 2.5 laws).
• The strict function space (D →⊥ E). This is exactly Scott's domain on the left of the induced map. The project already constructs it in Exercise510.lean: strictFun D E is the neighbourhood system whose elements are the strict approximable maps (IsStrict f, i.e. f(⊥) = ⊥), with the representation strictFunEquiv : |D →⊥ E| ≃o StrictMap D E mirroring Theorem 3.10. So this Definition is stated over Scott's strict maps verbatim, not the full function space.
• "is approximable". In this framework a function between domains is approximable exactly when it is the elementwise action (toElementMap) of an approximable map (Proposition 2.2 / Theorem 3.10). So λf. T(f) being approximable is rendered as the existence of a witnessing Φ : (D →⊥ E) → (T(D) →⊥ T(E)) (an ApproximableMap between the two strict function-space domains) whose action reproduces T on the underlying maps — transported across the representation strictFunEquiv via toStrictFilter/toStrictMap.

Because the witnessing equation reads off the underlying map of a StrictMap, it automatically forces T.map f to be strict whenever f is (lemma ContinuousOnMaps.isStrict_map): a T continuous on maps does restrict to Scott's subcategory of strict maps, as required.

A design note on the category (strict maps vs. all maps)

Scott states 6.8 on the category of domains and strict maps, whereas the project's abstract spine (Definitions 6.3–6.7) is built on the all-maps DomainObj category (its Hom is the full ApproximableMap). We bridge the two faithfully without introducing a second, strict-map category abstraction: the functor here is still T : Endofunctor DomainObj (acting on all maps), but the continuity condition is stated over the strict function spaces (D →⊥ E), and strictness-preservation is then derived (ContinuousOnMaps.isStrict_map) rather than assumed. So T lives on the all-maps category, yet "continuous on maps" pins down exactly the behaviour Scott asks for on the strict subcategory — keeping Definition 6.8 coherent with the rest of the Lecture VI spine while remaining literally about Scott's strict maps.

The identity functor is continuous on maps (continuousOnMaps_id), witnessing non-vacuity; its representing Φ is the identity on the function space. Everything here is choice-free (#print axioms ⊆ {propext, Quot.sound}).

def Domain.Neighborhood.idEndofunctor (Obj : Type u) [Category Obj] : Endofunctor Obj

The identity endofunctor on any category: it fixes objects and morphisms. (A convenient witness that Endofunctor is inhabited; used to show Definition 6.8 is non-vacuous.)

Equations

• Domain.Neighborhood.idEndofunctor Obj = { obj := fun (X : Obj) => X, map := fun {X Y : Obj} (f : Domain.Neighborhood.Category.Hom X Y) => f, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem Domain.Neighborhood.idEndofunctor_obj {Obj : Type u} [Category Obj] (X : Obj) : (idEndofunctor Obj).obj X = X

@[simp]

theorem Domain.Neighborhood.idEndofunctor_map {Obj : Type u} [Category Obj] {X Y : Obj} (f : Category.Hom X Y) : (idEndofunctor Obj).map f = f

def Domain.Neighborhood.ContinuousOnMaps (T : Endofunctor DomainObj) : Prop

Definition 6.8 (Scott 1981, PRG-19). An endofunctor T on the category of domains is continuous on maps when, for every pair of domains D and E, the induced action λf. T(f) on the strict function space (D →⊥ E) is approximable: there is an approximable map Φ from (D →⊥ E) to (T(D) →⊥ T(E)) whose elementwise action (read through the representation strictFunEquiv) sends each strict map f to T(f).

Equations

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

theorem Domain.Neighborhood.ContinuousOnMaps.isStrict_map {T : Endofunctor DomainObj} (h : ContinuousOnMaps T) {D E : DomainObj} (f : Exercise510.StrictMap D.sys E.sys) : Exercise510.IsStrict (T.map ↑f)

A functor continuous on maps preserves strictness (so it genuinely lives on Scott's category of domains and strict maps): if f is strict then so is T(f). This is automatic from the witnessing equation, whose left-hand side is the underlying map of a StrictMap.

theorem Domain.Neighborhood.toStrictMap_toStrictFilter {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (f : Exercise510.StrictMap V₀ V₁) : Exercise510.toStrictMap (Exercise510.toStrictFilter f) = f

toStrictMap ∘ toStrictFilter = id (the right inverse of the strict-function-space representation, Exercise 5.10).

theorem Domain.Neighborhood.continuousOnMaps_id : ContinuousOnMaps (idEndofunctor DomainObj)

The identity functor is continuous on maps — the basic witness that Definition 6.8 is satisfiable. The representing approximable map is the identity on (D →⊥ E).