Continuous lattice constructions (Scott 1972, §2.8–2.12) #
The Milner correction (March 1972, pp. 135–136) is in MilnerCorrection.lean.
Full proofs of
2.8–2.12 under CoarserThanScottTopology are the remaining 1972 items; the
Sierpiński
injectivity base case (1.2) is already complete.
This file additionally proves Scott's first two example/closure results, the order-theoretic content of Propositions 2.8 (finite lattices are continuous) and 2.9 (products of continuous lattices are continuous). The accompanying topological claims of 2.9–2.10 ("the induced topology agrees with the product / subspace topology") are the parts that require the Milner correction and remain open.
A non-empty finite directed set attains its supremum: ⊔S ∈ S. A maximal
element of
S (which exists by finiteness) is, by directedness, the greatest element, hence
the
supremum. This is the order-theoretic heart of "finite ⟹ continuous" (Scott 1972,
2.8).
Scott 1972, Proposition 2.8. A finite lattice is a continuous lattice. In
a finite
lattice every principal up-set Set.Ici y is Scott-open (a non-empty directed set
is finite,
so it attains its supremum), hence y ≪ y; therefore y is the supremum of {x | x ≪ y}.
Scott 1972, Proposition 2.9(a) (order-theoretic content). The Cartesian
product of any
family of continuous lattices is a continuous lattice. (Part (b), that the induced
topology of
the product agrees with the product topology, is proposition_2_9_b below;
proposition_2_9
bundles the two.)
The key step is that if a ≪ yᵢ in the factor Dᵢ, then the cylinder element
[a]ⁱ
(equal to a in coordinate i and ⊥ elsewhere) is way below y in the
product: the
preimage {z | zᵢ ∈ U} of a Scott-open witness U ⊆ Dᵢ is Scott-open in the
product
(suprema are computed coordinatewise). Any upper bound b of {x | x ≪ y}
therefore
dominates every [a]ⁱ, so a = ([a]ⁱ)ᵢ ≤ bᵢ; ranging over a ≪ yᵢ and using
continuity of
Dᵢ gives yᵢ ≤ bᵢ for all i, i.e. y ≤ b.
Proposition 2.9(b): the induced topology of a product is the product #
topology
Scott 1972, Proposition 2.9 also asserts that the Scott topology of the product
∏ᵢ Dᵢ of
continuous lattices coincides with the topological product of the Scott topologies
of the factors.
We prove the two inclusions:
- Product ⊆ Scott (
scottTopologicalSpace ≤ Pi.topologicalSpace): every projectioneval ipreserves directed suprema (they are computed coordinatewise), hence is Scott-continuous, hence the Scott topology of the product is finer than each induced topology, i.e. finer than their infimum (the product topology). - Scott ⊆ Product (
Pi.topologicalSpace ≤ scottTopologicalSpace): given a Scott-openUand a pointz ∈ U, the↟abasis (exists_wayBelow_Ici_subset) yieldsa ≪ zwith↑a ⊆ U. A way-below element of a product has finite support (wayBelow_finite_support) and is way-below in each coordinate (wayBelow_proj); the resulting finite box⋂_{i ∈ F} eval i ⁻¹' (↟aᵢ-neighbourhood of zᵢ)is a product-open neighbourhood ofzinside↑a ⊆ U.
Plugging a value into a fixed coordinate, v ↦ Function.update z i v,
preserves directed
suprema: away from i the result is the constant z j, and at i it is the
identity.
A way-below relation in a product projects to each coordinate: if a ≪ z in
∏ᵢ Eᵢ then
aᵢ ≪ zᵢ. The witnessing Scott-open neighbourhood of zᵢ is the preimage of a
product Scott-open
witness under v ↦ Function.update z i v, which is Scott-open by
update_preservesDirectedSup.
A way-below element of a product has finite support: if a ≪ z in ∏ᵢ Eᵢ
then aⱼ = ⊥ for
all but finitely many j. The finite truncations Z F = (fun j => if j ∈ F then z j else ⊥) form a
directed family with supremum z; since a ≪ z = ⊔_F Z F, already a ≤ Z F for
some finite F,
forcing aⱼ = ⊥ off F.
Scott 1972, Proposition 2.9(b). For a family of continuous lattices, the Scott topology of the product coincides with the product of the Scott topologies of the factors.
Scott 1972, Proposition 2.9 (full statement). The product of a family of
continuous lattices
is again a continuous lattice (proposition_2_9_a) whose Scott topology agrees
with the product
topology (proposition_2_9_b).
Proposition 2.11: continuous lattices are injective #
The substance of Scott's Theorem 2.12. We give the explicit extension operator
g(y) = ⊔_{V ∋ y open} ⊓ f''(e⁻¹V) and prove (a) it extends f along an
embedding e
(using continuity of D to interpolate from below) and (b) it is Scott-continuous
(using the
↟a basis of the Scott topology).
Scott's canonical extension of f : X → E along e : X → Y (Scott 1972,
proof of 2.11):
y ↦ ⊔ { ⊓ f''(e⁻¹V) : V an open neighbourhood of y }. No topology on E is
needed to state
the operator — it is purely order-theoretic.
Equations
Instances For
The defining family of scottExtend is directed: open neighbourhoods are
closed under
intersection, and ⊓ f''(e⁻¹ ·) is monotone in the neighbourhood (smaller set,
larger inf).
The extension agrees with f on the (embedded) subspace. The ≤ direction is
immediate
(f x₀ is one of the values being met); the ≥ direction uses continuity of E:
for each
a ≪ f x₀ the Scott-open ↟a pulls back along the continuous f and, by the
embedding, to an
open V ⊆ Y on whose e-preimage f ≥ a, so a ≤ ⊓ f''(e⁻¹V) ≤ g(e x₀).
The extension is Scott-continuous. For a Scott-open U and a point y₀ with
g y₀ ∈ U, the
basis lemma gives a ≪ g y₀ with ↟a ⊆ U; since g y₀ is a directed supremum,
a ≪ ⊓ f''(e⁻¹V)
for some open V ∋ y₀, and that value is ≤ g y' for every y' ∈ V, so V ⊆ g⁻¹U.
For a continuous f' : Y → E into a continuous lattice E (with its Scott
topology), the
value f' y is reconstructed as the supremum over open neighbourhoods U ∋ y of
the meets
⊓ f''(U). This is the order-theoretic content behind the maximality clause of
Proposition 3.8:
the ≤ direction interpolates from below using f' y = ⊔ {a | a ≪ f' y} and the
openness of each
f'⁻¹(↟a); the ≥ direction is immediate since f' y ∈ f''(U) whenever y ∈ U.
Maximality clause of Scott 1972, Proposition 3.8. Any continuous solution
f' of
f' ∘ e = f lies below scottExtend e f. Following Scott: expand f' via
continuous_eq_sSup_openInfs, restrict each meet from U to the embedded
subspace e(X) ∩ U
(only enlarging the meet), and recognize the result as a defining term of
scottExtend.
Scott 1972, remark following 3.8. scottExtend e g is also the maximal
sub-solution: any
continuous f' with f' ∘ e ⊑ g satisfies f' ⊑ scottExtend e g. Same proof as
scottExtend_maximal, replacing the final equality f' (e x) = f x by the
inequality
f' (e x) ≤ g x.
Scott 1972, Proposition 3.8. If E is a continuous lattice and e : X → Y a subspace
embedding, then for each continuous f : X → E the explicit formula scottExtend e f is the
maximal extension of f to [Y → E]: it is Scott-continuous
(scottExtend_continuous), it
restricts to f along e (scottExtend_eq_of_continuous), and it dominates
every continuous
solution of f' ∘ e = f (scottExtend_maximal).
Scott 1972, Proposition 2.11. Every continuous lattice is an injective
space under its
induced (Scott) topology. The witness is scottExtend, which extends any
continuous f along
any embedding e (scottExtend_eq_of_continuous) and is itself continuous
(scottExtend_continuous).
The Sierpiński space Prop (Scott's 𝕆) is a continuous lattice: it is a
finite complete
lattice, so Proposition 2.8 applies.
The Scott topology on Scott's two-point space 𝕆 = Prop is exactly the
Sierpiński topology
(generateFrom {{True}}). The Scott-open sets of Prop are the upper sets ∅,
{True}, univ,
which are precisely the Sierpiński-open sets. This is the topological
identification underlying
Theorem 2.12: the building block 𝕆 carries its Scott topology.
A power of Scott's two-point space 𝕆 = Prop is a continuous lattice: Prop
is a continuous
lattice (isContinuousLattice_prop) and products of continuous lattices are
continuous
(Proposition 2.9(a)). This is the order-theoretic content of "a Cartesian power of
𝕆 is a
continuous lattice", the construction Theorem 2.12 retracts onto.
The Scott topology on a power ι → 𝕆 of the Sierpiński space coincides with
the product
(= Sierpiński power) topology. Combine Proposition 2.9(b) (the Scott topology of a
product is the
product of the factors' Scott topologies) with scottTopology_prop (each factor's
Scott topology
is the Sierpiński topology).
Scott 1972, Theorem 2.12 (forward direction). Every continuous lattice is an injective space under its Scott topology. This is the substantial half of the equivalence "injective spaces = continuous lattices", and is exactly Proposition 2.11.
Scott 1972, Theorem 2.12 (backward, Sierpiński base case). Prop is a
continuous
lattice (isContinuousLattice_prop), so its injectivity (Proposition 1.2) is an
instance of the
equivalence.
Scott 1972, Theorem 2.12 (injectivity half, unconditional). Prop is
injective
(Sierpiński); the continuous-lattice half is now isContinuousLattice_prop.
The Sierpiński space 𝕆 = Prop realizes the smallest case of Theorem 2.12: it
is both
injective (1.2) and a continuous lattice (2.8).