Mathlib.Order.ScottContinuity

Module docstring

{"# Scott continuity

A function f : α → β between preorders is Scott continuous (referring to Dana Scott) if it distributes over IsLUB. Scott continuity corresponds to continuity in Scott topological spaces (defined in Mathlib/Topology/Order/ScottTopology.lean). It is distinct from the (more commonly used) continuity from topology (see Mathlib/Topology/Basic.lean).

Implementation notes

Given a set D of directed sets, we define say f is ScottContinuousOn D if it distributes over IsLUB for all elements of D. This allows us to consider Scott Continuity on all directed sets in this file, and ωScott Continuity on chains later in Mathlib/Order/OmegaCompletePartialOrder.lean.

References

[Abramsky and Jung, Domain Theory][abramskygabbaymaibaum_1994]
[Gierz et al, A Compendium of Continuous Lattices][GierzEtAl1980]

ScottContinuousOn definition

(D : Set (Set α)) (f : α → β) : Prop

Full source

/-- A function between preorders is said to be Scott continuous on a set `D` of directed sets if it
preserves `IsLUB` on elements of `D`.

The dual notion

```lean
∀ ⦃d : Set α⦄, d ∈ D →  d.Nonempty → DirectedOn (· ≥ ·) d → ∀ ⦃a⦄, IsGLB d a → IsGLB (f '' d) (f a)
```

does not appear to play a significant role in the literature, so is omitted here.
-/
def ScottContinuousOn (D : Set (Set α)) (f : α → β) : Prop :=
  ∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → DirectedOn (· ≤ ·) d → ∀ ⦃a⦄, IsLUB d a → IsLUB (f '' d) (f a)

Scott continuity on directed sets

Informal description

A function $f : \alpha \to \beta$ between preorders is called *Scott continuous* on a set $D$ of directed subsets of $\alpha$ if for every nonempty directed subset $d \in D$ with a least upper bound $a$, the image $f(d)$ has $f(a)$ as its least upper bound. That is, $f$ preserves least upper bounds for all directed sets in $D$.

ScottContinuousOn.mono theorem

(hD : D₁ ⊆ D₂) (hf : ScottContinuousOn D₂ f) : ScottContinuousOn D₁ f

Full source

lemma ScottContinuousOn.mono (hD : D₁ ⊆ D₂) (hf : ScottContinuousOn D₂ f) :
    ScottContinuousOn D₁ f := fun _  hdD₁ hd₁ hd₂ _ hda => hf (hD hdD₁) hd₁ hd₂ hda

Monotonicity of Scott Continuity with Respect to Directed Sets

Informal description

Let $D_1$ and $D_2$ be sets of directed subsets of a preorder $\alpha$ such that $D_1 \subseteq D_2$. If a function $f : \alpha \to \beta$ is Scott continuous on $D_2$, then $f$ is also Scott continuous on $D_1$.

ScottContinuousOn.monotone theorem

(D : Set (Set α)) (hD : ∀ a b : α, a ≤ b → { a, b } ∈ D) (h : ScottContinuousOn D f) : Monotone f

Full source

protected theorem ScottContinuousOn.monotone (D : Set (Set α)) (hD : ∀ a b : α, a ≤ b → {a, b}{a, b} ∈ D)
    (h : ScottContinuousOn D f) : Monotone f := by
  refine fun a b hab =>
    (h (hD a b hab) (insert_nonempty _ _) (directedOn_pair le_refl hab) ?_).1
      (mem_image_of_mem _ <| mem_insert _ _)
  rw [IsLUB, upperBounds_insert, upperBounds_singleton,
    inter_eq_self_of_subset_right (Ici_subset_Ici.2 hab)]
  exact isLeast_Ici

Monotonicity of Scott Continuous Functions on Directed Sets

Informal description

Let $D$ be a set of directed subsets of a preorder $\alpha$ such that for any two elements $a, b \in \alpha$ with $a \leq b$, the set $\{a, b\}$ belongs to $D$. If a function $f : \alpha \to \beta$ is Scott continuous on $D$, then $f$ is monotone. That is, for any $a, b \in \alpha$ with $a \leq b$, we have $f(a) \leq f(b)$.

ScottContinuousOn.id theorem

: ScottContinuousOn D (id : α → α)

Full source

@[simp] lemma ScottContinuousOn.id : ScottContinuousOn D (id : α → α) := by simp [ScottContinuousOn]

Scott Continuity of the Identity Function

Informal description

The identity function $\mathrm{id} : \alpha \to \alpha$ is Scott continuous on any set $D$ of directed subsets of a preorder $\alpha$. That is, for every nonempty directed subset $d \in D$ with a least upper bound $a$, the image $\mathrm{id}(d)$ has $\mathrm{id}(a) = a$ as its least upper bound.

ScottContinuousOn.prodMk theorem

 (hD : ∀ a b : α, a ≤ b → { a, b } ∈ D) (hf : ScottContinuousOn D f) (hg : ScottContinuousOn D g) :
  ScottContinuousOn D fun x => (f x, g x)

Full source

lemma ScottContinuousOn.prodMk (hD : ∀ a b : α, a ≤ b → {a, b}{a, b} ∈ D)
    (hf : ScottContinuousOn D f) (hg : ScottContinuousOn D g) :
    ScottContinuousOn D fun x => (f x, g x) := fun d hd₁ hd₂ hd₃ a hda => by
  rw [IsLUB, IsLeast, upperBounds]
  constructor
  · simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq,
      Prod.mk_le_mk]
    intro b hb
    exact ⟨hf.monotone D hD (hda.1 hb), hg.monotone D hD (hda.1 hb)⟩
  · intro ⟨p₁, p₂⟩ hp
    simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq,
      Prod.mk_le_mk] at hp
    constructor
    · rw [isLUB_le_iff (hf hd₁ hd₂ hd₃ hda), upperBounds]
      simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq]
      intro _ hb
      exact (hp _ hb).1
    · rw [isLUB_le_iff (hg hd₁ hd₂ hd₃ hda), upperBounds]
      simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq]
      intro _ hb
      exact (hp _ hb).2

Scott Continuity of the Product of Two Scott Continuous Functions

Informal description

Let $\alpha$ and $\beta$ be preorders, and let $D$ be a set of directed subsets of $\alpha$ such that for any $a, b \in \alpha$ with $a \leq b$, the set $\{a, b\}$ belongs to $D$. If $f : \alpha \to \beta$ and $g : \alpha \to \beta$ are Scott continuous on $D$, then the function $x \mapsto (f(x), g(x))$ is also Scott continuous on $D$.

ScottContinuous definition

(f : α → β) : Prop

Full source

/-- A function between preorders is said to be Scott continuous if it preserves `IsLUB` on directed
sets. It can be shown that a function is Scott continuous if and only if it is continuous wrt the
Scott topology.
-/
def ScottContinuous (f : α → β) : Prop :=
  ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (· ≤ ·) d → ∀ ⦃a⦄, IsLUB d a → IsLUB (f '' d) (f a)

Scott continuous function

Informal description

A function $f : \alpha \to \beta$ between preorders is called *Scott continuous* if for every nonempty directed subset $d \subseteq \alpha$ with respect to the order $\leq$, and for every least upper bound $a$ of $d$, the image $f(d)$ has $f(a)$ as its least upper bound. In other words, $f$ preserves least upper bounds of directed sets.

scottContinuousOn_univ theorem

: ScottContinuousOn univ f ↔ ScottContinuous f

Full source

@[simp] lemma scottContinuousOn_univ : ScottContinuousOnScottContinuousOn univ f ↔ ScottContinuous f := by
  simp [ScottContinuousOn, ScottContinuous]

Equivalence of Scott Continuity on Universal Set and General Scott Continuity

Informal description

A function $f : \alpha \to \beta$ between preorders is Scott continuous on the universal set of directed subsets of $\alpha$ if and only if it is Scott continuous. That is, $f$ preserves least upper bounds of all nonempty directed subsets of $\alpha$ precisely when it preserves least upper bounds of directed sets in general.

ScottContinuous.scottContinuousOn theorem

{D : Set (Set α)} : ScottContinuous f → ScottContinuousOn D f

Full source

lemma ScottContinuous.scottContinuousOn {D : Set (Set α)} :
    ScottContinuous f → ScottContinuousOn D f := fun h _ _ d₂ d₃ _ hda => h d₂ d₃ hda

Scott continuity implies Scott continuity on any set of directed subsets

Informal description

If a function $f : \alpha \to \beta$ between preorders is Scott continuous, then it is Scott continuous on any set $D$ of directed subsets of $\alpha$.

ScottContinuous.monotone theorem

(h : ScottContinuous f) : Monotone f

Full source

protected theorem ScottContinuous.monotone (h : ScottContinuous f) : Monotone f :=
  h.scottContinuousOn.monotone univ (fun _ _ _ ↦ mem_univ _)

Monotonicity of Scott Continuous Functions

Informal description

If a function $f : \alpha \to \beta$ between preorders is Scott continuous, then it is monotone. That is, for any $a, b \in \alpha$ with $a \leq b$, we have $f(a) \leq f(b)$.

ScottContinuous.id theorem

: ScottContinuous (id : α → α)

Full source

@[simp] lemma ScottContinuous.id : ScottContinuous (id : α → α) := by simp [ScottContinuous]

Scott Continuity of the Identity Function

Informal description

The identity function $\mathrm{id} : \alpha \to \alpha$ on a preorder $\alpha$ is Scott continuous. That is, for every nonempty directed subset $d \subseteq \alpha$ with a least upper bound $a$, the identity function preserves the least upper bound, meaning $\mathrm{id}(a)$ is the least upper bound of $\mathrm{id}(d)$.

ScottContinuousOn.sup₂ theorem

{D : Set (Set (β × β))} : ScottContinuousOn D fun (a, b) => (a ⊔ b : β)

Full source

lemma ScottContinuousOn.sup₂ {D : Set (Set (β × β))} :
    ScottContinuousOn D fun (a, b) => (a ⊔ b : β) := by
  simp only
  intro d _ _ _ ⟨p₁, p₂⟩ hdp
  rw [IsLUB, IsLeast, upperBounds] at hdp
  simp only [Prod.forall, mem_setOf_eq, Prod.mk_le_mk] at hdp
  rw [IsLUB, IsLeast, upperBounds]
  constructor
  · simp only [mem_image, Prod.exists, forall_exists_index, and_imp, mem_setOf_eq]
    intro a b₁ b₂ hbd hba
    rw [← hba]
    exact sup_le_sup (hdp.1 _ _ hbd).1 (hdp.1 _ _ hbd).2
  · simp only [mem_image, Prod.exists, forall_exists_index, and_imp]
    intro b hb
    simp only [sup_le_iff]
    have e1 : (p₁, p₂)(p₁, p₂) ∈ lowerBounds {x | ∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → (b₁, b₂) ≤ x} := hdp.2
    rw [lowerBounds] at e1
    simp only [mem_setOf_eq, Prod.forall, Prod.mk_le_mk] at e1
    apply e1
    intro b₁ b₂ hb'
    exact sup_le_iff.mp (hb b₁ b₂ hb' rfl)

Scott Continuity of the Supremum Operation on Directed Sets

Informal description

For any set $D$ of directed subsets of $\beta \times \beta$, the supremum operation $(a, b) \mapsto a \sqcup b$ is Scott continuous on $D$. That is, for every nonempty directed subset $d \in D$ with a least upper bound $(a, b)$, the image of $d$ under the supremum operation has $a \sqcup b$ as its least upper bound.