The function-space tower and Scott's D_∞ ≅ [D_∞ → D_∞] (Scott 1972, §4, #
Theorem 4.4)
Starting from a continuous lattice D₀ together with a chosen projection j₀ : [D₀ → D₀] → D₀
(Proposition 3.13 provides one), we build the recursively-defined ω-system
D_{n+1} = [D_n → D_n], j_{n+1} = [j_n → j_n] (the function-space
functor, Proposition 3.7),
and form its inverse limit D_∞. Theorem 4.4 is that D_∞ is homeomorphic to
its own function
space [D_∞ → D_∞].
A complete lattice bundled with its instance, used to define the
function-space tower by
recursion on ℕ (the type at level n+1 depends on the lattice structure at
level n).
- carrier : Type u
The underlying carrier type of the bundled complete lattice.
- str : CompleteLattice self.carrier
Instances For
The tower D₀, [D₀→D₀], [[D₀→D₀]→[D₀→D₀]], … as bundled complete lattices.
Equations
- One or more equations did not get rendered due to their size.
- Domain.ContinuousLattice.towerCLat D₀ 0 = D₀
Instances For
The carrier Dₙ of the function-space tower.
Equations
Instances For
Equations
Apply an element of D_{n+1} as a function Dₙ → Dₙ (definitional via
towerType_succ).
Equations
- Domain.ContinuousLattice.towerCoeFun = { coe := fun (f : Domain.ContinuousLattice.towerType D₀ (n + 1)) => ↑(Domain.ContinuousLattice.towerToMap f) }
The map view of a tower element is definitionally the original element.
The function-space functor on projections (Proposition 3.7, continuous #
form)
proposition37Projection builds the embedding/projection pair on function
spaces as plain
functions; here we upgrade them to genuine Scott maps, so that [Dₙ → Dₙ] is a
continuous-lattice
projection of [D_{n+1} → D_{n+1}]. The map f ↦ post ∘ f ∘ pre (conjugation) is
Scott-continuous
because directed suprema of function spaces are computed pointwise.
Conjugation f ↦ post ∘ f ∘ pre as a bare function [Y → Y] → [W → Z].
Equations
- Domain.ContinuousLattice.conjMapFun post pre f = post.comp (f.comp pre)
Instances For
Conjugation f ↦ post ∘ f ∘ pre as a Scott map [Y → Y] → [W → Z].
Equations
- Domain.ContinuousLattice.conjMap post pre = ⟨Domain.ContinuousLattice.conjMapFun post pre, ⋯⟩
Instances For
Scott 1972, Proposition 3.7 (continuous projection on the diagonal). If
D is a
continuous-lattice projection of D', then [D → D] is a projection of [D' → D'] via
i_{[·]}(f) = i ∘ f ∘ j and j_{[·]}(g) = j ∘ g ∘ i.
Equations
- P.functionSpace = { incl := Domain.ContinuousLattice.conjMap P.incl P.retr, retr := Domain.ContinuousLattice.conjMap P.retr P.incl, retr_incl := ⋯, incl_retr_le := ⋯ }
Instances For
The projection tower j_{n+1} = [j_n → j_n], anchored at a chosen base
projection
j₀ : [D₀ → D₀] → D₀.
Equations
- Domain.ContinuousLattice.towerProj D₀ j₀ 0 = j₀
- Domain.ContinuousLattice.towerProj D₀ j₀ n.succ = (Domain.ContinuousLattice.towerProj D₀ j₀ n).functionSpace
Instances For
Scott 1972, §4 (recursion for the embeddings). i_{n+1}(x) = iₙ ∘ x ∘ jₙ.
Scott 1972, §4 (recursion for the projections). j_{n+1}(x') = jₙ ∘ x' ∘ iₙ.
Scott 1972, §4 (application is preserved). iₙ(f(x)) = i_{n+1}(f)(iₙ(x))
for f ∈ D_{n+1},
x ∈ Dₙ. The embeddings turn functional application into application one level
up.
Theorem 4.4(a): the limit maps i_∞ and j_∞ #
We now wire the concrete inverse limit D_∞ of the function-space tower and write
down Scott's pair
i_∞(x) = ⨆ₙ (i_{n∞} ∘ x_{n+1} ∘ j_{∞n}) : D_∞ → [D_∞ → D_∞]
j_∞(f) = ⨆ₙ i_{(n+1)∞}(j_{∞n} ∘ f ∘ i_{n∞}) : [D_∞ → D_∞] → D_∞
Each summand is itself a Scott map (a composite of conjMap, embInf,
projInf), so each of
i_∞, j_∞ is a supremum of Scott maps and is therefore Scott-continuous
automatically: by
Theorem 3.3 the function space [A → B] is a complete lattice in which suprema
are computed
pointwise. No bespoke continuity argument is needed.
The inverse limit D_∞ of the function-space tower ⟨Dₙ, jₙ⟩.
Equations
Instances For
The function space [D_∞ → D_∞].
Equations
Instances For
The n-th summand of i_∞: the Scott map x ↦ i_{n∞} ∘ x_{n+1} ∘ j_{∞n},
where x_{n+1} is
the (n+1)-st component of x ∈ D_∞. As a map D_∞ → [D_∞ → D_∞] it is the
composite of the
component projection j_{∞(n+1)} with conjugation by (i_{n∞}, j_{∞n}).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Scott 1972, §4 (Theorem 4.4). The embedding i_∞ : D_∞ → [D_∞ → D_∞],
i_∞(x) = ⨆ₙ i_{n∞} ∘ x_{n+1} ∘ j_{∞n}. It is Scott-continuous because it is a
supremum of the
Scott maps iInfTerm n (suprema in [D_∞ → [D_∞ → D_∞]] are computed pointwise).
Equations
- Domain.ContinuousLattice.embInfInf D₀ j₀ = ⨆ (n : ℕ), Domain.ContinuousLattice.iInfTerm D₀ j₀ n
Instances For
The n-th summand of j_∞: the Scott map f ↦ i_{(n+1)∞}(j_{∞n} ∘ f ∘ i_{n∞}). As a map
[D_∞ → D_∞] → D_∞ it is conjugation by (j_{∞n}, i_{n∞}) (landing in D_{n+1})
followed by the
embedding i_{(n+1)∞}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Scott 1972, §4 (Theorem 4.4). The projection j_∞ : [D_∞ → D_∞] → D_∞,
j_∞(f) = ⨆ₙ i_{(n+1)∞}(j_{∞n} ∘ f ∘ i_{n∞}). Scott-continuous as a supremum of
the Scott maps
jInfTerm n.
Equations
- Domain.ContinuousLattice.projInfInf D₀ j₀ = ⨆ (n : ℕ), Domain.ContinuousLattice.jInfTerm D₀ j₀ n
Instances For
j_∞ evaluated at f is the supremum of the summands jInfTerm n f.
i_∞ is Scott-continuous (it is a bundled ScottMap).
j_∞ is Scott-continuous (it is a bundled ScottMap).
Theorem 4.4(b): j_∞ ∘ i_∞ = id on D_∞ #
Scott's calculation (~lines 1290–1294): expand j_∞(i_∞(x)) as a double sup,
collapse the monotone
double limit to the diagonal using projInf ∘ embInf = id on each summand, then
recognize x via
inverseLimit_eq_iSup (with a one-step index shift).
Conjugation commutes with a supremum indexed by ℕ (the range is directed
when f is
monotone).
Since conjMap post pre is itself a Scott map, this is just preservation of
directed suprema.
Diagonal simplification. conjMap (j_{∞n}, i_{n∞}) applied to the n-th
summand of i_∞
recovers the component x_{n+1}. This is exactly j_{[·]} ∘ i_{[·]} = id for the
function-space
projection built from proposition_4_2.
i_{n∞}(yₙ) ⊑ y_{n+1}: climbing one level and embedding stays below the next
component.
Conjugation climbs the tower (one step). Lifting conjMap (j_{∞n}, i_{n∞}) f along
i_{n+1}
stays below conjMap (j_{∞(n+1)}, i_{(n+1)∞}) f. Both sides live in D_{n+2};
the inequality is the
algebraic content that makes the double sup defining j_∞ ∘ i_∞ monotone in the
level index n.
j_∞(i_∞(x)) = ⨆ₙ i_{(n+1)∞}(x_{n+1}).
Scott 1972, §4 (Theorem 4.4, first half). j_∞ ∘ i_∞ = id on D_∞.
Theorem 4.4(c): i_∞ ∘ j_∞ = id on [D_∞ → D_∞] #
This is the converse half (Scott ~lines 1322–1335). The restrictions
u_n = j_{∞n} ∘ f ∘ i_{n∞} ∈ D_{n+1} satisfy the Lemma-4.5 recursion
j_{n+1}(u_{n+2}) = u_{n+1}
(towerProj_retr_conjMap_succ), so Lemma 4.5 identifies the components of
j_∞(f). Expanding
i_∞(j_∞(f)) then yields the approximation ⨆ₙ rₙ ∘ f ∘ rₙ with rₙ = i_{n∞} ∘ j_{∞n}, and the
functional equation id = ⨆ₙ rₙ (via inverseLimit_eq_iSup) plus continuity of
f collapse this
to f.
Step 1 (Lemma-4.5 recursion). j_{n+1}(j_{∞(n+1)} ∘ f ∘ i_{(n+1)∞}) = j_{∞n} ∘ f ∘ i_{n∞}.
This is the equality counterpart of conjMap_incl_le_conjMap_succ; it is the
hypothesis Lemma 4.5
needs to recognize j_∞(f) from its restrictions.
Scott 1972, §4 (Theorem 4.4, second half). i_∞ ∘ j_∞ = id on [D_∞ → D_∞].
Theorem 4.4(d): capstone D_∞ ≅ [D_∞ → D_∞] #
Package the mutually-inverse Scott maps from (b) and (c). Scott's homeomorphism
follows because
i_∞ and j_∞ are Scott-continuous (embInfInf / projInfInf are bundled
ScottMaps).
Scott 1972, §4 (Theorem 4.4). The inverse limit D_∞ of the
function-space tower is
order-isomorphic to its own function space [D_∞ → D_∞] via the mutually-inverse
Scott maps
i_∞ = embInfInf and j_∞ = projInfInf.
The order isomorphism D_∞ ≃o [D_∞ → D_∞] witnessing Theorem 4.4. Both
directions are
Scott-continuous (they are bundled ScottMaps), so this is the order-theoretic
half of Scott's
homeomorphism.
Equations
- One or more equations did not get rendered due to their size.