Theorem 2.12: injective spaces are exactly the continuous lattices

Scott's Theorem 2.12 states that a T₀-space is injective iff it is a continuous lattice under its Scott topology. The forward direction (continuous lattice ⟹ injective) is theorem_2_12_forward (= Proposition 2.11) in Constructions.lean.

This file supplies the backward direction. The argument (Scott 1972, §2) is:

• an injective space is a retract of a power of the Sierpiński space 𝕆 = Prop (Corollary 1.6);
• a power of 𝕆 is a continuous lattice whose Scott topology is its product topology (sierpinskiPower_isContinuousLattice, scottTopology_sierpinskiPower);
• a retract of a continuous lattice is a continuous lattice (Proposition 2.10).

The retraction r : 𝕆^I → D with section s : D → 𝕆^I makes e := s ∘ r a Scott-continuous idempotent on 𝕆^I, whose fixed-point set is a continuous lattice (Proposition 2.10) and is homeomorphic to D. Hence every injective space is homeomorphic to a continuous lattice under its Scott topology.

The order-theoretic core is the construction IdemFix: the fixed points of a Scott-continuous idempotent on a complete lattice form a complete lattice (IdemFix.completeLattice).

@[reducible, inline]

abbrev Domain.ContinuousLattice.IdemFix {L : Type u_1} (e : L → L) : Type u_1

The fixed-point set {x | e x = x} of an endomap e, as a subtype.

Equations

• Domain.ContinuousLattice.IdemFix e = { x : L // e x = x }

@[reducible]

noncomputable def Domain.ContinuousLattice.IdemFix.supSet {L : Type u_1} [CompleteLattice L] {e : L → L} (hidem : ∀ (x : L), e (e x) = e x) : SupSet (IdemFix e)

The supremum in the fixed-point set: apply e to the ambient supremum (which lands back in the fixed-point set because e is idempotent).

Equations

• Domain.ContinuousLattice.IdemFix.supSet hidem = { sSup := fun (S : Set (Domain.ContinuousLattice.IdemFix e)) => ⟨e (sSup (Subtype.val '' S)), ⋯⟩ }

theorem Domain.ContinuousLattice.IdemFix.isLUB_sSup {L : Type u_1} [CompleteLattice L] {e : L → L} (hidem : ∀ (x : L), e (e x) = e x) (hmono : Monotone e) (S : Set (IdemFix e)) : IsLUB S (sSup S)

With the ambient-then-e supremum, every set has a least upper bound in IdemFix e. This needs only that e is monotone (which follows from Scott continuity).

@[reducible]

noncomputable def Domain.ContinuousLattice.IdemFix.completeLattice {L : Type u_1} [CompleteLattice L] {e : L → L} (hidem : ∀ (x : L), e (e x) = e x) (hmono : Monotone e) : CompleteLattice (IdemFix e)

Fixed points of a monotone idempotent form a complete lattice. The supremum is the ambient supremum corrected by e; the rest follows from completeLatticeOfSup.

Equations

• Domain.ContinuousLattice.IdemFix.completeLattice hidem hmono = completeLatticeOfSup (Domain.ContinuousLattice.IdemFix e) ⋯

theorem Domain.ContinuousLattice.IdemFix.coe_sSup {L : Type u_1} [CompleteLattice L] {e : L → L} (hidem : ∀ (x : L), e (e x) = e x) (hmono : Monotone e) (S : Set (IdemFix e)) : ↑(sSup S) = e (sSup (Subtype.val '' S))

The ambient supremum corrected by e is the supremum in IdemFix e.

The fixed-point set of a Scott-continuous idempotent is a continuous

lattice

theorem Domain.ContinuousLattice.idemFix_incl_preservesDirectedSup {L : Type u_1} [CompleteLattice L] {e : L → L} (hidem : ∀ (x : L), e (e x) = e x) (hsc : PreservesDirectedSup e) : PreservesDirectedSup Subtype.val

theorem Domain.ContinuousLattice.idemFix_retr_preservesDirectedSup {L : Type u_1} [CompleteLattice L] {e : L → L} (hidem : ∀ (x : L), e (e x) = e x) (hsc : PreservesDirectedSup e) : PreservesDirectedSup fun (x : L) => ⟨e x, ⋯⟩

noncomputable def Domain.ContinuousLattice.idemFixRetraction {L : Type u_1} [CompleteLattice L] {e : L → L} (hidem : ∀ (x : L), e (e x) = e x) (hsc : PreservesDirectedSup e) : IsContinuousLatticeRetraction (IdemFix e) L

The fixed-point set of a Scott-continuous idempotent e on L, with the ambient-supremum-corrected complete-lattice structure, is a retract of L: the inclusion and the corestriction of e are Scott-continuous and compose to the identity.

Equations

• Domain.ContinuousLattice.idemFixRetraction hidem hsc = { incl := ⟨Subtype.val, ⋯⟩, retr := ⟨fun (x : L) => ⟨e x, ⋯⟩, ⋯⟩, retr_incl := ⋯ }

theorem Domain.ContinuousLattice.idemFix_isContinuousLattice {L : Type u_1} [CompleteLattice L] {e : L → L} (hidem : ∀ (x : L), e (e x) = e x) (hsc : PreservesDirectedSup e) (hL : IsContinuousLattice L) : IsContinuousLattice (IdemFix e)

Fixed points of a Scott-continuous idempotent form a continuous lattice. Combine the retraction idemFixRetraction with Proposition 2.10(a).

theorem Domain.ContinuousLattice.idemFix_scottTopology {L : Type u_1} [CompleteLattice L] {e : L → L} (hidem : ∀ (x : L), e (e x) = e x) (hsc : PreservesDirectedSup e) (hL : IsContinuousLattice L) : scottTopologicalSpace = TopologicalSpace.induced Subtype.val scottTopologicalSpace

Scott topology of the fixed-point lattice = subspace topology. Proposition 2.10(b) applied to idemFixRetraction: the Scott topology of IdemFix e is the topology induced by the inclusion from the Scott topology of L.

Theorem 2.12, backward direction

theorem Domain.ContinuousLattice.theorem_2_12_backward {D : Type u} [TopologicalSpace D] [T0Space D] (hD : IsInjectiveSpace D) : ∃ (E : Type u) (inst : CompleteLattice E), IsContinuousLattice E ∧ Nonempty (D ≃ₜ E)

Scott 1972, Theorem 2.12 (backward direction). Every injective T₀-space is homeomorphic to a continuous lattice equipped with its Scott topology.

The injective space D is a retract of a power 𝕆^I = (I → Prop) of the Sierpiński space (Corollary 1.6). Writing s : D → 𝕆^I for the embedding and r : 𝕆^I → D for the retraction, e := s ∘ r is a Scott-continuous idempotent on 𝕆^I (its topology is its Scott topology by scottTopology_sierpinskiPower). The fixed-point set IdemFix e is therefore a continuous lattice (idemFix_isContinuousLattice, via Proposition 2.10), and d ↦ s d is a homeomorphism D ≃ₜ IdemFix e with inverse the retraction.

theorem Domain.ContinuousLattice.theorem_2_12 {D : Type u} [TopologicalSpace D] [T0Space D] : IsInjectiveSpace D ↔ ∃ (E : Type u) (inst : CompleteLattice E), IsContinuousLattice E ∧ Nonempty (D ≃ₜ E)

Scott 1972, Theorem 2.12. A T₀-space is injective iff it is (homeomorphic to) a continuous lattice under its Scott topology. The forward direction is Proposition 2.11; the backward direction is theorem_2_12_backward.

Lemma 3.9: compatibility of maximal extensions with a projection on the

range

theorem Domain.ContinuousLattice.lemma_3_9 {X : Type u_1} {Y : Type u_2} {D : Type u_3} {D' : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [CompleteLattice D] [CompleteLattice D'] (hD : IsContinuousLattice D) (hD' : IsContinuousLattice D') (P : IsContinuousLatticeProjection D D') (e : X → Y) (he : Topology.IsEmbedding e) {f : X → D} {g : X → D'} (hf : Continuous f) (hg : Continuous g) (hfg : ∀ (x : X), f x = ↑P.retr (g x)) (y : Y) : scottExtend e f y = ↑P.retr (scottExtend e g y)

Scott 1972, Lemma 3.9. With e : X → Y a subspace embedding and i, j : D ⇄ D' a projection on the range, if continuous f : X → D and g : X → D' satisfy f = j ∘ g, then the maximal extensions (Proposition 3.8) satisfy fbar = j ∘ gbar.

The proof is Scott's, recast through the faithful scottExtend:

• j ∘ gbar ⊑ fbar: j ∘ gbar is a continuous solution of (j ∘ gbar) ∘ e = j ∘ g = f, so maximality of fbar (scottExtend_maximal) gives the bound;
• i ∘ fbar ⊑ gbar: (i ∘ fbar) ∘ e = i ∘ f = i ∘ j ∘ g ⊑ g (since i ∘ j ⊑ id), so the sub-solution maximality of gbar (scottExtend_maximal_le, the remark after 3.8) gives the bound;
• combining: fbar = j ∘ i ∘ fbar ⊑ j ∘ gbar ⊑ fbar (using j ∘ i = id and monotonicity of j).