Function spaces on continuous lattices (Scott 1972, §3)

Scott's §3 studies spaces of continuous maps [X → Y] with the topology of pointwise convergence (subbasic sets {f | f x ∈ U}), the pointwise specialization order (3.2), and the fact that [D → D'] is a continuous lattice when D → D'] is (3.3).

March 1972 correction (Milner)

Scott's remark before Proposition 2.5 was mistaken: a T₀-topology on a complete lattice need not have every open set Scott-open. The two extreme T₀-topologies inducing the same order are generated by {x | not x <= y} (lower) and {x | y ⊑ x} (principal up-sets). The corrected proofs of 2.9, 2.10, and 3.3 assume the given topology is coarser than the Scott (lattice) topology (scottTopologicalSpace ≤ τ in mathlib). We revisit that hypothesis when formalizing those results.

In the March 1972 correction (p. 135), Scott writes ⊔S′ (prime on the index, not on the join): for S ⊆ D a subspace of ambient D′, ⊔S′ is the supremum of S computed in D′, while ⊔S is the supremum in the subspace D; the retraction identity is j(⊔S′) = ⊔S.

Definition 3.1

def Domain.ContinuousLattice.scottFunctionEvalSubbasis (X : Type u_10) (Y : Type u_11) [TopologicalSpace X] [TopologicalSpace Y] : Set (Set C(X, Y))

Subbasic sets for Scott's function-space topology (pointwise convergence).

Equations

• Domain.ContinuousLattice.scottFunctionEvalSubbasis X Y = {W : Set C(X, Y) | ∃ (x : X) (U : Set Y), IsOpen U ∧ W = {f : C(X, Y) | f x ∈ U}}

@[reducible]

noncomputable def Domain.ContinuousLattice.scottFunctionTopology (X : Type u_10) (Y : Type u_11) [TopologicalSpace X] [TopologicalSpace Y] : TopologicalSpace C(X, Y)

Scott 1972, Definition 3.1. The function space [X → Y] carries the topology generated by {f : f x ∈ U | x ∈ X, U open in Y}.

Equations

• Domain.ContinuousLattice.scottFunctionTopology X Y = TopologicalSpace.generateFrom (Domain.ContinuousLattice.scottFunctionEvalSubbasis X Y)

@[reducible, inline]

abbrev Domain.ContinuousLattice.ScottFunctionSpace (X : Type u_10) (Y : Type u_11) [TopologicalSpace X] [TopologicalSpace Y] : Type (max u_10 u_11)

Scott's notation [X → Y]: continuous maps with the pointwise (product) topology.

Equations

• Domain.ContinuousLattice.ScottFunctionSpace X Y = C(X, Y)

Proposition 3.2

theorem Domain.ContinuousLattice.scottFunctionSubbasis_isOpen {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {U : Set Y} (hU : IsOpen U) : IsOpen {f : C(X, Y) | f x ∈ U}

theorem Domain.ContinuousLattice.specializationLe_generateOpen {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f g : C(X, Y)) (hfg : ∀ (x : X), SpecializationLe (f x) (g x)) {V : Set C(X, Y)} (hV : TopologicalSpace.GenerateOpen (scottFunctionEvalSubbasis X Y) V) (hf : f ∈ V) : g ∈ V

theorem Domain.ContinuousLattice.scottFunctionSpecializationLe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} : SpecializationLe f g ↔ ∀ (x : X), SpecializationLe (f x) (g x)

theorem Domain.ContinuousLattice.proposition_3_2 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} : SpecializationLe f g ↔ ∀ (x : X), SpecializationLe (f x) (g x)

Scott 1972, Proposition 3.2. The specialization order on [X → Y] is pointwise.

§3 on continuous lattices: pointwise lattice structure

@[reducible, inline]

abbrev Domain.ContinuousLattice.ScottC (D : Type u_10) (D' : Type u_11) [CompleteLattice D] [CompleteLattice D'] : Type (max u_10 u_11)

Continuous maps D → D' with Scott topologies on domain and codomain.

Equations

• Domain.ContinuousLattice.ScottC D D' = C(D, D')

def Domain.ContinuousLattice.ScottMap (D : Type u_10) (D' : Type u_11) [CompleteLattice D] [CompleteLattice D'] : Type (max u_10 u_11)

Continuous maps between complete lattices with Scott's induced topologies.

Equations

• Domain.ContinuousLattice.ScottMap D D' = { f : D → D' // Continuous f }

@[implicit_reducible]

instance Domain.ContinuousLattice.ScottMap.instCoeFunForall {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] : CoeFun (ScottMap D D') fun (x : ScottMap D D') => D → D'

Equations

• Domain.ContinuousLattice.ScottMap.instCoeFunForall = { coe := fun (f : Domain.ContinuousLattice.ScottMap D D') => ↑f }

theorem Domain.ContinuousLattice.ScottMap.ext {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] {f g : ScottMap D D'} (h : ∀ (x : D), ↑f x = ↑g x) : f = g

theorem Domain.ContinuousLattice.ScottMap.ext_iff {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] {f g : ScottMap D D'} : f = g ↔ ∀ (x : D), ↑f x = ↑g x

theorem Domain.ContinuousLattice.ScottMap.continuous {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (f : ScottMap D D') : Continuous ↑f

theorem Domain.ContinuousLattice.ScottMap.preservesDirectedSup_coe {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (f : ScottMap D D') (S : Set D) (hS : S.Nonempty) (hSdir : DirectedOn (fun (x1 x2 : D) => x1 ≤ x2) S) : ↑f (sSup S) = sSup (↑f '' S)

theorem Domain.ContinuousLattice.ScottMap.monotone {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (f : ScottMap D D') : Monotone ↑f

theorem Domain.ContinuousLattice.ScottMap.preservesDirectedSup_comp {D : Type u_3} {D' : Type u_4} {D'' : Type u_5} [CompleteLattice D] [CompleteLattice D'] [CompleteLattice D''] {f : D' → D''} {g : D → D'} (hf : PreservesDirectedSup f) (hg : PreservesDirectedSup g) : PreservesDirectedSup (f ∘ g)

def Domain.ContinuousLattice.ScottMap.comp {D : Type u_3} {D' : Type u_4} {D'' : Type u_5} [CompleteLattice D] [CompleteLattice D'] [CompleteLattice D''] (f : ScottMap D' D'') (g : ScottMap D D') : ScottMap D D''

Composition of Scott-continuous maps.

Equations

• f.comp g = ⟨↑f ∘ ↑g, ⋯⟩

def Domain.ContinuousLattice.ScottMap.const {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (c : D') : ScottMap D D'

The constant Scott map with value c.

Equations

• Domain.ContinuousLattice.ScottMap.const c = ⟨fun (x : D) => c, ⋯⟩

theorem Domain.ContinuousLattice.ScottMap.pointwise_sup_preservesDirectedSup {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (f g : ScottMap D D') : PreservesDirectedSup fun (x : D) => ↑f x ⊔ ↑g x

noncomputable def Domain.ContinuousLattice.ScottMap.bot {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] : ScottMap D D'

The bottom Scott map, pointwise constantly ⊥.

Equations

• Domain.ContinuousLattice.ScottMap.bot = Domain.ContinuousLattice.ScottMap.const ⊥

def Domain.ContinuousLattice.ScottMap.le {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (f g : ScottMap D D') : Prop

The pointwise order on Scott maps.

Equations

• f.le g = ∀ (x : D), ↑f x ≤ ↑g x

noncomputable def Domain.ContinuousLattice.ScottMap.sup {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (f g : ScottMap D D') : ScottMap D D'

The pointwise supremum of two Scott maps.

Equations

• f.sup g = ⟨fun (x : D) => ↑f x ⊔ ↑g x, ⋯⟩

theorem Domain.ContinuousLattice.ScottMap.pointwise_sSup_preservesDirectedSup {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (F : Set (ScottMap D D')) : PreservesDirectedSup fun (x : D) => sSup ((fun (f : ScottMap D D') => ↑f x) '' F)

noncomputable def Domain.ContinuousLattice.ScottMap.sSupMaps {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (F : Set (ScottMap D D')) : ScottMap D D'

The pointwise supremum of a set of Scott maps.

Equations

• Domain.ContinuousLattice.ScottMap.sSupMaps F = ⟨fun (x : D) => sSup ((fun (f : Domain.ContinuousLattice.ScottMap D D') => ↑f x) '' F), ⋯⟩

theorem Domain.ContinuousLattice.ScottMap.sSupMaps_apply {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (F : Set (ScottMap D D')) (x : D) : ↑(sSupMaps F) x = sSup ((fun (f : ScottMap D D') => ↑f x) '' F)

The complete lattice [D → D'] (Theorem 3.3, order content)

The pointwise order makes ScottMap D D' a partial order; sSupMaps gives suprema (pointwise, since directed and arbitrary suprema of Scott maps are computed pointwise — Theorem 3.3). By completeLatticeOfSup this is a complete lattice. Note infima are not pointwise (Scott's warning); completeLatticeOfSup derives them as sSup of lower bounds.

@[implicit_reducible]

instance Domain.ContinuousLattice.ScottMap.instPartialOrder {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] : PartialOrder (ScottMap D D')

Equations

• Domain.ContinuousLattice.ScottMap.instPartialOrder = { le := Domain.ContinuousLattice.ScottMap.le, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

theorem Domain.ContinuousLattice.ScottMap.le_def {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] {f g : ScottMap D D'} : f ≤ g ↔ ∀ (x : D), ↑f x ≤ ↑g x

@[implicit_reducible]

noncomputable instance Domain.ContinuousLattice.ScottMap.instSupSet {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] : SupSet (ScottMap D D')

Equations

• Domain.ContinuousLattice.ScottMap.instSupSet = { sSup := Domain.ContinuousLattice.ScottMap.sSupMaps }

theorem Domain.ContinuousLattice.ScottMap.sSup_apply {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (F : Set (ScottMap D D')) (x : D) : ↑(sSup F) x = sSup ((fun (f : ScottMap D D') => ↑f x) '' F)

theorem Domain.ContinuousLattice.ScottMap.isLUB_sSup {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (F : Set (ScottMap D D')) : IsLUB F (sSup F)

@[implicit_reducible]

noncomputable instance Domain.ContinuousLattice.ScottMap.instCompleteLattice {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] : CompleteLattice (ScottMap D D')

Equations

• Domain.ContinuousLattice.ScottMap.instCompleteLattice = completeLatticeOfSup (Domain.ContinuousLattice.ScottMap D D') ⋯

def Domain.ContinuousLattice.ScottMap.idMap {D : Type u_3} [CompleteLattice D] : ScottMap D D

The identity Scott map.

Equations

• Domain.ContinuousLattice.ScottMap.idMap = ⟨fun (x : D) => x, ⋯⟩

@[simp]

theorem Domain.ContinuousLattice.ScottMap.idMap_apply {D : Type u_3} [CompleteLattice D] (x : D) : ↑idMap x = x

@[simp]

theorem Domain.ContinuousLattice.ScottMap.comp_apply {D : Type u_3} {D' : Type u_4} {D'' : Type u_5} [CompleteLattice D] [CompleteLattice D'] [CompleteLattice D''] (f : ScottMap D' D'') (g : ScottMap D D') (x : D) : ↑(f.comp g) x = ↑f (↑g x)

theorem Domain.ContinuousLattice.ScottMap.sup_apply {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (f g : ScottMap D D') (x : D) : ↑(f ⊔ g) x = ↑f x ⊔ ↑g x

The (completeLatticeOfSup-derived) binary join of Scott maps is computed pointwise.

theorem Domain.ContinuousLattice.ScottMap.bot_apply {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (x : D) : ↑⊥ x = ⊥

The bottom Scott map is the constant ⊥.

@[simp]

theorem Domain.ContinuousLattice.ScottMap.const_apply {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (c : D') (x : D) : ↑(const c) x = c

Theorem 3.3 (core)

noncomputable def Domain.ContinuousLattice.theorem33sSup {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (F : Set (ScottMap D D')) : ScottMap D D'

Scott 1972, Theorem 3.3 (directed sup). Pointwise suprema of Scott-continuous maps are Scott-continuous; this is the heart of Scott's proof that [D → D'] is a complete lattice.

Equations

• Domain.ContinuousLattice.theorem33sSup F = Domain.ContinuousLattice.ScottMap.sSupMaps F

noncomputable def Domain.ContinuousLattice.theorem33Sup {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (f g : ScottMap D D') : ScottMap D D'

Scott 1972, Theorem 3.3 (binary join). Pointwise join of Scott-continuous maps is Scott-continuous.

Equations

• Domain.ContinuousLattice.theorem33Sup f g = f.sup g

Theorem 3.3 ([D → D'] is a continuous lattice)

Scott's step functions ē[e, e'] are the building blocks: ē[e,e'](x) = e' if e ≪ x, else ⊥. We encode the conditional value as ⨆ _ : e ≪ x, e' (which is e' when e ≪ x and ⊥ otherwise), avoiding any decidability assumption. Each step function is Scott-continuous (the way-above set {x | e ≪ x} is Scott-open), is way below f whenever e' ≪ f e, and f is the supremum of the step functions below it — whence [D → D'] is a continuous lattice.

noncomputable def Domain.ContinuousLattice.stepFun {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (e : D) (e' : D') (x : D) : D'

The (value of the) step function ē[e, e'] at x: e' if e ≪ x, else ⊥.

Equations

• Domain.ContinuousLattice.stepFun e e' x = ⨆ (_ : Domain.ContinuousLattice.WayBelow e x), e'

theorem Domain.ContinuousLattice.stepFun_of_wayBelow {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] {e : D} {e' : D'} {x : D} (h : WayBelow e x) : stepFun e e' x = e'

theorem Domain.ContinuousLattice.stepFun_of_not_wayBelow {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] {e : D} {e' : D'} {x : D} (h : ¬WayBelow e x) : stepFun e e' x = ⊥

theorem Domain.ContinuousLattice.stepFun_preservesDirectedSup {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (e : D) (e' : D') : PreservesDirectedSup (stepFun e e')

Step functions are Scott-continuous: {x | e ≪ x} is Scott-open, so the conditional commutes with directed suprema.

noncomputable def Domain.ContinuousLattice.stepMap {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (e : D) (e' : D') : ScottMap D D'

The step function ē[e, e'] as a Scott map.

Equations

• Domain.ContinuousLattice.stepMap e e' = ⟨Domain.ContinuousLattice.stepFun e e', ⋯⟩

theorem Domain.ContinuousLattice.stepMap_apply_of_wayBelow {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] {e : D} {e' : D'} {x : D} (h : WayBelow e x) : ↑(stepMap e e') x = e'

theorem Domain.ContinuousLattice.stepMap_le_of_wayBelow {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] {e : D} {e' : D'} {g : ScottMap D D'} (h : WayBelow e' (↑g e)) : stepMap e e' ≤ g

If e' ≪ g e then the step function ē[e, e'] lies below g (a pointwise argument).

theorem Domain.ContinuousLattice.stepMap_wayBelow {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] {e : D} {e' : D'} {f : ScottMap D D'} (he' : WayBelow e' (↑f e)) : WayBelow (stepMap e e') f

The step function is way below f. If e' ≪ f e, then ē[e, e'] ≪ f in [D → D'], witnessed by the Scott-open set {g | e' ≪ g e} (open because suprema in [D → D'] are pointwise and {· ≪ ·} is inaccessible by directed suprema).

theorem Domain.ContinuousLattice.stepMap_pointwise_sSup {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (hD : IsContinuousLattice D) (hD' : IsContinuousLattice D') (f : ScottMap D D') (x : D) : sSup {e' : D' | ∃ (e : D), WayBelow e x ∧ WayBelow e' (↑f e)} = ↑f x

Pointwise reconstruction. For a Scott map f, the supremum of the values of the step functions below f recovers f x: f x = ⊔ {e' | ∃ e ≪ x, e' ≪ f e}. Uses continuity of D (x = ⊔{e | e ≪ x}), Scott-continuity of f, and continuity of D'.

theorem Domain.ContinuousLattice.theorem_3_3_isContinuousLattice {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (hD : IsContinuousLattice D) (hD' : IsContinuousLattice D') : IsContinuousLattice (ScottMap D D')

Scott 1972, Theorem 3.3 (order content). If D and D' are continuous lattices, then so is [D → D'] under the pointwise order. Every f is the supremum of the step functions way below it: f = ⊔ {ē[e,e'] | e' ≪ f e}, and each such step function is way below f.

Theorem 3.3(b): the lattice topology = the topology of pointwise

convergence

The Scott topology of the continuous lattice [D → D'] coincides with the product (pointwise convergence) topology, whose subbasis is {f | f x ∈ U} (U Scott-open in D'). One inclusion (pointwise ⊆ Scott) is immediate: each subbasic set is Scott-open in the lattice (joins are pointwise). The other (Scott ⊆ pointwise) is Scott's argument via the ↟φ basis of a continuous lattice: φ ≪ g forces φ ≤ ⊔ᵢ ē[eᵢ,eᵢ'] for finitely many pairs with eᵢ' ≪ g eᵢ, and the finite intersection ⋂ᵢ {h | eᵢ' ≪ h eᵢ} is a pointwise-open neighbourhood of g inside ↟φ.

theorem Domain.ContinuousLattice.wayBelow_finset_sup {ι : Type u_10} {L : Type u_11} [CompleteLattice L] {s : Finset ι} {f : ι → L} {g : L} (h : ∀ i ∈ s, WayBelow (f i) g) : WayBelow (s.sup f) g

A finite sup of elements way below g is way below g.

def Domain.ContinuousLattice.scottMapPointwiseSubbasis (D : Type u_10) (D' : Type u_11) [CompleteLattice D] [CompleteLattice D'] : Set (Set (ScottMap D D'))

Subbasic sets of the pointwise (product) topology on [D → D']: {f | f x ∈ U} for U Scott-open in D'.

Equations

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

@[reducible]

noncomputable def Domain.ContinuousLattice.scottMapPointwiseTopology (D : Type u_10) (D' : Type u_11) [CompleteLattice D] [CompleteLattice D'] : TopologicalSpace (ScottMap D D')

Scott 1972, Definition 3.1 (on lattices). The topology of pointwise convergence on [D → D'].

Equations

• Domain.ContinuousLattice.scottMapPointwiseTopology D D' = TopologicalSpace.generateFrom (Domain.ContinuousLattice.scottMapPointwiseSubbasis D D')

theorem Domain.ContinuousLattice.pointwiseSubbasic_isOpen {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (x : D) {U : Set D'} (hU : IsOpen U) : IsOpen {f : ScottMap D D' | ↑f x ∈ U}

theorem Domain.ContinuousLattice.pointwiseSubbasic_scottOpen {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (x : D) {U : Set D'} (hU : ScottOpen U) : ScottOpen {f : ScottMap D D' | ↑f x ∈ U}

Each pointwise-subbasic set {f | f x ∈ U} (U Scott-open) is Scott-open in the lattice [D → D'], because suprema there are pointwise. This is the easy inclusion pointwise ⊆ Scott.

theorem Domain.ContinuousLattice.wayBelow_le_finset_sup_step {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (hD : IsContinuousLattice D) (hD' : IsContinuousLattice D') {φ g : ScottMap D D'} (h : WayBelow φ g) : ∃ (F : Finset (D × D')), (∀ p ∈ F, WayBelow p.2 (↑g p.1)) ∧ φ ≤ F.sup fun (p : D × D') => stepMap p.1 p.2

Step-function decomposition of ≪. If φ ≪ g in [D → D'], then φ lies below a finite join of step functions ē[eᵢ,eᵢ'] with eᵢ' ≪ g eᵢ. The finite joins of such step functions form a directed family with supremum g, so wayBelow_sSup_iff produces one above φ.

theorem Domain.ContinuousLattice.theorem_3_3_topology {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (hD : IsContinuousLattice D) (hD' : IsContinuousLattice D') : scottTopologicalSpace = scottMapPointwiseTopology D D'

Scott 1972, Theorem 3.3(b). The Scott (lattice) topology on [D → D'] agrees with the topology of pointwise convergence.

theorem Domain.ContinuousLattice.theorem_3_3 {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (hD : IsContinuousLattice D) (hD' : IsContinuousLattice D') : IsContinuousLattice (ScottMap D D') ∧ scottTopologicalSpace = scottMapPointwiseTopology D D'

Scott 1972, Theorem 3.3 (full statement). For continuous lattices D, D', the function space [D → D'] is a continuous lattice (theorem_3_3_isContinuousLattice) whose Scott topology agrees with the topology of pointwise convergence (theorem_3_3_topology).

Corollary 3.4

theorem Domain.ContinuousLattice.scottFunctionSubbasis_isOpen_scott {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] {x : D} {U : Set D'} (hU : IsOpen U) : IsOpen {f : ScottC D D' | f x ∈ U}

theorem Domain.ContinuousLattice.corollary_3_4_eval_on_C {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (x : D) : Continuous fun (f : ScottC D D') => f x

theorem Domain.ContinuousLattice.corollary_3_4 {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (x : D) : Continuous fun (f : ScottC D D') => f x

Scott 1972, Corollary 3.4 (fixed x). Evaluation at fixed x is continuous on [D → D'] (with Scott topologies on D and D'); this is one half of the separate-continuity input to joint continuity.

theorem Domain.ContinuousLattice.corollary_3_4_preservesDirectedSup {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] : PreservesDirectedSup fun (p : ScottMap D D' × D) => ↑p.1 p.2

Scott 1972, Corollary 3.4 (joint continuity, core). Evaluation [D → D'] × D → D', (f, x) ↦ f x, preserves directed suprema. By Proposition 2.6 it suffices to check separate Scott-continuity: in x (with f fixed) it is f's own continuity, and in f (with x fixed) it is the pointwise formula for suprema in [D → D'] (ScottMap.sSup_apply).

theorem Domain.ContinuousLattice.corollary_3_4_jointly_continuous {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] : Continuous fun (p : ScottMap D D' × D) => ↑p.1 p.2

Scott 1972, Corollary 3.4. The evaluation map eval : [D → D'] × D → D', (f, x) ↦ f x, is (jointly) Scott-continuous. Via Theorem 3.3(b) and Proposition 2.9(b) the Scott topology of the product lattice is the product of the pointwise topology on [D → D'] and the Scott topology on D, so this is exactly joint continuity for Scott's product topology.

Proposition 3.5 (currying)

theorem Domain.ContinuousLattice.sSup_image_prod_mk_left {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (x : D) (S : Set D') (hS : S.Nonempty) : sSup ((fun (y : D') => (x, y)) '' S) = (x, sSup S)

theorem Domain.ContinuousLattice.curry_right_preservesDirectedSup {D : Type u_3} {D' : Type u_4} {D'' : Type u_5} [CompleteLattice D] [CompleteLattice D'] [CompleteLattice D''] (f : ScottMap (D × D') D'') (x : D) : PreservesDirectedSup fun (y : D') => ↑f (x, y)

noncomputable def Domain.ContinuousLattice.scottLambdaAt {D : Type u_3} {D' : Type u_4} {D'' : Type u_5} [CompleteLattice D] [CompleteLattice D'] [CompleteLattice D''] (f : ScottMap (D × D') D'') (x : D) : ScottMap D' D''

Scott 1972, Proposition 3.5 (right). Currying in the y-variable is Scott-continuous.

Equations

• Domain.ContinuousLattice.scottLambdaAt f x = ⟨fun (y : D') => ↑f (x, y), ⋯⟩

theorem Domain.ContinuousLattice.sSup_image_prod_mk_right {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (y : D') (S : Set D) (hS : S.Nonempty) : sSup ((fun (x : D) => (x, y)) '' S) = (sSup S, y)

theorem Domain.ContinuousLattice.curry_left_preservesDirectedSup {D : Type u_3} {D' : Type u_4} {D'' : Type u_5} [CompleteLattice D] [CompleteLattice D'] [CompleteLattice D''] (f : ScottMap (D × D') D'') (y : D') : PreservesDirectedSup fun (x : D) => ↑f (x, y)

Currying in the x-variable: x ↦ f (x, y) is Scott-continuous (used for continuity of lambda f as a map D → [D' → D'']).

theorem Domain.ContinuousLattice.lambda_outer_preservesDirectedSup {D : Type u_3} {D' : Type u_4} {D'' : Type u_5} [CompleteLattice D] [CompleteLattice D'] [CompleteLattice D''] (f : ScottMap (D × D') D'') : PreservesDirectedSup fun (x : D) => scottLambdaAt f x

The outer half of currying: x ↦ (y ↦ f (x, y)) preserves directed suprema (so lambda f is a Scott map D → [D' → D'']). Equality in [D' → D''] is pointwise, reducing to curry_left.

noncomputable def Domain.ContinuousLattice.scottLambda {D : Type u_3} {D' : Type u_4} {D'' : Type u_5} [CompleteLattice D] [CompleteLattice D'] [CompleteLattice D''] (f : ScottMap (D × D') D'') : ScottMap D (ScottMap D' D'')

Scott 1972, Proposition 3.5. Functional abstraction lambda : [[D × D'] → D''] → [D → [D' → D'']], lambda f x y = f (x, y). By Theorem 3.3, [D → [D' → D'']] is itself a continuous lattice, and lambda f is a Scott map.

Equations

• Domain.ContinuousLattice.scottLambda f = ⟨fun (x : D) => Domain.ContinuousLattice.scottLambdaAt f x, ⋯⟩

@[simp]

theorem Domain.ContinuousLattice.scottLambda_apply {D : Type u_3} {D' : Type u_4} {D'' : Type u_5} [CompleteLattice D] [CompleteLattice D'] [CompleteLattice D''] (f : ScottMap (D × D') D'') (x : D) (y : D') : ↑(↑(scottLambda f) x) y = ↑f (x, y)

theorem Domain.ContinuousLattice.proposition_3_5_preservesDirectedSup {D : Type u_3} {D' : Type u_4} {D'' : Type u_5} [CompleteLattice D] [CompleteLattice D'] [CompleteLattice D''] : PreservesDirectedSup scottLambda

lambda preserves directed suprema: both sides evaluate, pointwise at (x, y), to ⊔ {f (x, y) | f ∈ 𝓕}, since suprema in every function lattice involved are pointwise.

theorem Domain.ContinuousLattice.proposition_3_5 {D : Type u_3} {D' : Type u_4} {D'' : Type u_5} [CompleteLattice D] [CompleteLattice D'] [CompleteLattice D''] : Continuous scottLambda

Scott 1972, Proposition 3.5. Functional abstraction lambda is Scott-continuous.

Definition 3.6

structure Domain.ContinuousLattice.IsContinuousLatticeRetraction (D : Type u_10) (D' : Type u_11) [CompleteLattice D] [CompleteLattice D'] : Type (max u_10 u_11)

Scott 1972, Definition 3.6. A retraction of continuous lattices.

• incl : ScottMap D D'

  The inclusion map into the ambient lattice.

• retr : ScottMap D' D

  The retraction map back to the sublattice.

• retr_incl (d : D) : ↑self.retr (↑self.incl d) = d

structure Domain.ContinuousLattice.IsContinuousLatticeProjection (D : Type u_10) (D' : Type u_11) [CompleteLattice D] [CompleteLattice D'] extends Domain.ContinuousLattice.IsContinuousLatticeRetraction D D' : Type (max u_10 u_11)

Scott 1972, Definition 3.6. A projection of continuous lattices: a retract with i ∘ j ⊑ id.

• incl : ScottMap D D'
• retr : ScottMap D' D
• retr_incl (d : D) : ↑self.retr (↑self.incl d) = d
• incl_retr_le (d : D') : ↑self.incl (↑self.retr d) ≤ d

noncomputable def Domain.ContinuousLattice.IsContinuousLatticeRetraction.ambientSSup {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (R : IsContinuousLatticeRetraction D D') (S : Set D) : D'

Scott 1972, Prop 2.10 / March 1972 correction (p. 135). For S ⊆ D a subspace of ambient D', write ⊔S′ for the supremum of S computed in D' (Scott's prime is on the index, not the join). This is sSup (i '' S) in Lean.

Equations

• R.ambientSSup S = sSup (↑R.incl '' S)

theorem Domain.ContinuousLattice.IsContinuousLatticeRetraction.retr_ambientSSup_eq_sSup {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (R : IsContinuousLatticeRetraction D D') (S : Set D) (hS : S.Nonempty) (hdir : DirectedOn (fun (x1 x2 : D) => x1 ≤ x2) S) : ↑R.retr (R.ambientSSup S) = sSup S

Scott 1972, Prop 2.10 / March 1972 correction (p. 135). For directed S ⊆ D, j(⊔S′) = ⊔S: the retraction sends the ambient join back to the subspace join.

theorem Domain.ContinuousLattice.IsContinuousLatticeRetraction.incl_preservesDirectedSup {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (R : IsContinuousLatticeRetraction D D') : PreservesDirectedSup ↑R.incl

The inclusion of a retraction preserves directed suprema (it is a Scott map).

theorem Domain.ContinuousLattice.IsContinuousLatticeRetraction.retr_wayBelow_of_wayBelow_incl {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (R : IsContinuousLatticeRetraction D D') {d : D} {x' : D'} (hx' : WayBelow x' (↑R.incl d)) : WayBelow (↑R.retr x') d

Heart of Scott's proof of 2.10. If x' ≪ i(d) in the ambient continuous lattice D', then its image j(x') is way below d in the retract D. The Scott-open witness in D is the preimage i⁻¹V' of an ambient Scott-open witness V' (Scott-open because i preserves directed suprema); for z ∈ i⁻¹V' we have x' ⊑ i(z), hence j(x') ⊑ j(i(z)) = z. No projection hypothesis is needed — j ∘ i = id and monotonicity suffice.

theorem Domain.ContinuousLattice.IsContinuousLatticeRetraction.sSup_image_retr_wayBelow {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (R : IsContinuousLatticeRetraction D D') (hD' : IsContinuousLattice D') (d : D) : sSup (↑R.retr '' {x' : D' | WayBelow x' (↑R.incl d)}) = d

For d in the retract, the ambient way-below set of i(d) pushed back by j is a directed family whose supremum (computed in D) is d. This is the identity j(⊔S′) = ⊔S applied to S = {j(x') : x' ≪ i(d)}, combined with continuity of D'.

theorem Domain.ContinuousLattice.IsContinuousLatticeRetraction.image_retr_wayBelow_nonempty {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (R : IsContinuousLatticeRetraction D D') (d : D) : (↑R.retr '' {x' : D' | WayBelow x' (↑R.incl d)}).Nonempty

theorem Domain.ContinuousLattice.IsContinuousLatticeRetraction.image_retr_wayBelow_directed {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (R : IsContinuousLatticeRetraction D D') (d : D) : DirectedOn (fun (x1 x2 : D) => x1 ≤ x2) (↑R.retr '' {x' : D' | WayBelow x' (↑R.incl d)})

Proposition 2.10: a retract of a continuous lattice is a continuous

lattice

theorem Domain.ContinuousLattice.proposition_2_10_a {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (R : IsContinuousLatticeRetraction D D') (hD' : IsContinuousLattice D') : IsContinuousLattice D

Scott 1972, Proposition 2.10(a). A (Scott-continuous) retract of a continuous lattice is a continuous lattice. For d ∈ D we have, in the ambient D', i(d) = ⊔{x' | x' ≪ i(d)}; applying the retraction j (which preserves this directed supremum) gives d = ⊔{j(x') | x' ≪ i(d)} in D, and each j(x') ≪ d by retr_wayBelow_of_wayBelow_incl. Hence any upper bound of {x | x ≪ d} dominates d, so d = ⊔{x | x ≪ d}.

theorem Domain.ContinuousLattice.proposition_2_10_b {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (R : IsContinuousLatticeRetraction D D') (hD' : IsContinuousLattice D') : scottTopologicalSpace = TopologicalSpace.induced (↑R.incl) scottTopologicalSpace

Scott 1972, Proposition 2.10(b) (March 1972 / Milner correction). The Scott topology of the retract D coincides with the subspace topology induced from the ambient D' along i.

• scott ≤ induced: each induced-open i⁻¹V' is Scott-open in D because i is a Scott map.
• induced ≤ scott: the sets i⁻¹(↟x') = {z | x' ≪ i(z)} (x' ∈ D') are a basis of D's Scott topology — given a Scott-open U ∋ d, the directed family {j(x') | x' ≪ i(d)} (sup d) meets U at some j(x'), and i⁻¹(↟x') ⊆ U since x' ≪ i(z) ⟹ j(x') ⊑ z with U upper. Each such basic set is induced-open by construction, so every Scott-open of D is induced-open.

theorem Domain.ContinuousLattice.proposition_2_10 {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (R : IsContinuousLatticeRetraction D D') (hD' : IsContinuousLattice D') : IsContinuousLattice D ∧ scottTopologicalSpace = TopologicalSpace.induced (↑R.incl) scottTopologicalSpace

Scott 1972, Proposition 2.10 (full statement). A retract of a continuous lattice is a continuous lattice (proposition_2_10_a) whose Scott topology agrees with the subspace topology (proposition_2_10_b).

Proposition 3.7

structure Domain.ContinuousLattice.ScottMapRetraction (D₀ : Type u_10) (D₀' : Type u_11) (D₁ : Type u_12) (D₁' : Type u_13) [CompleteLattice D₀] [CompleteLattice D₀'] [CompleteLattice D₁] [CompleteLattice D₁'] : Type (max (max (max u_10 u_11) u_12) u_13)

Scott 1972, Proposition 3.7 (retraction half). If D_n is a retract of D'_n (n = 0,1), then [D₀ → D₁] is a retract of [D'₀ → D'₁] via f ↦ i₁ ∘ f ∘ j₀ and f' ↦ j₁ ∘ f' ∘ i₀.

• incl : ScottMap D₀ D₁ → ScottMap D₀' D₁'

  The induced inclusion on function spaces.

• retr : ScottMap D₀' D₁' → ScottMap D₀ D₁

  The induced retraction on function spaces.

• retr_incl (f : ScottMap D₀ D₁) : self.retr (self.incl f) = f

structure Domain.ContinuousLattice.ScottMapProjection (D₀ : Type u_10) (D₀' : Type u_11) (D₁ : Type u_12) (D₁' : Type u_13) [CompleteLattice D₀] [CompleteLattice D₀'] [CompleteLattice D₁] [CompleteLattice D₁'] extends Domain.ContinuousLattice.ScottMapRetraction D₀ D₀' D₁ D₁' : Type (max (max (max u_10 u_11) u_12) u_13)

Scott 1972, Proposition 3.7 (projection half). Under the same hypotheses with projections, the induced pair on function spaces is also a projection.

• incl : ScottMap D₀ D₁ → ScottMap D₀' D₁'
• retr : ScottMap D₀' D₁' → ScottMap D₀ D₁
• retr_incl (f : ScottMap D₀ D₁) : self.retr (self.incl f) = f
• incl_retr_le (f' : ScottMap D₀' D₁') (x : D₀') : ↑(self.incl (self.retr f')) x ≤ ↑f' x

def Domain.ContinuousLattice.ScottMapRetraction.functionSpace {D₀ : Type u_6} {D₀' : Type u_7} {D₁ : Type u_8} {D₁' : Type u_9} [CompleteLattice D₀] [CompleteLattice D₀'] [CompleteLattice D₁] [CompleteLattice D₁'] (R₀ : IsContinuousLatticeRetraction D₀ D₀') (R₁ : IsContinuousLatticeRetraction D₁ D₁') : ScottMapRetraction D₀ D₀' D₁ D₁'

The function-space retraction induced by retractions on the domain and codomain.

Equations

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

def Domain.ContinuousLattice.ScottMapProjection.functionSpace {D₀ : Type u_6} {D₀' : Type u_7} {D₁ : Type u_8} {D₁' : Type u_9} [CompleteLattice D₀] [CompleteLattice D₀'] [CompleteLattice D₁] [CompleteLattice D₁'] (P₀ : IsContinuousLatticeProjection D₀ D₀') (P₁ : IsContinuousLatticeProjection D₁ D₁') : ScottMapProjection D₀ D₀' D₁ D₁'

The function-space projection induced by projections on the domain and codomain.

Equations

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

def Domain.ContinuousLattice.proposition37Retraction {D₀ : Type u_6} {D₀' : Type u_7} {D₁ : Type u_8} {D₁' : Type u_9} [CompleteLattice D₀] [CompleteLattice D₀'] [CompleteLattice D₁] [CompleteLattice D₁'] (R₀ : IsContinuousLatticeRetraction D₀ D₀') (R₁ : IsContinuousLatticeRetraction D₁ D₁') : ScottMapRetraction D₀ D₀' D₁ D₁'

Scott 1972, Proposition 3.7 (retraction). Function spaces inherit retractions.

Equations

• Domain.ContinuousLattice.proposition37Retraction R₀ R₁ = Domain.ContinuousLattice.ScottMapRetraction.functionSpace R₀ R₁

def Domain.ContinuousLattice.proposition37Projection {D₀ : Type u_6} {D₀' : Type u_7} {D₁ : Type u_8} {D₁' : Type u_9} [CompleteLattice D₀] [CompleteLattice D₀'] [CompleteLattice D₁] [CompleteLattice D₁'] (P₀ : IsContinuousLatticeProjection D₀ D₀') (P₁ : IsContinuousLatticeProjection D₁ D₁') : ScottMapProjection D₀ D₀' D₁ D₁'

Scott 1972, Proposition 3.7 (projection). Function spaces inherit projections.

Equations

• Domain.ContinuousLattice.proposition37Projection P₀ P₁ = Domain.ContinuousLattice.ScottMapProjection.functionSpace P₀ P₁

Proposition 3.10

theorem Domain.ContinuousLattice.IsContinuousLatticeProjection.incl_injective {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (P : IsContinuousLatticeProjection D D') {x y : D} (h : ↑P.incl x = ↑P.incl y) : x = y

Scott 1972, Proposition 3.10(ii). The inclusion map of a projection is injective.

theorem Domain.ContinuousLattice.IsContinuousLatticeProjection.retr_bot {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (P : IsContinuousLatticeProjection D D') : ↑P.retr ⊥ = ⊥

theorem Domain.ContinuousLattice.IsContinuousLatticeProjection.incl_bot {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (P : IsContinuousLatticeProjection D D') : ↑P.incl ⊥ = ⊥

Scott 1972, Proposition 3.10(i), empty case. i(⊥) = ⊥.

theorem Domain.ContinuousLattice.IsContinuousLatticeProjection.incl_sup {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (P : IsContinuousLatticeProjection D D') (x y : D) : ↑P.incl (x ⊔ y) = ↑P.incl x ⊔ ↑P.incl y

Scott 1972, Proposition 3.10(i), binary case. i(x ⊔ y) = i(x) ⊔ i(y).

theorem Domain.ContinuousLattice.IsContinuousLatticeProjection.incl_finset_sup {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (P : IsContinuousLatticeProjection D D') (T : Finset D) : ↑P.incl (T.sup fun (x : D) => x) = T.sup fun (x : D) => ↑P.incl x

def Domain.ContinuousLattice.IsContinuousLatticeProjection.finsetSupOf {D : Type u_3} [CompleteLattice D] (S : Set D) : Set D

Finite sub-lubs used in Scott's proof of Proposition 3.10(i).

Equations

• Domain.ContinuousLattice.IsContinuousLatticeProjection.finsetSupOf S = {z : D | ∃ (T : Finset D), (∀ x ∈ T, x ∈ S) ∧ z = T.sup id}

theorem Domain.ContinuousLattice.IsContinuousLatticeProjection.mem_finsetSupOf_of_mem {D : Type u_3} [CompleteLattice D] {S : Set D} {x : D} (hx : x ∈ S) : x ∈ finsetSupOf S

theorem Domain.ContinuousLattice.IsContinuousLatticeProjection.le_sSup_finsetSupOf {D : Type u_3} [CompleteLattice D] (S : Set D) : sSup S ≤ sSup (finsetSupOf S)

theorem Domain.ContinuousLattice.IsContinuousLatticeProjection.sSup_le_finsetSupOf {D : Type u_3} [CompleteLattice D] (S : Set D) : sSup (finsetSupOf S) ≤ sSup S

theorem Domain.ContinuousLattice.IsContinuousLatticeProjection.sSup_finsetSupOf {D : Type u_3} [CompleteLattice D] (S : Set D) : sSup S = sSup (finsetSupOf S)

theorem Domain.ContinuousLattice.IsContinuousLatticeProjection.directedOn_finsetSupOf {D : Type u_3} [CompleteLattice D] (S : Set D) : DirectedOn (fun (x1 x2 : D) => x1 ≤ x2) (finsetSupOf S)

theorem Domain.ContinuousLattice.IsContinuousLatticeProjection.directedOn_wayBelow {D : Type u_3} [CompleteLattice D] (a : D) : DirectedOn (fun (x1 x2 : D) => x1 ≤ x2) {z : D | WayBelow z a}

theorem Domain.ContinuousLattice.IsContinuousLatticeProjection.incl_sSup {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (P : IsContinuousLatticeProjection D D') (S : Set D) : ↑P.incl (sSup S) = sSup (↑P.incl '' S)

Scott 1972, Proposition 3.10(i). Projections preserve arbitrary suprema.

theorem Domain.ContinuousLattice.IsContinuousLatticeProjection.incl_wayBelow {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (P : IsContinuousLatticeProjection D D') (hD' : IsContinuousLattice D') {x y : D} (h : WayBelow x y) : WayBelow (↑P.incl x) (↑P.incl y)

Scott 1972, Proposition 3.10(iii). Projections preserve the way-below relation.

theorem Domain.ContinuousLattice.IsContinuousLatticeProjection.proposition_3_10_forward {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (P : IsContinuousLatticeProjection D D') (hD' : IsContinuousLattice D') : (∀ (S : Set D), ↑P.incl (sSup S) = sSup (↑P.incl '' S)) ∧ Function.Injective ↑P.incl ∧ ∀ (x y : D), WayBelow x y → WayBelow (↑P.incl x) (↑P.incl y)

Scott 1972, Proposition 3.10(i)–(iii), bundled. The inclusion i of a projection preserves arbitrary suprema, is injective, and preserves the way-below relation.

theorem Domain.ContinuousLattice.IsContinuousLatticeProjection.retr_eq_sSup {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (P : IsContinuousLatticeProjection D D') (x' : D') : ↑P.retr x' = sSup {x : D | ↑P.incl x ≤ x'}

Scott 1972, Proposition 3.10(iv), uniqueness. The retraction of any projection is forced to be Scott's formula j(x') = ⊔ { x | i(x) ⊑ x' }. ≤: j(x') itself satisfies i(j x') ⊑ x' (by i ∘ j ⊑ id), so it is a member of the set; ≥: each member x (with i x ⊑ x') satisfies x = j(i x) ⊑ j(x') by j ∘ i = id and monotonicity.

Proposition 3.10, converse direction

Given a map i : D → D' satisfying (i)–(iii), Scott's formula (iv) j(x') = ⊔ { x | i(x) ⊑ x' } is the unique continuous retraction making D a projection of D'.

noncomputable def Domain.ContinuousLattice.converseRetr {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (i : D → D') (x' : D') : D

Scott 1972, Proposition 3.10(iv). Scott's candidate retraction j(x') = ⊔ { x | i(x) ⊑ x' }.

Equations

• Domain.ContinuousLattice.converseRetr i x' = sSup {x : D | i x ≤ x'}

theorem Domain.ContinuousLattice.converseRetr_mono {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] (i : D → D') : Monotone (converseRetr i)

theorem Domain.ContinuousLattice.incl_sup_of_preservesSSup {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] {i : D → D'} (hi : ∀ (S : Set D), i (sSup S) = sSup (i '' S)) (x y : D) : i (x ⊔ y) = i x ⊔ i y

From (i): i preserves binary joins (Scott checks (i) on two-element sets).

theorem Domain.ContinuousLattice.incl_mono_of_preservesSSup {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] {i : D → D'} (hi : ∀ (S : Set D), i (sSup S) = sSup (i '' S)) : Monotone i

From (i): i is monotone.

theorem Domain.ContinuousLattice.le_of_incl_le {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] {i : D → D'} (hi : ∀ (S : Set D), i (sSup S) = sSup (i '' S)) (hinj : Function.Injective i) {x y : D} (h : i x ≤ i y) : x ≤ y

From (i)+(ii): i is order-reflecting (x ⊑ y ↔ i x ⊑ i y), since x ⊑ y ↔ x ⊔ y = y.

theorem Domain.ContinuousLattice.incl_converseRetr_le {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] {i : D → D'} (hi : ∀ (S : Set D), i (sSup S) = sSup (i '' S)) (x' : D') : i (converseRetr i x') ≤ x'

i ∘ j ⊑ id (uses only (i)).

theorem Domain.ContinuousLattice.converseRetr_incl {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] {i : D → D'} (hi : ∀ (S : Set D), i (sSup S) = sSup (i '' S)) (hinj : Function.Injective i) (y : D) : converseRetr i (i y) = y

j ∘ i = id (uses (i)+(ii)): {x | i x ⊑ i y} = Iic y, whose join is y.

theorem Domain.ContinuousLattice.converseRetr_preservesDirectedSup {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] {i : D → D'} (_hi : ∀ (S : Set D), i (sSup S) = sSup (i '' S)) (hwb : ∀ {x y : D}, WayBelow x y → WayBelow (i x) (i y)) (hD : IsContinuousLattice D) : PreservesDirectedSup (converseRetr i)

j is Scott-continuous (uses (i)+(iii) and continuity of D). For directed S': monotonicity gives ⊔ j''S' ⊑ j(⊔S'); conversely if i x ⊑ ⊔S' then for every z ≪ x we have i z ≪ i x ⊑ ⊔S', so i z ⊑ x' for some x' ∈ S' (directedness), whence z ⊑ j(x') ⊑ ⊔ j''S'; continuity of D then gives x ⊑ ⊔ j''S'.

noncomputable def Domain.ContinuousLattice.converseProjection {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] {i : D → D'} (hi : ∀ (S : Set D), i (sSup S) = sSup (i '' S)) (hinj : Function.Injective i) (hwb : ∀ {x y : D}, WayBelow x y → WayBelow (i x) (i y)) (hD : IsContinuousLattice D) : IsContinuousLatticeProjection D D'

The projection assembled from a map i satisfying 3.10(i)–(iii).

Equations

• Domain.ContinuousLattice.converseProjection hi hinj hwb hD = { incl := ⟨i, ⋯⟩, retr := ⟨Domain.ContinuousLattice.converseRetr i, ⋯⟩, retr_incl := ⋯, incl_retr_le := ⋯ }

theorem Domain.ContinuousLattice.proposition_3_10_converse {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] {i : D → D'} (hi : ∀ (S : Set D), i (sSup S) = sSup (i '' S)) (hinj : Function.Injective i) (hwb : ∀ {x y : D}, WayBelow x y → WayBelow (i x) (i y)) (hD : IsContinuousLattice D) : ∃ (P : IsContinuousLatticeProjection D D'), (∀ (d : D), ↑P.incl d = i d) ∧ ∀ (x' : D'), ↑P.retr x' = sSup {x : D | i x ≤ x'}

Scott 1972, Proposition 3.10 (converse). If i : D → D' (between continuous lattices) satisfies (i) preservation of arbitrary suprema, (ii) injectivity, and (iii) preservation of ≪, then there is a continuous j making D a projection of D' via i, with j given by Scott's formula (iv) j(x') = ⊔ { x | i(x) ⊑ x' }.

Proposition 3.8

noncomputable def Domain.ContinuousLattice.scottSubspaceExtendInf {D : Type u_3} [CompleteLattice D] {X : Type u_10} {Y : Type u_11} (e : X → Y) (f : X → D) (U : Set Y) : D

Scott 1972, Proposition 3.8. The infimum term ⊓ { f(x) : e(x) ∈ U } for open U ⊆ Y.

Equations

• Domain.ContinuousLattice.scottSubspaceExtendInf e f U = sInf (f '' e ⁻¹' U)

noncomputable def Domain.ContinuousLattice.scottSubspaceExtend {D : Type u_3} [CompleteLattice D] {X : Type u_10} {Y : Type u_11} [CompleteLattice Y] (e : X → Y) (f : X → D) (y : Y) : D

Scott 1972, Proposition 3.8. Scott's maximal subspace extension fbar : Y → D.

Equations

• Domain.ContinuousLattice.scottSubspaceExtend e f y = sSup {d : D | ∃ (U : Set Y), IsOpen U ∧ y ∈ U ∧ d = Domain.ContinuousLattice.scottSubspaceExtendInf e f U}

theorem Domain.ContinuousLattice.scottSubspaceExtendInf_le_of_mem {D : Type u_3} [CompleteLattice D] {Y : Type u_11} [CompleteLattice Y] {f' : ScottMap Y D} {U : Set Y} {y : Y} (hyU : y ∈ U) : sInf (↑f' '' U) ≤ ↑f' y

theorem Domain.ContinuousLattice.sInf_image_le_sInf_image_of_subset {D : Type u_3} [CompleteLattice D] {α : Type u_12} {f : α → D} {S T : Set α} (hST : S ⊆ T) : sInf (f '' T) ≤ sInf (f '' S)

theorem Domain.ContinuousLattice.scottMap_eq_sSup_openInfs {D : Type u_3} [CompleteLattice D] {Y : Type u_11} [CompleteLattice Y] (hD : IsContinuousLattice D) (f' : ScottMap Y D) (y : Y) : ↑f' y = sSup {d : D | ∃ (U : Set Y), IsOpen U ∧ y ∈ U ∧ d = sInf (↑f' '' U)}

theorem Domain.ContinuousLattice.scottSubspaceExtendInf_eq_of_comp {D : Type u_3} [CompleteLattice D] {X : Type u_10} {Y : Type u_11} [CompleteLattice Y] {e : X → Y} {f : X → D} {U : Set Y} (f' : ScottMap Y D) (h : ∀ (x : X), ↑f' (e x) = f x) : scottSubspaceExtendInf e f U = sInf (↑f' '' (e '' Set.univ ∩ U))

theorem Domain.ContinuousLattice.scottSubspaceExtend_maximal {D : Type u_3} [CompleteLattice D] {X : Type u_10} {Y : Type u_11} [TopologicalSpace X] [TopologicalSpace Y] [CompleteLattice Y] (hD : IsContinuousLattice D) (e : X → Y) (_he : Topology.IsEmbedding e) (f : X → D) (f' : ScottMap Y D) (h_ext : ∀ (x : X), ↑f' (e x) = f x) (y : Y) : ↑f' y ≤ scottSubspaceExtend e f y

Scott 1972, Proposition 3.8 (subspace variant). fbar (with the Scott topology on Y) is the maximal extension along a subspace embedding. The faithful statement (arbitrary topology on Y) is proposition_3_8 in Constructions.lean.

theorem Domain.ContinuousLattice.scottSubspaceExtendInf_mono {D : Type u_3} [CompleteLattice D] {X : Type u_10} {Y : Type u_11} {e : X → Y} {f g₀ : X → D} (hfg : ∀ (x : X), f x ≤ g₀ x) (U : Set Y) : scottSubspaceExtendInf e f U ≤ scottSubspaceExtendInf e g₀ U

theorem Domain.ContinuousLattice.scottSubspaceExtend_mono {D : Type u_3} [CompleteLattice D] {X : Type u_10} {Y : Type u_11} [CompleteLattice Y] {e : X → Y} {f g₀ : X → D} (hfg : ∀ (x : X), f x ≤ g₀ x) (y : Y) : scottSubspaceExtend e f y ≤ scottSubspaceExtend e g₀ y

theorem Domain.ContinuousLattice.scottSubspaceExtendInf_eq_of_ext {D : Type u_3} [CompleteLattice D] {X : Type u_10} {Y : Type u_11} {e : X → Y} {f g' : X → D} (h : ∀ (x : X), f x = g' x) (U : Set Y) : scottSubspaceExtendInf e f U = scottSubspaceExtendInf e g' U

theorem Domain.ContinuousLattice.scottSubspaceExtend_eq_of_ext {D : Type u_3} [CompleteLattice D] {X : Type u_10} {Y : Type u_11} [CompleteLattice Y] {e : X → Y} {f g' : X → D} (h : ∀ (x : X), f x = g' x) (y : Y) : scottSubspaceExtend e f y = scottSubspaceExtend e g' y

theorem Domain.ContinuousLattice.scottSubspaceExtendInf_mono_retr {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] {X : Type u_10} {Y : Type u_11} {e : X → Y} {g : X → D'} (P : IsContinuousLatticeProjection D D') (U : Set Y) : ↑P.retr (scottSubspaceExtendInf e g U) ≤ scottSubspaceExtendInf e (fun (x : X) => ↑P.retr (g x)) U

theorem Domain.ContinuousLattice.scottSubspaceExtendInf_mono_incl {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] {X : Type u_10} {Y : Type u_11} {e : X → Y} {f : X → D} {g : X → D'} (P : IsContinuousLatticeProjection D D') (hfg : ∀ (x : X), f x = ↑P.retr (g x)) (U : Set Y) : scottSubspaceExtendInf e (fun (x : X) => ↑P.incl (f x)) U ≤ scottSubspaceExtendInf e g U

theorem Domain.ContinuousLattice.scottSubspaceExtendInf_mono_incl_apply {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] {X : Type u_10} {Y : Type u_11} {e : X → Y} {f : X → D} (U : Set Y) (P : IsContinuousLatticeProjection D D') : ↑P.incl (scottSubspaceExtendInf e f U) ≤ scottSubspaceExtendInf e (fun (x : X) => ↑P.incl (f x)) U

theorem Domain.ContinuousLattice.lemma_3_9_incl_inf {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] {X : Type u_10} {Y : Type u_11} {e : X → Y} (P : IsContinuousLatticeProjection D D') {f : X → D} {g : X → D'} (hfg : ∀ (x : X), f x = ↑P.retr (g x)) (U : Set Y) : ↑P.incl (scottSubspaceExtendInf e f U) ≤ scottSubspaceExtendInf e g U

Scott 1972, Lemma 3.9 (inclusion at infimum level). Used in the inverse-limit argument (Theorem 4.4).

theorem Domain.ContinuousLattice.lemma_3_9_retr_inf {D : Type u_3} {D' : Type u_4} [CompleteLattice D] [CompleteLattice D'] {X : Type u_10} {Y : Type u_11} {e : X → Y} (P : IsContinuousLatticeProjection D D') {g : X → D'} (U : Set Y) : ↑P.retr (scottSubspaceExtendInf e g U) ≤ scottSubspaceExtendInf e (fun (x : X) => ↑P.retr (g x)) U

Scott 1972, Lemma 3.9 (retraction at infimum level). The global equality fbar = j ∘ gbar assembles these infimum bounds via Proposition 3.10(i).

Definition 3.11 / Proposition 3.12: the lattice of projections J_D

def Domain.ContinuousLattice.IsProjection {D : Type u_3} [CompleteLattice D] (j : ScottMap D D) : Prop

Scott 1972, Definition 3.11. J_D = { j ∈ [D → D] : j = j ∘ j ⊑ id }: the Scott-continuous projections of D (idempotent self-maps below the identity), as a predicate on [D → D].

Equations

• Domain.ContinuousLattice.IsProjection j = (j.comp j = j ∧ j ≤ Domain.ContinuousLattice.ScottMap.idMap)

theorem Domain.ContinuousLattice.isProjection_iff {D : Type u_3} [CompleteLattice D] {j : ScottMap D D} : IsProjection j ↔ (∀ (x : D), ↑j (↑j x) = ↑j x) ∧ ∀ (x : D), ↑j x ≤ x

Pointwise characterization of projections: idempotent and deflationary.

theorem Domain.ContinuousLattice.isProjection_bot {D : Type u_3} [CompleteLattice D] : IsProjection ⊥

⊥ (the constant ⊥ map) is a projection — Scott's ⊔∅ ∈ J_D.

theorem Domain.ContinuousLattice.isProjection_sup {D : Type u_3} [CompleteLattice D] {j k : ScottMap D D} (hj : IsProjection j) (hk : IsProjection k) : IsProjection (j ⊔ k)

J_D is closed under binary joins (Scott 1972, 3.12). The key step: since j x ⊔ k x ⊑ x, monotonicity and idempotency force j (j x ⊔ k x) = j x and k (j x ⊔ k x) = k x.

theorem Domain.ContinuousLattice.isProjection_finsetSup {D : Type u_3} [CompleteLattice D] {T : Finset (ScottMap D D)} (hT : ∀ j ∈ T, IsProjection j) : IsProjection (T.sup id)

J_D is closed under finite joins.

theorem Domain.ContinuousLattice.isProjection_directedSup {D : Type u_3} [CompleteLattice D] {S : Set (ScottMap D D)} (hSne : S.Nonempty) (hSdir : DirectedOn (fun (x1 x2 : ScottMap D D) => x1 ≤ x2) S) (hS : ∀ j ∈ S, IsProjection j) : IsProjection (sSup S)

J_D is closed under directed joins (Scott 1972, 3.12). Continuity of each member lets the inner (⊔S)-application distribute over the directed family { j x : j ∈ S }, and directedness plus idempotency collapse the double family { k (j x) } to (⊔S) x.

theorem Domain.ContinuousLattice.isProjection_sSup {D : Type u_3} [CompleteLattice D] {T : Set (ScottMap D D)} (hT : ∀ j ∈ T, IsProjection j) : IsProjection (sSup T)

Scott 1972, Proposition 3.12 (⊔-closure). J_D is closed under arbitrary suprema in [D → D]: every supremum is the directed supremum of finite sub-joins (finsetSupOf), each a projection by isProjection_finsetSup.

@[reducible, inline]

abbrev Domain.ContinuousLattice.Projections (D : Type u_10) [CompleteLattice D] : Type u_10

Scott 1972, Definition 3.11. The space J_D of projections of D, as a subtype of [D → D].

Equations

• Domain.ContinuousLattice.Projections D = { j : Domain.ContinuousLattice.ScottMap D D // Domain.ContinuousLattice.IsProjection j }

@[implicit_reducible]

noncomputable instance Domain.ContinuousLattice.Projections.instSupSet {D : Type u_3} [CompleteLattice D] : SupSet (Projections D)

Equations

• Domain.ContinuousLattice.Projections.instSupSet = { sSup := fun (T : Set (Domain.ContinuousLattice.Projections D)) => ⟨sSup (Subtype.val '' T), ⋯⟩ }

theorem Domain.ContinuousLattice.Projections.isLUB_sSup {D : Type u_3} [CompleteLattice D] (T : Set (Projections D)) : IsLUB T (sSup T)

@[implicit_reducible]

noncomputable instance Domain.ContinuousLattice.Projections.instCompleteLattice {D : Type u_3} [CompleteLattice D] : CompleteLattice (Projections D)

Scott 1972, Proposition 3.12. J_D is a complete lattice (a ⊔-closed subspace of [D → D]). Suprema are inherited from [D → D]; infima are derived by completeLatticeOfSup.

Equations

• Domain.ContinuousLattice.Projections.instCompleteLattice = completeLatticeOfSup (Domain.ContinuousLattice.Projections D) ⋯

theorem Domain.ContinuousLattice.proposition_3_12 {D : Type u_3} [CompleteLattice D] : (∀ (T : Set (ScottMap D D)), (∀ j ∈ T, IsProjection j) → IsProjection (sSup T)) ∧ Nonempty (CompleteLattice (Projections D))

Scott 1972, Proposition 3.12. For a (complete, in particular continuous) lattice D, the projections J_D form a complete lattice as a ⊔-closed subspace of [D → D]: the ⊔-closure is isProjection_sSup, and the complete-lattice structure is Projections.instCompleteLattice.

Proposition 3.13: D is a projection of [D → D]

noncomputable def Domain.ContinuousLattice.Proposition313.con {D : Type u_3} [CompleteLattice D] : ScottMap D (ScottMap D D)

Scott 1972, Proposition 3.13. con : D → [D → D] sends x to the constant function x.

Equations

• Domain.ContinuousLattice.Proposition313.con = ⟨fun (x : D) => Domain.ContinuousLattice.ScottMap.const x, ⋯⟩

noncomputable def Domain.ContinuousLattice.Proposition313.min {D : Type u_3} [CompleteLattice D] : ScottMap (ScottMap D D) D

Scott 1972, Proposition 3.13. min : [D → D] → D sends f to its least value f(⊥).

Equations

• Domain.ContinuousLattice.Proposition313.min = ⟨fun (f : Domain.ContinuousLattice.ScottMap D D) => ↑f ⊥, ⋯⟩

@[simp]

theorem Domain.ContinuousLattice.Proposition313.con_apply {D : Type u_3} [CompleteLattice D] (x y : D) : ↑(↑con x) y = x

@[simp]

theorem Domain.ContinuousLattice.Proposition313.min_apply {D : Type u_3} [CompleteLattice D] (f : ScottMap D D) : ↑min f = ↑f ⊥

noncomputable def Domain.ContinuousLattice.Proposition313.projection {D : Type u_3} [CompleteLattice D] : IsContinuousLatticeProjection D (ScottMap D D)

Scott 1972, Proposition 3.13. (con, min) makes D a projection of [D → D]: min ∘ con = id (a constant's least value is its value) and con ∘ min ⊑ id (the constant f(⊥) is ≤ f pointwise, since f(⊥) ⊑ f(y) by monotonicity).

Equations

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

theorem Domain.ContinuousLattice.proposition_3_13 {D : Type u_3} [CompleteLattice D] (_hD : IsContinuousLattice D) : Nonempty (IsContinuousLatticeProjection D (ScottMap D D))

Scott 1972, Proposition 3.13. Every continuous lattice D is a projection of its function space [D → D], via con/min (Proposition313.projection).

Proposition 3.14: the fixed-point operator fix : [D → D] → D

def Domain.ContinuousLattice.Proposition314.toOrderHom {D : Type u_3} [CompleteLattice D] (f : ScottMap D D) : D →o D

The monotone map underlying a Scott map, suitable for OrderHom.lfp.

Equations

• Domain.ContinuousLattice.Proposition314.toOrderHom f = { toFun := ↑f, monotone' := ⋯ }

noncomputable def Domain.ContinuousLattice.Proposition314.fix {D : Type u_3} [CompleteLattice D] (f : ScottMap D D) : D

Scott 1972, Proposition 3.14. fix f is the least (pre-)fixed point of f, supplied by mathlib's OrderHom.lfp.

Equations

• Domain.ContinuousLattice.Proposition314.fix f = OrderHom.lfp (Domain.ContinuousLattice.Proposition314.toOrderHom f)

theorem Domain.ContinuousLattice.Proposition314.fix_eq {D : Type u_3} [CompleteLattice D] (f : ScottMap D D) : ↑f (fix f) = fix f

fix f is a fixed point of f.

theorem Domain.ContinuousLattice.Proposition314.fix_le {D : Type u_3} [CompleteLattice D] {f : ScottMap D D} {x : D} (h : ↑f x ≤ x) : fix f ≤ x

fix f is below every pre-fixed point: f x ⊑ x ⟹ fix f ⊑ x.

theorem Domain.ContinuousLattice.Proposition314.fix_mono {D : Type u_3} [CompleteLattice D] {f f' : ScottMap D D} (hff' : f ≤ f') : fix f ≤ fix f'

fix is monotone in f: if f ⊑ f' then fix f ⊑ fix f', since f (fix f') ⊑ f' (fix f') = fix f' makes fix f' a pre-fixed point of f.

theorem Domain.ContinuousLattice.Proposition314.fix_preservesDirectedSup {D : Type u_3} [CompleteLattice D] : PreservesDirectedSup fix

Scott 1972, Proposition 3.14 (continuity). fix preserves directed suprema. Direct lattice argument (no Kleene iteration): write g = ⊔S and a = ⊔{fix f : f ∈ S}. The reverse bound a ⊑ fix g is fix-monotonicity. For fix g ⊑ a it suffices (by fix_le) that a is a pre-fixed point of g. Now g a = ⊔_{f∈S} f a (pointwise sup), and each f a = ⊔_{f'∈S} f (fix f') (continuity of f on the directed family {fix f'}); for any f, f' ∈ S pick h ∈ S above both, so f (fix f') ⊑ h (fix f') ⊑ h (fix h) = fix h ⊑ a. Hence g a ⊑ a.

noncomputable def Domain.ContinuousLattice.Proposition314.fixMap {D : Type u_3} [CompleteLattice D] : ScottMap (ScottMap D D) D

Scott 1972, Proposition 3.14. The fixed-point operator as a Scott-continuous map.

Equations

• Domain.ContinuousLattice.Proposition314.fixMap = ⟨Domain.ContinuousLattice.Proposition314.fix, ⋯⟩

@[simp]

theorem Domain.ContinuousLattice.Proposition314.fixMap_apply {D : Type u_3} [CompleteLattice D] (f : ScottMap D D) : ↑fixMap f = fix f

theorem Domain.ContinuousLattice.Proposition314.fix_unique {D : Type u_3} [CompleteLattice D] {f : ScottMap D D} {a : D} (hfix : ↑f a = a) (hleast : ∀ (x : D), ↑f x ≤ x → a ≤ x) : a = fix f

Uniqueness: any value that is a fixed point of f and below every pre-fixed point equals fix f (the least fixed point is unique).

theorem Domain.ContinuousLattice.proposition_3_14 {D : Type u_3} [CompleteLattice D] (_hD : IsContinuousLattice D) : ∃ (Fix : ScottMap (ScottMap D D) D), (∀ (f : ScottMap D D), ↑f (↑Fix f) = ↑Fix f) ∧ (∀ (f : ScottMap D D) (x : D), ↑f x ≤ x → ↑Fix f ≤ x) ∧ ∀ (g : ScottMap D D → D), (∀ (f : ScottMap D D), ↑f (g f) = g f) → (∀ (f : ScottMap D D) (x : D), ↑f x ≤ x → g f ≤ x) → ∀ (f : ScottMap D D), g f = ↑Fix f

Scott 1972, Proposition 3.14. For a continuous lattice D there is a uniquely determined continuous mapping fix : [D → D] → D such that f (fix f) = fix f for all f, and fix f ⊑ x whenever f x ⊑ x. Existence and continuity are Proposition314.fixMap; the defining equations are fix_eq/fix_le; uniqueness (any operator with these two properties agrees with fix) is fix_unique.