Exercise 6.26 (Scott 1981, PRG-19, §6) — the lifting 𝒟_⊥ over {0,1}*

EXERCISE 6.26. For systems 𝒟 as in 6.19 define 𝒟_⊥ = {{Λ} ∪ 0Δ} ∪ {0X ∣ X ∈ 𝒟}. Describe the construct in terms of elements. Is this a suitable functor? Prove that 𝒟_⊥ ⊕ ℰ_⊥ ≅ 𝒟 + ℰ. What is 𝒟_⊥ ⊗ ℰ_⊥ ≅ ??

The lifting 𝒟_⊥ adds a new bottom below a 0-tagged copy of 𝒟. Its master is {Λ} ∪ 0Δ and its proper neighbourhoods are the 0X for X ∈ 𝒟 (including 0Δ, which sits strictly above the new bottom {{Λ} ∪ 0Δ}). It is the one-summand analogue of Exercise 6.19's sum.

Contents

• liftTok/ScottSys.lift — the lifted system over Str = {0,1}*, again ∅-free.
• Elements (liftBot, liftUp, unlift): |𝒟_⊥| ≅ |𝒟|_⊥. The bottom liftBot is the fresh least element; liftUp x embeds |𝒟| order-isomorphically above it (liftBot_lt_liftUp, liftUp_le_liftUp_iff); every element is one or the other (eq_liftBot_or_exists_liftUp).
• Functor (liftMapTok, liftMapTok_isStrict, liftMapTok_id, liftMapTok_comp): yes, (·)_⊥ is a (strict) functor on Scott's category — the action on maps preserves identities and composition.
• 𝒟_⊥ ⊕ ℰ_⊥ ≅ᴰ 𝒟 + ℰ (lift_oplus_lift_iso_sum): coalescing the two fresh bottoms of the lifts reproduces exactly the separated sum.
• 𝒟_⊥ ⊗ ℰ_⊥ ≅ᴰ (𝒟 × ℰ)_⊥ (lift_otimes_lift_iso_lift_prod): the answer to Scott's ?? — the smash of two lifts is the lift of the product.

All constructions are choice-free (#print axioms ⊆ {propext, Quot.sound}); the lone exception is eq_liftBot_or_exists_liftUp, a Prop-level case split that uses excluded middle (Classical) to decide whether an element lies above the fresh bottom — unavoidable and called out there.

The lifted system 𝒟_⊥ over {0,1}*

def Domain.Neighborhood.Exercise619.liftTokMaster (D : NeighborhoodSystem ExampleB.Str) : Set ExampleB.Str

The master neighbourhood {Λ} ∪ 0Δ of the lift.

Equations

• Domain.Neighborhood.Exercise619.liftTokMaster D = insert [] (Domain.Neighborhood.Example62.embBit false D.master)

theorem Domain.Neighborhood.Exercise619.nil_mem_liftTokMaster {D : NeighborhoodSystem ExampleB.Str} : [] ∈ liftTokMaster D

theorem Domain.Neighborhood.Exercise619.embF_subset_liftTokMaster {D : NeighborhoodSystem ExampleB.Str} {X : Set ExampleB.Str} (hX : D.mem X) : Example62.embBit false X ⊆ liftTokMaster D

theorem Domain.Neighborhood.Exercise619.liftTokMaster_inter_embF {D : NeighborhoodSystem ExampleB.Str} {X : Set ExampleB.Str} (hX : D.mem X) : liftTokMaster D ∩ Example62.embBit false X = Example62.embBit false X

theorem Domain.Neighborhood.Exercise619.embF_ne_liftTokMaster {D : NeighborhoodSystem ExampleB.Str} {X : Set ExampleB.Str} : Example62.embBit false X ≠ liftTokMaster D

def Domain.Neighborhood.Exercise619.liftTok (D : NeighborhoodSystem ExampleB.Str) : NeighborhoodSystem ExampleB.Str

Exercise 6.26 — the lifted system 𝒟_⊥ over {0,1}*. A neighbourhood is the master {Λ} ∪ 0Δ or a tagged copy 0X (X ∈ 𝒟). ∅-freeness of 𝒟 (hD) keeps it ∅-free.

Equations

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

theorem Domain.Neighborhood.Exercise619.liftTok_nonempty {D : NeighborhoodSystem ExampleB.Str} (hD : ∀ (X : Set ExampleB.Str), D.mem X → X.Nonempty) (W : Set ExampleB.Str) : (liftTok D).mem W → W.Nonempty

def Domain.Neighborhood.Exercise619.ScottSys.lift (A : ScottSys) : ScottSys

The lift object 𝒟_⊥ of Scott's category.

Equations

• A.lift = { sys := Domain.Neighborhood.Exercise619.liftTok A.sys, ne := ⋯ }

theorem Domain.Neighborhood.Exercise619.liftTok_mem_master {D : NeighborhoodSystem ExampleB.Str} : (liftTok D).mem (liftTokMaster D)

theorem Domain.Neighborhood.Exercise619.liftTok_mem_embF {D : NeighborhoodSystem ExampleB.Str} {X : Set ExampleB.Str} (hX : D.mem X) : (liftTok D).mem (Example62.embBit false X)

theorem Domain.Neighborhood.Exercise619.liftTok_mem_embF_inv {D : NeighborhoodSystem ExampleB.Str} {W : Set ExampleB.Str} (h : (liftTok D).mem (Example62.embBit false W)) : D.mem W

Elements: |𝒟_⊥| ≅ |𝒟|_⊥

def Domain.Neighborhood.Exercise619.liftBot (D : NeighborhoodSystem ExampleB.Str) : (liftTok D).Element

The fresh bottom of 𝒟_⊥: the element whose only neighbourhood is the master {Λ} ∪ 0Δ.

Equations

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

def Domain.Neighborhood.Exercise619.liftUp {D : NeighborhoodSystem ExampleB.Str} (x : D.Element) : (liftTok D).Element

The embedding |𝒟| ↪ |𝒟_⊥|: liftUp x = {{Λ} ∪ 0Δ} ∪ {0X ∣ X ∈ x}, the image of x sitting above the fresh bottom.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise619.mem_liftBot {D : NeighborhoodSystem ExampleB.Str} {W : Set ExampleB.Str} : (liftBot D).mem W ↔ W = liftTokMaster D

@[simp]

theorem Domain.Neighborhood.Exercise619.mem_liftUp {D : NeighborhoodSystem ExampleB.Str} {x : D.Element} {W : Set ExampleB.Str} : (liftUp x).mem W ↔ W = liftTokMaster D ∨ ∃ (X : Set ExampleB.Str), x.mem X ∧ W = Example62.embBit false X

theorem Domain.Neighborhood.Exercise619.liftBot_le {D : NeighborhoodSystem ExampleB.Str} (z : (liftTok D).Element) : liftBot D ≤ z

liftBot is the least element of 𝒟_⊥.

theorem Domain.Neighborhood.Exercise619.liftUp_le_liftUp_iff {D : NeighborhoodSystem ExampleB.Str} {x y : D.Element} : liftUp x ≤ liftUp y ↔ x ≤ y

liftUp is an order embedding: liftUp x ⊑ liftUp y ↔ x ⊑ y.

theorem Domain.Neighborhood.Exercise619.liftBot_lt_liftUp {D : NeighborhoodSystem ExampleB.Str} (x : D.Element) : liftBot D < liftUp x

The fresh bottom is strictly below every lifted element.

def Domain.Neighborhood.Exercise619.unlift {D : NeighborhoodSystem ExampleB.Str} (z : (liftTok D).Element) (hz : z.mem (Example62.embBit false D.master)) : D.Element

The unlift of an element that lies above the fresh bottom (i.e. contains 0Δ): the 𝒟-element {X ∣ 0X ∈ z}.

Equations

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

theorem Domain.Neighborhood.Exercise619.liftUp_unlift {D : NeighborhoodSystem ExampleB.Str} (z : (liftTok D).Element) (hz : z.mem (Example62.embBit false D.master)) : liftUp (unlift z hz) = z

theorem Domain.Neighborhood.Exercise619.eq_liftBot_or_exists_liftUp {D : NeighborhoodSystem ExampleB.Str} (z : (liftTok D).Element) : z = liftBot D ∨ ∃ (x : D.Element), z = liftUp x

Exercise 6.26 — "describe in terms of elements". Every element of 𝒟_⊥ is either the fresh bottom or a lifted 𝒟-element: |𝒟_⊥| ≅ |𝒟|_⊥. (Prop-level; the case split on "does z contain 0Δ?" uses excluded middle — the only non-constructive step in this module.)

Functoriality: (·)_⊥ is a strict functor

def Domain.Neighborhood.Exercise619.liftMapTok {A B : ScottSys} (f : ApproximableMap A.sys B.sys) : ApproximableMap A.lift.sys B.lift.sys

f_⊥, the action of lifting on (approximable) maps. It carries the master to the master (so it is strict) and a copy 0X to 0X' whenever X f X'.

Equations

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

theorem Domain.Neighborhood.Exercise619.liftMapTok_isStrict {A B : ScottSys} (f : ApproximableMap A.sys B.sys) : Exercise510.IsStrict (liftMapTok f)

f_⊥ is strict for any f: the master Λ-bearing input relates only to the master.

theorem Domain.Neighborhood.Exercise619.liftMapTok_id {A : ScottSys} : liftMapTok (ApproximableMap.idMap A.sys) = ApproximableMap.idMap A.lift.sys

(I_𝒟)_⊥ = I_{𝒟_⊥}.

theorem Domain.Neighborhood.Exercise619.liftMapTok_comp {A B C : ScottSys} (f : ApproximableMap A.sys B.sys) (g : ApproximableMap B.sys C.sys) : liftMapTok (g.comp f) = (liftMapTok g).comp (liftMapTok f)

(g ∘ f)_⊥ = g_⊥ ∘ f_⊥.

𝒟_⊥ ⊕ ℰ_⊥ ≅ᴰ 𝒟 + ℰ

The coalesced sum of the two lifts has tokens 0·0·X' (X' ∈ 𝒟) and 1·0·Y' (Y' ∈ ℰ), with the shared bottom {Λ} ∪ 0(liftTokMaster 𝒟) ∪ 1(liftTokMaster ℰ). The separated sum 𝒟 + ℰ has tokens 0X', 1Y'. The element iso simply deletes the inner 0. The cross-tag intersections vanish (∅-freeness), exactly as in Exercise 6.19's toSum/fromSum.

theorem Domain.Neighborhood.Exercise619.o_mem_embFF {D E : ScottSys} {X' : Set ExampleB.Str} (hX' : D.sys.mem X') : (D.lift.oplus E.lift).sys.mem (Example62.embBit false (Example62.embBit false X'))

theorem Domain.Neighborhood.Exercise619.o_mem_embTF {D E : ScottSys} {Y' : Set ExampleB.Str} (hY' : E.sys.mem Y') : (D.lift.oplus E.lift).sys.mem (Example62.embBit true (Example62.embBit false Y'))

theorem Domain.Neighborhood.Exercise619.o_embFF_inv {D E : ScottSys} {W : Set ExampleB.Str} (h : (D.lift.oplus E.lift).sys.mem (Example62.embBit false (Example62.embBit false W))) : D.sys.mem W

theorem Domain.Neighborhood.Exercise619.o_embTF_inv {D E : ScottSys} {W : Set ExampleB.Str} (h : (D.lift.oplus E.lift).sys.mem (Example62.embBit true (Example62.embBit false W))) : E.sys.mem W

def Domain.Neighborhood.Exercise619.toSumLift {D E : ScottSys} (z : (D.lift.oplus E.lift).sys.Element) : (D.sum E).sys.Element

The forward half |𝒟_⊥ ⊕ ℰ_⊥| → |𝒟 + ℰ|: delete the inner 0.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise619.toSumLift_mem_embF {D E : ScottSys} {z : (D.lift.oplus E.lift).sys.Element} {X : Set ExampleB.Str} (hX : D.sys.mem X) : (toSumLift z).mem (Example62.embBit false X) ↔ z.mem (Example62.embBit false (Example62.embBit false X))

@[simp]

theorem Domain.Neighborhood.Exercise619.toSumLift_mem_embT {D E : ScottSys} {z : (D.lift.oplus E.lift).sys.Element} {Y : Set ExampleB.Str} (hY : E.sys.mem Y) : (toSumLift z).mem (Example62.embBit true Y) ↔ z.mem (Example62.embBit true (Example62.embBit false Y))

def Domain.Neighborhood.Exercise619.fromSumLift {D E : ScottSys} (s : (D.sum E).sys.Element) : (D.lift.oplus E.lift).sys.Element

The inverse half |𝒟 + ℰ| → |𝒟_⊥ ⊕ ℰ_⊥|: reinstate the inner 0.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise619.fromSumLift_mem_embFF {D E : ScottSys} {s : (D.sum E).sys.Element} {X : Set ExampleB.Str} (hX : D.sys.mem X) : (fromSumLift s).mem (Example62.embBit false (Example62.embBit false X)) ↔ s.mem (Example62.embBit false X)

@[simp]

theorem Domain.Neighborhood.Exercise619.fromSumLift_mem_embTF {D E : ScottSys} {s : (D.sum E).sys.Element} {Y : Set ExampleB.Str} (hY : E.sys.mem Y) : (fromSumLift s).mem (Example62.embBit true (Example62.embBit false Y)) ↔ s.mem (Example62.embBit true Y)

theorem Domain.Neighborhood.Exercise619.fromSumLift_toSumLift {D E : ScottSys} (z : (D.lift.oplus E.lift).sys.Element) : fromSumLift (toSumLift z) = z

theorem Domain.Neighborhood.Exercise619.toSumLift_fromSumLift {D E : ScottSys} (s : (D.sum E).sys.Element) : toSumLift (fromSumLift s) = s

def Domain.Neighborhood.Exercise619.sumLiftEquiv {D E : ScottSys} : (D.lift.oplus E.lift).sys.Element ≃o (D.sum E).sys.Element

The order-isomorphism |𝒟_⊥ ⊕ ℰ_⊥| ≃o |𝒟 + ℰ|.

Equations

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

theorem Domain.Neighborhood.Exercise619.lift_oplus_lift_iso_sum {D E : ScottSys} : (D.lift.oplus E.lift).sys ≅ᴰ (D.sum E).sys

Exercise 6.26 — 𝒟_⊥ ⊕ ℰ_⊥ ≅ 𝒟 + ℰ. Coalescing the fresh bottoms of the two lifts reproduces the separated sum.

𝒟_⊥ ⊗ ℰ_⊥ ≅ᴰ (𝒟 × ℰ)_⊥ — the answer to Scott's ??

The smash of the two lifts has proper neighbourhoods {Λ} ∪ 0(0X') ∪ 1(0Y') (i.e. prodTokNbhd (0X') (0Y'), with X' ∈ 𝒟, Y' ∈ ℰ). The lift of the product has proper neighbourhoods 0(prodTokNbhd X' Y'). The element iso transports one rectangle presentation to the other. Unlike the sum there are no cross-tag intersections, so the proof is purely "rectangular".

theorem Domain.Neighborhood.Exercise619.ot_mem_prod {D E : ScottSys} {X' Y' : Set ExampleB.Str} (hX' : D.sys.mem X') (hY' : E.sys.mem Y') : (D.lift.otimes E.lift).sys.mem (prodTokNbhd (Example62.embBit false X') (Example62.embBit false Y'))

theorem Domain.Neighborhood.Exercise619.ot_mem_prod_inv {D E : ScottSys} {X' Y' : Set ExampleB.Str} (h : (D.lift.otimes E.lift).sys.mem (prodTokNbhd (Example62.embBit false X') (Example62.embBit false Y'))) : D.sys.mem X' ∧ E.sys.mem Y'

theorem Domain.Neighborhood.Exercise619.lp_mem_embF {D E : ScottSys} {X' Y' : Set ExampleB.Str} (hX' : D.sys.mem X') (hY' : E.sys.mem Y') : (D.prod E).lift.sys.mem (Example62.embBit false (prodTokNbhd X' Y'))

theorem Domain.Neighborhood.Exercise619.lp_prod_inv {D E : ScottSys} {X' Y' : Set ExampleB.Str} (h : (D.prod E).lift.sys.mem (Example62.embBit false (prodTokNbhd X' Y'))) : D.sys.mem X' ∧ E.sys.mem Y'

def Domain.Neighborhood.Exercise619.toLiftProd {D E : ScottSys} (z : (D.lift.otimes E.lift).sys.Element) : (D.prod E).lift.sys.Element

The forward half |𝒟_⊥ ⊗ ℰ_⊥| → |(𝒟 × ℰ)_⊥|.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise619.toLiftProd_mem_embF {D E : ScottSys} {z : (D.lift.otimes E.lift).sys.Element} {X Y : Set ExampleB.Str} (hX : D.sys.mem X) (hY : E.sys.mem Y) : (toLiftProd z).mem (Example62.embBit false (prodTokNbhd X Y)) ↔ z.mem (prodTokNbhd (Example62.embBit false X) (Example62.embBit false Y))

def Domain.Neighborhood.Exercise619.fromLiftProd {D E : ScottSys} (s : (D.prod E).lift.sys.Element) : (D.lift.otimes E.lift).sys.Element

The inverse half |(𝒟 × ℰ)_⊥| → |𝒟_⊥ ⊗ ℰ_⊥|.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise619.fromLiftProd_mem_prod {D E : ScottSys} {s : (D.prod E).lift.sys.Element} {X Y : Set ExampleB.Str} (hX : D.sys.mem X) (hY : E.sys.mem Y) : (fromLiftProd s).mem (prodTokNbhd (Example62.embBit false X) (Example62.embBit false Y)) ↔ s.mem (Example62.embBit false (prodTokNbhd X Y))

theorem Domain.Neighborhood.Exercise619.fromLiftProd_toLiftProd {D E : ScottSys} (z : (D.lift.otimes E.lift).sys.Element) : fromLiftProd (toLiftProd z) = z

theorem Domain.Neighborhood.Exercise619.toLiftProd_fromLiftProd {D E : ScottSys} (s : (D.prod E).lift.sys.Element) : toLiftProd (fromLiftProd s) = s

def Domain.Neighborhood.Exercise619.liftProdEquiv {D E : ScottSys} : (D.lift.otimes E.lift).sys.Element ≃o (D.prod E).lift.sys.Element

The order-isomorphism |𝒟_⊥ ⊗ ℰ_⊥| ≃o |(𝒟 × ℰ)_⊥|.

Equations

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

theorem Domain.Neighborhood.Exercise619.lift_otimes_lift_iso_lift_prod {D E : ScottSys} : (D.lift.otimes E.lift).sys ≅ᴰ (D.prod E).lift.sys

Exercise 6.26 — 𝒟_⊥ ⊗ ℰ_⊥ ≅ (𝒟 × ℰ)_⊥ (the answer to Scott's ??). The smash product of two lifts is the lift of the product.