Inverse limits of continuous lattices (Scott 1972, §4) #
We formalize Scott's Proposition 4.1: the inverse limit D_∞ of an ω-system
of continuous
lattices ⟨Dₙ, jₙ⟩ with each jₙ : D_{n+1} → Dₙ a projection is again a
continuous lattice.
Scott proves this through injectivity (D_∞ is an injective T₀-space, hence —
Theorem 2.12 — a
continuous lattice), using the maximal-extension Proposition 3.8 and the
compatibility Lemma 3.9.
The retraction of ∏ Dₙ onto D_∞ that Scott's argument constructs (extend the
identity of
D_∞ along its inclusion) is realized here order-theoretically and without
topology:
- each projection
jₙ = (P n).retris the upper adjoint of its embeddingiₙ = (P n).incl(projection_galoisConnection), hence preserves arbitrary infima; - therefore the compatibility predicate is closed under pointwise
sInf, makingD_∞a complete lattice (completeLatticeOfInf); - the inclusion
D_∞ ↪ ∏ Dₙpreserves infima, so it has a left adjointr : ∏ Dₙ → D_∞(invLimRetr); a left adjoint preserves all suprema, in particular directed ones, soris Scott-continuous, andr ∘ incl = id.
Thus D_∞ is a (Scott-continuous) retract of the continuous lattice ∏ Dₙ (Prop
2.9a), so by
Prop 2.10a it is a continuous lattice. This is exactly the retraction Scott builds
via injectivity,
obtained here as the adjoint of the inclusion.
The embedding–projection pair of a projection is a Galois connection iₙ ⊣ jₙ: from
jₙ ∘ iₙ = id and iₙ ∘ jₙ ⊑ id we get iₙ x ⊑ y ↔ x ⊑ jₙ y. In particular jₙ
(the upper
adjoint) preserves arbitrary infima.
Compatibility of a sequence: jₙ(x_{n+1}) = xₙ for all n.
Instances For
Scott 1972, §4. The inverse limit D_∞ as the subspace of compatible
sequences.
Equations
- Domain.ContinuousLattice.InverseLimit D P = { x : (n : ℕ) → D n // Domain.ContinuousLattice.Compatible D P x }
Instances For
jₙ preserves arbitrary infima (it is the upper adjoint of iₙ).
The pointwise infimum of compatible sequences is compatible.
Equations
- Domain.ContinuousLattice.instInfSetInverseLimit D P = { sInf := fun (S : Set (Domain.ContinuousLattice.InverseLimit D P)) => ⟨sInf (Subtype.val '' S), ⋯⟩ }
For a directed, nonempty family, the inverse-limit supremum is computed
pointwise (each jₙ
is Scott-continuous, so the pointwise sup of compatible sequences is compatible
and is the least
upper bound in D_∞).
The inclusion D_∞ ↪ ∏ Dₙ preserves directed suprema.
Scott's retraction r : ∏ Dₙ → D_∞, realized as the left adjoint of the
inclusion:
r y = ⊓ { x ∈ D_∞ : y ⊑ x }, the least compatible sequence above y.
Equations
- Domain.ContinuousLattice.invLimRetr D P y = sInf {x : Domain.ContinuousLattice.InverseLimit D P | y ≤ ↑x}
Instances For
r ⊣ incl: the retraction is left adjoint to the inclusion.
The retraction preserves directed suprema (a left adjoint preserves all suprema).
r ∘ incl = id: the retraction fixes D_∞.
D_∞ is a Scott-continuous retract of the product ∏ Dₙ.
Equations
- Domain.ContinuousLattice.inverseLimitRetraction D P = { incl := ⟨Subtype.val, ⋯⟩, retr := ⟨Domain.ContinuousLattice.invLimRetr D P, ⋯⟩, retr_incl := ⋯ }
Instances For
Scott 1972, Proposition 4.1. The inverse limit D_∞ of an ω-system of
continuous lattices
with projection bonding maps is itself a continuous lattice. The product ∏ Dₙ is
a continuous
lattice (Prop 2.9a) and D_∞ is a retract of it (inverseLimitRetraction), so
Prop 2.10a applies.
Proposition 4.2: the maps j_{∞n} are projections #
We construct Scott's embeddings i_{n∞} : Dₙ → D_∞ and show that ⟨i_{n∞}, j_{∞n}⟩ is a
projection, where j_{∞n}(x) = xₙ. The component i_{n∞}(x)_m climbs the tower
of embeddings
iₖ = (P k).incl for m ≥ n (embLE) and descends the tower of projections jₖ = (P k).retr
for m < n (projLE).
Climb the tower of embeddings: for n ≤ m, embLE h = i_{m-1} ∘ … ∘ iₙ : Dₙ → D_m.
Equations
- Domain.ContinuousLattice.embLE D P h x = Nat.leRecOn h (fun {k : ℕ} (y : D k) => ↑(P k).incl y) x
Instances For
Descend the tower of projections: for m ≤ n, projLE h = j_m ∘ … ∘ j_{n-1} : D_n → Dₘ.
Equations
- Domain.ContinuousLattice.projLE D P h x = Nat.leRecOn h (fun {k : ℕ} (g : D k → D m) (w : D (k + 1)) => g (↑(P k).retr w)) id x
Instances For
Peeling the last projection: (P m).retr ∘ projLE (m+1 ≤ n) = projLE (m ≤ n).
Scott's embedding component i_{n∞}(x)_m: climb for m ≥ n, descend for m < n.
Equations
- Domain.ContinuousLattice.iComp D P n x m = if h : n ≤ m then Domain.ContinuousLattice.embLE D P h x else Domain.ContinuousLattice.projLE D P ⋯ x
Instances For
The sequence i_{n∞}(x) is compatible, hence a genuine point of D_∞.
For a compatible sequence y, descending from level n to m ≤ n recovers
yₘ.
For a compatible sequence y, climbing yₙ up to level m ≥ n stays below
yₘ.
i_{n∞}(yₙ) ⊑ y coordinatewise (the heart of incl_retr_le for j_{∞n}).
The tower of embeddings is Scott-continuous (a composite of the iₖ).
The tower of projections is Scott-continuous (a composite of the jₖ).
The embedding i_{n∞} : Dₙ → D_∞ as a bare function into the inverse limit.
Equations
- Domain.ContinuousLattice.embInfFun D P n x = ⟨Domain.ContinuousLattice.iComp D P n x, ⋯⟩
Instances For
The projection j_{∞n} : D_∞ → Dₙ as a bare function.
Equations
- Domain.ContinuousLattice.projInfFun D P n y = ↑y n
Instances For
The embedding i_{n∞} : Dₙ → D_∞, Scott-continuous.
Equations
- Domain.ContinuousLattice.embInf D P n = ⟨Domain.ContinuousLattice.embInfFun D P n, ⋯⟩
Instances For
The projection j_{∞n} : D_∞ → Dₙ, Scott-continuous.
Equations
Instances For
Scott 1972, Proposition 4.2. Each j_{∞n} : D_∞ → Dₙ is a projection of
continuous
lattices, with embedding i_{n∞} = embInf n.
Equations
- Domain.ContinuousLattice.proposition_4_2 D P n = { incl := Domain.ContinuousLattice.embInf D P n, retr := Domain.ContinuousLattice.projInf D P n, retr_incl := ⋯, incl_retr_le := ⋯ }
Instances For
Scott 1972, §4 (recursion equation). i_{n∞} = i_{(n+1)∞} ∘ iₙ.
The family n ↦ i_{n∞}(xₙ) is monotone (the lub defining x is monotone).
Scott 1972, §4. Each x ∈ D_∞ is the (monotone) lub of its projections:
x = ⨆ₙ i_{n∞}(xₙ).
Scott 1972, §4 (functional equation, "the remark following 4.2"). The
identity of D_∞ is
the directed lub of the approximating projections rₙ = i_{n∞} ∘ j_{∞n}:
id = ⨆ₙ i_{n∞} ∘ j_{∞n}. This is the algebraic identity at the heart of Theorem
4.4.
Scott 1972, Lemma 4.5. A criterion for recognizing projections out of the
limit: if a
sequence u : ∀ n, D_{n+1} satisfies the (shifted) recursion j_{n+1}(u_{n+2}) = u_{n+1}, then the
monotone limit u_∞ = ⨆ₙ i_{(n+1)∞}(uₙ) has j_{∞(n+1)}(u_∞) = uₙ.
Proof: extend u to a compatible sequence w (w₀ = j₀(u₀), w_{k+1} = u_k);
then w is a
point of D_∞, and since the family k ↦ i_{k∞}(w_k) is monotone, dropping its
0-th term does
not change the lub (Monotone.iSup_nat_add), so u_∞ = ⨆ₖ i_{k∞}(w_k) = w by
inverseLimit_eq_iSup.
Hence j_{∞(n+1)}(u_∞) = w_{n+1} = uₙ.
Corollary 4.3: D_∞ is also the direct limit #
Given continuous fₙ : Dₙ → D' into any complete lattice with fₙ = f_{n+1} ∘ iₙ, the map
f∞(x) = ⨆ₙ fₙ(xₙ) is the unique continuous mediating map with fₙ = f∞ ∘ i_{n∞}.
The mediating map of Corollary 4.3: f∞(x) = ⨆ₙ fₙ(xₙ).
Equations
- Domain.ContinuousLattice.coconeInf D P f x = ⨆ (n : ℕ), ↑(f n) (↑x n)
Instances For
Climbing then applying f is constant: f_m(i_{m-1}…iₙ x) = fₙ(x).
Descending then applying f only decreases: f_m(j_m…j_{n-1} x) ⊑ fₙ(x).
Scott 1972, Corollary 4.3 (factorization). fₙ = f∞ ∘ i_{n∞}.
f∞ is Scott-continuous: f∞(⊔S) = ⊔ f∞(S) for directed S (each fₙ is
continuous and a
double ⨆ over ℕ × S commutes).
Scott 1972, Corollary 4.3. Within complete lattices, D_∞ is also the
direct limit of
the Dₙ along the embeddings iₙ: for every compatible cocone fₙ : Dₙ → D'
(continuous, with
fₙ = f_{n+1} ∘ iₙ) there is a unique continuous f∞ : D_∞ → D' with fₙ = f∞ ∘ i_{n∞},
namely f∞(x) = ⨆ₙ fₙ(xₙ).