Exercise 3.17 (Scott 1981, PRG-19, §3) — B is a retract of T^∞

Using the binary system B (Example 1.B) and the three-element truth system T (Example 1.2), Scott asks for a one-one approximable map f : B → T^∞ and a map g : T^∞ → B with

g ∘ f = I_B and f ∘ g ⊑ I_{T^∞},

i.e. B is a retract of T^∞ (f a section, g a retraction). He then asks whether B ≅ T^∞ and B ≅ T × B (the point of the exercise being that retract ≠ isomorphism here).

The encoding. A binary string σ = b₀b₁…b_{k-1} (a neighbourhood σΣ* of B) is sent to the T^∞-neighbourhood encSet σ that pins copy i to the truth value bitNbhd bᵢ ({0} for false, {1} for true) for i < k, and leaves copies i ≥ k free (Δ_T). Concretely encSet σ is the pointwise set {(i, t) ∣ ∀ b, σ[i]? = some b → t ∈ bitNbhd b}.

• f relates σΣ* to every T^∞-neighbourhood weaker than encSet σ;
• g relates a T^∞-neighbourhood W to τΣ* exactly when W ⊆ encSet τ, i.e. W already pins the first |τ| copies to τ (decoding the longest gap-free prefix).

g ∘ f = I_B (gf_eq_id) — decoding recovers the prefix, the key being prefix_of_encSet_subset (encSet σ ⊆ encSet τ ⟹ τ prefix σ), which uses that T-neighbourhoods are non-empty. f ∘ g ⊑ I_{T^∞} (fg_le_id) holds because re-encoding a decoded element can only lose the post-gap information. Hence f is one-one (f_injective).

@[reducible, inline]

abbrev Domain.Neighborhood.Exercise317.T : NeighborhoodSystem Example12.Token

The truth domain T of Example 1.2.

Equations

• Domain.Neighborhood.Exercise317.T = Domain.Neighborhood.Example12.neighborhoodSystem

@[reducible, inline]

abbrev Domain.Neighborhood.Exercise317.Token : Type

Tokens of T: {0, 1}.

Equations

• Domain.Neighborhood.Exercise317.Token = Domain.Neighborhood.Example12.Token

def Domain.Neighborhood.Exercise317.bitNbhd : Bool → Set Token

The T-neighbourhood selected by a bit: false ↦ {0}, true ↦ {1}.

Equations

• Domain.Neighborhood.Exercise317.bitNbhd false = Domain.Neighborhood.Example12.zero
• Domain.Neighborhood.Exercise317.bitNbhd true = Domain.Neighborhood.Example12.one

theorem Domain.Neighborhood.Exercise317.bitNbhd_mem (b : Bool) : T.mem (bitNbhd b)

theorem Domain.Neighborhood.Exercise317.exists_not_mem_bitNbhd (b : Bool) : ∃ (t : Token), t ∉ bitNbhd b

theorem Domain.Neighborhood.Exercise317.T_nbhd_nonempty {F : Set Token} (hF : T.mem F) : F.Nonempty

T-neighbourhoods are non-empty (∅ ∉ T).

The encoding set encSet σ.

def Domain.Neighborhood.Exercise317.encSet (σ : ExampleB.Str) : Set (ℕ × Token)

encSet σ ⊆ ℕ × {0,1}: pin copy i to bitNbhd σ[i] for i < |σ|, free otherwise.

Equations

• Domain.Neighborhood.Exercise317.encSet σ = {p : ℕ × Domain.Neighborhood.Exercise317.Token | ∀ (b : Bool), σ[p.1]? = some b → p.2 ∈ Domain.Neighborhood.Exercise317.bitNbhd b}

@[simp]

theorem Domain.Neighborhood.Exercise317.mem_encSet {σ : ExampleB.Str} {p : ℕ × Token} : p ∈ encSet σ ↔ ∀ (b : Bool), σ[p.1]? = some b → p.2 ∈ bitNbhd b

theorem Domain.Neighborhood.Exercise317.fiber_encSet_some {σ : ExampleB.Str} {i : ℕ} {b : Bool} (h : σ[i]? = some b) : fiber (encSet σ) i = bitNbhd b

theorem Domain.Neighborhood.Exercise317.fiber_encSet_none {σ : ExampleB.Str} {i : ℕ} (h : σ[i]? = none) : fiber (encSet σ) i = Set.univ

@[simp]

theorem Domain.Neighborhood.Exercise317.encSet_nil : encSet [] = Set.univ

theorem Domain.Neighborhood.Exercise317.encSet_mem (σ : ExampleB.Str) : (iterSys T).mem (encSet σ)

encSet σ is a T^∞-neighbourhood.

theorem Domain.Neighborhood.Exercise317.encSet_anti {σ σ' : ExampleB.Str} (h : σ <+: σ') : encSet σ' ⊆ encSet σ

A longer prefix encodes to a smaller set: σ prefix σ' ⟹ encSet σ' ⊆ encSet σ.

Comparability and the prefix recovery lemma.

theorem Domain.Neighborhood.Exercise317.encSet_agree {τ τ' : ExampleB.Str} {W : Set (ℕ × Token)} (hW : (iterSys T).mem W) (h : W ⊆ encSet τ) (h' : W ⊆ encSet τ') {i : ℕ} {b b' : Bool} (hb : τ[i]? = some b) (hb' : τ'[i]? = some b') : b = b'

Two prefixes that both bound a common non-empty T^∞-neighbourhood agree where both defined.

theorem Domain.Neighborhood.Exercise317.comparable_of_agree {τ τ' : ExampleB.Str} : (∀ (i : ℕ) (b b' : Bool), τ[i]? = some b → τ'[i]? = some b' → b = b') → τ <+: τ' ∨ τ' <+: τ

theorem Domain.Neighborhood.Exercise317.prefix_of_encSet_subset {σ τ : ExampleB.Str} (h : encSet σ ⊆ encSet τ) : τ <+: σ

Prefix recovery. encSet σ ⊆ encSet τ forces τ to be an initial segment of σ.

The section f : B → T^∞ and retraction g : T^∞ → B.

def Domain.Neighborhood.Exercise317.f : ApproximableMap ExampleB.B (iterSys T)

The encoding map f : B → T^∞. Relates the cone σΣ* to every T^∞-neighbourhood weaker than encSet σ.

Equations

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

def Domain.Neighborhood.Exercise317.g : ApproximableMap (iterSys T) ExampleB.B

The decoding map g : T^∞ → B. Relates W to the cone τΣ* exactly when W ⊆ encSet τ, i.e. W pins the first |τ| copies to τ.

Equations

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

g ∘ f = I_B and f ∘ g ⊑ I_{T^∞}.

theorem Domain.Neighborhood.Exercise317.gf_eq_id : g.comp f = ApproximableMap.idMap ExampleB.B

Exercise 3.17 — g is a retraction of f. g ∘ f = I_B.

theorem Domain.Neighborhood.Exercise317.fg_le_id : f.comp g ≤ ApproximableMap.idMap (iterSys T)

Exercise 3.17 — f is a section of g. f ∘ g ⊑ I_{T^∞}.

theorem Domain.Neighborhood.Exercise317.f_injective : Function.Injective f.toElementMap

f is one-one. Since g ∘ f = I_B, the elementwise map of f is injective.