Exercise 6.17 (Scott 1981, PRG-19, §6) — the algebras for which C is initial

EXERCISE 6.17. What are the algebras for which C is initial? If A of 6.2 is a generalization of B, what is the corresponding generalization of C? Prove that it exists and explain what are the algebras involved.

C (Example 4.4: finite-or-infinite binary sequences) satisfies the domain equation C ≅ {{Λ}} + C + C (Example 6.2, Example62C.lean). So C is a solution of the domain equation for the functor

T(X) = 𝟙 + X + X (one terminator + two successor copies).

This module proves that C is the initial T-algebra: for every T-algebra (E, k) there is a unique homomorphism C → E. Concretely a T-algebra is a strict map `k : 𝟙 + E

• E → E`, which by the universal property of the separated sum is the same data as

• a distinguished element e ∈ |E| (the image of the terminator 𝟙), and
• two strict endomaps f₀, f₁ : E → E (the two successor branches);

so the algebras for which C is initial are the domains carrying a point and two strict unary operations, and the unique homomorphism C → E interprets a finite-or-infinite binary sequence b₀b₁b₂… as f_{b₀}(f_{b₁}(… e …)).

Why a bespoke category of ∅-free domains

Scott's separated sum 𝒟₀ + 𝒟₁ (Exercise 3.18) is a neighbourhood system only under the standing assumption ∅ ∉ 𝒟 (an empty neighbourhood of one summand would become a spurious consistency witness for the other tag, breaking inter_mem). Consequently the functor T(X) = 𝟙 + X + X does not extend to a total endofunctor of the all-systems category DomainObj, and the existence Theorem 6.14 (stated over DomainObj) cannot be instantiated directly.

Following Scott — who restricts to the category of ∅-free systems and strict maps in Exercise 6.19 — we instantiate the abstract categorical vocabulary (Definitions 6.3–6.5) on the bespoke object type StrictDomainObj of neighbourhood systems with no empty neighbourhood, with strict approximable maps as morphisms. The functor T then reuses the existing sum3 (Example 6.2, the genuine three-way separated sum) and a three-way sum map, and initiality of C is proved directly (we construct the homomorphism and prove its uniqueness by the finite-approximant argument), rather than routing through the colimit construction of Theorem 6.14.

Everything is choice-free where it is data; the homomorphism/uniqueness layer reuses the project's established machinery.

The category of ∅-free domains and strict maps

structure Domain.Neighborhood.StrictDomainObj : Type (w + 1)

An object of Scott's category (Exercise 6.19): a token type, a neighbourhood system on it, and the standing assumption ∅ ∉ 𝒟 (every neighbourhood is non-empty).

• carrier : Type w

  The token type.

• sys : NeighborhoodSystem self.carrier

  The neighbourhood system.

• nonempty (X : Set self.carrier) : self.sys.mem X → X.Nonempty

  Scott's standing assumption ∅ ∉ 𝒟.

@[implicit_reducible]

instance Domain.Neighborhood.instCategoryStrictDomainObj : Category StrictDomainObj

The category of ∅-free domains and strict maps. Morphisms are strict approximable maps (StrictMap, Exercise 5.10); identities and associative composition come from Theorem 2.5, and strictness is preserved by isStrict_idMap / isStrict_comp.

Equations

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

@[simp]

theorem Domain.Neighborhood.StrictDomainObj.id_val (D : StrictDomainObj) : ↑(Category.id D) = ApproximableMap.idMap D.sys

@[simp]

theorem Domain.Neighborhood.StrictDomainObj.comp_val {D E F : StrictDomainObj} (g : Category.Hom E F) (f : Category.Hom D E) : ↑(g ⊚ f) = (↑g).comp ↑f

The functor T(X) = 𝟙 + X + X on objects

theorem Domain.Neighborhood.sum3_nonempty {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {h₂ : ∀ (Z : Set γ), V₂.mem Z → Z.Nonempty} (W : Set (Option (α ⊕ β ⊕ γ))) : (sum3 V₀ V₁ V₂ h₀ h₁ h₂).mem W → W.Nonempty

Every neighbourhood of the three-way separated sum sum3 is non-empty (so sum3 is again an object of the ∅-free category).

def Domain.Neighborhood.tcObj (D : StrictDomainObj) : StrictDomainObj

The functor T(X) = 𝟙 + X + X on objects. Over D, the system is the genuine three-way separated sum 𝟙 + D + D (Example 6.2's sum3, with 𝟙 = unitSys), again ∅-free by sum3_nonempty.

Equations

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

@[simp]

theorem Domain.Neighborhood.tcObj_sys (D : StrictDomainObj) : (tcObj D).sys = sum3 unitSys D.sys D.sys Example62C.unitSys_nonempty ⋯ ⋯

Membership-shape lemmas for sum3 (no nesting through the wrong tag)

theorem Domain.Neighborhood.mem_subset_j0_inv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {h₂ : ∀ (Z : Set γ), V₂.mem Z → Z.Nonempty} {W : Set (Option (α ⊕ β ⊕ γ))} {X : Set α} (hW : (sum3 V₀ V₁ V₂ h₀ h₁ h₂).mem W) (hsub : W ⊆ j0 X) : ∃ (X₂ : Set α), V₀.mem X₂ ∧ W = j0 X₂

A sum3-neighbourhood contained in a 0-copy 0X is itself a 0-copy.

theorem Domain.Neighborhood.mem_subset_j1_inv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {h₂ : ∀ (Z : Set γ), V₂.mem Z → Z.Nonempty} {W : Set (Option (α ⊕ β ⊕ γ))} {Y : Set β} (hW : (sum3 V₀ V₁ V₂ h₀ h₁ h₂).mem W) (hsub : W ⊆ j1 Y) : ∃ (Y₂ : Set β), V₁.mem Y₂ ∧ W = j1 Y₂

A sum3-neighbourhood contained in a 1-copy 1Y is itself a 1-copy.

theorem Domain.Neighborhood.mem_subset_j2_inv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {h₂ : ∀ (Z : Set γ), V₂.mem Z → Z.Nonempty} {W : Set (Option (α ⊕ β ⊕ γ))} {Z : Set γ} (hW : (sum3 V₀ V₁ V₂ h₀ h₁ h₂).mem W) (hsub : W ⊆ j2 Z) : ∃ (Z₂ : Set γ), V₂.mem Z₂ ∧ W = j2 Z₂

A sum3-neighbourhood contained in a 2-copy 2Z is itself a 2-copy.

The three-way sum map f₀ + f₁ + f₂

def Domain.Neighborhood.sumMap3 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} {β' : Type u_5} {γ' : Type u_6} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {V₀' : NeighborhoodSystem α'} {V₁' : NeighborhoodSystem β'} {V₂' : NeighborhoodSystem γ'} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {h₂ : ∀ (Z : Set γ), V₂.mem Z → Z.Nonempty} {h₀' : ∀ (X : Set α'), V₀'.mem X → X.Nonempty} {h₁' : ∀ (Y : Set β'), V₁'.mem Y → Y.Nonempty} {h₂' : ∀ (Z : Set γ'), V₂'.mem Z → Z.Nonempty} (f₀ : ApproximableMap V₀ V₀') (f₁ : ApproximableMap V₁ V₁') (f₂ : ApproximableMap V₂ V₂') : ApproximableMap (sum3 V₀ V₁ V₂ h₀ h₁ h₂) (sum3 V₀' V₁' V₂' h₀' h₁' h₂')

The three-way sum map f₀ + f₁ + f₂ : 𝒟₀+𝒟₁+𝒟₂ → 𝒟₀'+𝒟₁'+𝒟₂'. Routes each tagged copy iX through fᵢ (to iYᵢ'), and sends everything to the codomain master. (The three-way analogue of Exercise 3.19's sumMap.)

Equations

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

theorem Domain.Neighborhood.isStrict_sumMap3 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} {β' : Type u_5} {γ' : Type u_6} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {V₀' : NeighborhoodSystem α'} {V₁' : NeighborhoodSystem β'} {V₂' : NeighborhoodSystem γ'} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {h₂ : ∀ (Z : Set γ), V₂.mem Z → Z.Nonempty} {h₀' : ∀ (X : Set α'), V₀'.mem X → X.Nonempty} {h₁' : ∀ (Y : Set β'), V₁'.mem Y → Y.Nonempty} {h₂' : ∀ (Z : Set γ'), V₂'.mem Z → Z.Nonempty} (f₀ : ApproximableMap V₀ V₀') (f₁ : ApproximableMap V₁ V₁') (f₂ : ApproximableMap V₂ V₂') : Exercise510.IsStrict (sumMap3 f₀ f₁ f₂)

The three-way sum map is always strict: (f₀+f₁+f₂)(⊥) = ⊥. (The master only relates to the master, since master3 is not any tagged copy.)

theorem Domain.Neighborhood.sumMap3_id {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {h₂ : ∀ (Z : Set γ), V₂.mem Z → Z.Nonempty} : sumMap3 (ApproximableMap.idMap V₀) (ApproximableMap.idMap V₁) (ApproximableMap.idMap V₂) = ApproximableMap.idMap (sum3 V₀ V₁ V₂ h₀ h₁ h₂)

Functoriality (identities): I + I + I = I.

theorem Domain.Neighborhood.sumMap3_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} {β' : Type u_5} {γ' : Type u_6} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {V₀' : NeighborhoodSystem α'} {V₁' : NeighborhoodSystem β'} {V₂' : NeighborhoodSystem γ'} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {h₂ : ∀ (Z : Set γ), V₂.mem Z → Z.Nonempty} {h₀' : ∀ (X : Set α'), V₀'.mem X → X.Nonempty} {h₁' : ∀ (Y : Set β'), V₁'.mem Y → Y.Nonempty} {h₂' : ∀ (Z : Set γ'), V₂'.mem Z → Z.Nonempty} {α'' : Type u_7} {β'' : Type u_8} {γ'' : Type u_9} {V₀'' : NeighborhoodSystem α''} {V₁'' : NeighborhoodSystem β''} {V₂'' : NeighborhoodSystem γ''} {h₀'' : ∀ (X : Set α''), V₀''.mem X → X.Nonempty} {h₁'' : ∀ (Y : Set β''), V₁''.mem Y → Y.Nonempty} {h₂'' : ∀ (Z : Set γ''), V₂''.mem Z → Z.Nonempty} (g₀ : ApproximableMap V₀' V₀'') (g₁ : ApproximableMap V₁' V₁'') (g₂ : ApproximableMap V₂' V₂'') (f₀ : ApproximableMap V₀ V₀') (f₁ : ApproximableMap V₁ V₁') (f₂ : ApproximableMap V₂ V₂') : sumMap3 (g₀.comp f₀) (g₁.comp f₁) (g₂.comp f₂) = (sumMap3 g₀ g₁ g₂).comp (sumMap3 f₀ f₁ f₂)

Functoriality (composition): (g₀∘f₀) + (g₁∘f₁) + (g₂∘f₂) = (g₀+g₁+g₂) ∘ (f₀+f₁+f₂).

The canonical injections D_i ↪ D₀+D₁+D₂

def Domain.Neighborhood.sinj0 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {h₂ : ∀ (Z : Set γ), V₂.mem Z → Z.Nonempty} (x₀ : V₀.Element) : (sum3 V₀ V₁ V₂ h₀ h₁ h₂).Element

The 0-injection D₀ ↪ D₀+D₁+D₂: send x₀∈|D₀| to the sum element whose only proper neighbourhoods are the 0-copies 0X with X∈x₀.

Equations

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

def Domain.Neighborhood.sinj1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {h₂ : ∀ (Z : Set γ), V₂.mem Z → Z.Nonempty} (x₁ : V₁.Element) : (sum3 V₀ V₁ V₂ h₀ h₁ h₂).Element

The 1-injection D₁ ↪ D₀+D₁+D₂.

Equations

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

def Domain.Neighborhood.sinj2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {h₂ : ∀ (Z : Set γ), V₂.mem Z → Z.Nonempty} (x₂ : V₂.Element) : (sum3 V₀ V₁ V₂ h₀ h₁ h₂).Element

The 2-injection D₂ ↪ D₀+D₁+D₂.

Equations

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

@[simp]

theorem Domain.Neighborhood.sinj0_mem_j0 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {h₂ : ∀ (Z : Set γ), V₂.mem Z → Z.Nonempty} {x₀ : V₀.Element} {X : Set α} (hX : V₀.mem X) : (sinj0 x₀).mem (j0 X) ↔ x₀.mem X

@[simp]

theorem Domain.Neighborhood.sinj1_mem_j1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {h₂ : ∀ (Z : Set γ), V₂.mem Z → Z.Nonempty} {x₁ : V₁.Element} {Y : Set β} (hY : V₁.mem Y) : (sinj1 x₁).mem (j1 Y) ↔ x₁.mem Y

@[simp]

theorem Domain.Neighborhood.sinj2_mem_j2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {h₂ : ∀ (Z : Set γ), V₂.mem Z → Z.Nonempty} {x₂ : V₂.Element} {Z : Set γ} (hZ : V₂.mem Z) : (sinj2 x₂).mem (j2 Z) ↔ x₂.mem Z

Monotonicity of the injections, and the action of f₀+f₁+f₂ on them

theorem Domain.Neighborhood.sinj1_mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {h₂ : ∀ (Z : Set γ), V₂.mem Z → Z.Nonempty} {x x' : V₁.Element} (hx : x ≤ x') : sinj1 x ≤ sinj1 x'

theorem Domain.Neighborhood.sinj2_mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {h₂ : ∀ (Z : Set γ), V₂.mem Z → Z.Nonempty} {x x' : V₂.Element} (hx : x ≤ x') : sinj2 x ≤ sinj2 x'

theorem Domain.Neighborhood.sumMap3_sinj0 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} {β' : Type u_5} {γ' : Type u_6} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {V₀' : NeighborhoodSystem α'} {V₁' : NeighborhoodSystem β'} {V₂' : NeighborhoodSystem γ'} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {h₂ : ∀ (Z : Set γ), V₂.mem Z → Z.Nonempty} {h₀' : ∀ (X : Set α'), V₀'.mem X → X.Nonempty} {h₁' : ∀ (Y : Set β'), V₁'.mem Y → Y.Nonempty} {h₂' : ∀ (Z : Set γ'), V₂'.mem Z → Z.Nonempty} (f₀ : ApproximableMap V₀ V₀') (f₁ : ApproximableMap V₁ V₁') (f₂ : ApproximableMap V₂ V₂') (x₀ : V₀.Element) : (sumMap3 f₀ f₁ f₂).toElementMap (sinj0 x₀) = sinj0 (f₀.toElementMap x₀)

(f₀+f₁+f₂)(inj₀ x) = inj₀(f₀ x).

theorem Domain.Neighborhood.sumMap3_sinj1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} {β' : Type u_5} {γ' : Type u_6} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {V₀' : NeighborhoodSystem α'} {V₁' : NeighborhoodSystem β'} {V₂' : NeighborhoodSystem γ'} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {h₂ : ∀ (Z : Set γ), V₂.mem Z → Z.Nonempty} {h₀' : ∀ (X : Set α'), V₀'.mem X → X.Nonempty} {h₁' : ∀ (Y : Set β'), V₁'.mem Y → Y.Nonempty} {h₂' : ∀ (Z : Set γ'), V₂'.mem Z → Z.Nonempty} (f₀ : ApproximableMap V₀ V₀') (f₁ : ApproximableMap V₁ V₁') (f₂ : ApproximableMap V₂ V₂') (x₁ : V₁.Element) : (sumMap3 f₀ f₁ f₂).toElementMap (sinj1 x₁) = sinj1 (f₁.toElementMap x₁)

(f₀+f₁+f₂)(inj₁ x) = inj₁(f₁ x).

theorem Domain.Neighborhood.sumMap3_sinj2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} {β' : Type u_5} {γ' : Type u_6} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {V₀' : NeighborhoodSystem α'} {V₁' : NeighborhoodSystem β'} {V₂' : NeighborhoodSystem γ'} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {h₂ : ∀ (Z : Set γ), V₂.mem Z → Z.Nonempty} {h₀' : ∀ (X : Set α'), V₀'.mem X → X.Nonempty} {h₁' : ∀ (Y : Set β'), V₁'.mem Y → Y.Nonempty} {h₂' : ∀ (Z : Set γ'), V₂'.mem Z → Z.Nonempty} (f₀ : ApproximableMap V₀ V₀') (f₁ : ApproximableMap V₁ V₁') (f₂ : ApproximableMap V₂ V₂') (x₂ : V₂.Element) : (sumMap3 f₀ f₁ f₂).toElementMap (sinj2 x₂) = sinj2 (f₂.toElementMap x₂)

(f₀+f₁+f₂)(inj₂ x) = inj₂(f₂ x).

The functor T(X) = 𝟙 + X + X

def Domain.Neighborhood.tcMapHom {D E : StrictDomainObj} (f : Category.Hom D E) : Category.Hom (tcObj D) (tcObj E)

The morphism action of T: T(f) = I_𝟙 + f + f (identity on the terminator, f on each successor copy). Always strict (isStrict_sumMap3).

Equations

• Domain.Neighborhood.tcMapHom f = ⟨Domain.Neighborhood.sumMap3 (Domain.Neighborhood.ApproximableMap.idMap Domain.Neighborhood.unitSys) ↑f ↑f, ⋯⟩

def Domain.Neighborhood.Tc : Endofunctor StrictDomainObj

Exercise 6.17 — the functor T(X) = 𝟙 + X + X on the category of ∅-free domains and strict maps. On objects, T(D) = 𝟙 + D + D (Example 6.2's three-way sum); on maps, T(f) = I_𝟙 + f + f.

Equations

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

@[simp]

theorem Domain.Neighborhood.Tc_obj (D : StrictDomainObj) : Tc.obj D = tcObj D

@[simp]

theorem Domain.Neighborhood.Tc_map_val {D E : StrictDomainObj} (f : Category.Hom D E) : ↑(Tc.map f) = sumMap3 (ApproximableMap.idMap unitSys) ↑f ↑f

C as a T-algebra

theorem Domain.Neighborhood.isStrict_ofIso {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (e : V₀.Element ≃o V₁.Element) : Exercise510.IsStrict (ApproximableMap.ofIso e)

The map of an order-isomorphism is strict (an iso of domains preserves ⊥).

def Domain.Neighborhood.Cobj : StrictDomainObj

C (Example 4.4: finite-or-infinite binary sequences) as an object of the ∅-free category.

Equations

• Domain.Neighborhood.Cobj = { carrier := Domain.Neighborhood.ExampleB.Str, sys := Domain.Neighborhood.Example44.C, nonempty := Domain.Neighborhood.Example62C.C_nonempty }

def Domain.Neighborhood.cStr : Category.Hom (Tc.obj Cobj) Cobj

The T-algebra structure on C. (tcObj Cobj).sys = 𝟙 + C + C (definitionally Example 6.2's CC), and the structure map i : 𝟙 + C + C → C is the inverse of the domain-equation isomorphism ccEquiv (Example 6.2), realised as an approximable map by ofIso; it is strict by isStrict_ofIso. Concretely i sends the terminator to Λ̂ and each b-copy of x to b·x.

Equations

• Domain.Neighborhood.cStr = ⟨Domain.Neighborhood.ApproximableMap.ofIso Domain.Neighborhood.Example62C.ccEquiv.symm, Domain.Neighborhood.cStr._proof_1⟩

def Domain.Neighborhood.Calg : TAlgebra Tc

C is a T-algebra, (C, i) with T(X) = 𝟙 + X + X.

Equations

• Domain.Neighborhood.Calg = { carrier := Domain.Neighborhood.Cobj, str := Domain.Neighborhood.cStr }

Initiality of (C, i): the unique homomorphism into any T-algebra

We first relate the domain-equation isomorphism toCC = ccEquiv to the separated-sum injections: the terminator Λ̂ lands on the 𝟙-copy, and prepending a bit (consMap b) lands on the b-th C-copy.

@[simp]

theorem Domain.Neighborhood.Example62C.ccEquiv_apply (x : Example44.C.Element) : ccEquiv x = toCC x

theorem Domain.Neighborhood.Example62C.consMap_mem_embBit {b : Bool} {z : Example44.C.Element} {X : Set ExampleB.Str} (hX : Example44.C.mem X) : ((Example44.consMap b).toElementMap z).mem (Example62.embBit b X) ↔ z.mem X

(b·z).mem (bX) ↔ z.mem X: the b-successor's filter restricted to the b-copy is z.

theorem Domain.Neighborhood.Example62C.consMap_not_mem_embBit_ne {b c : Bool} (hbc : b ≠ c) {z : Example44.C.Element} {X : Set ExampleB.Str} : ¬((Example44.consMap b).toElementMap z).mem (Example62.embBit c X)

(b·z) never meets the (¬b)-copy: 0z avoids the 1-copies and vice versa (used to discharge the cross-tag cases in toCC_consMap).

theorem Domain.Neighborhood.Example62C.consMap_not_mem_nil {b : Bool} {z : Example44.C.Element} : ¬((Example44.consMap b).toElementMap z).mem {[]}

(b·z) avoids the terminator {Λ} (since bσ ≠ Λ).

theorem Domain.Neighborhood.Example62C.toCC_consMap (b : Bool) (z : Example44.C.Element) : toCC ((Example44.consMap b).toElementMap z) = bif b then sinj2 z else sinj1 z

toCC ∘ (0·) = inj₁ and toCC ∘ (1·) = inj₂. Prepending the bit b to z is, across the isomorphism C ≅ 𝟙+C+C, the injection of z into the b-th C-summand.

theorem Domain.Neighborhood.Example62C.toCC_strElem_nil : toCC (Example44.strElem []) = sinj0 unitSys.bot

toCC Λ̂ = inj₀. The finished empty sequence is the terminator (the 𝟙-summand).

The homomorphism desc : C → E for a T-algebra B = (E, k)

def Domain.Neighborhood.descE (B : TAlgebra Tc) : B.carrier.sys.Element

The distinguished point e = k(Λ): the image under k of the terminator (𝟙-injection).

Equations

• Domain.Neighborhood.descE B = (↑B.str).toElementMap (Domain.Neighborhood.sinj0 Domain.Neighborhood.unitSys.bot)

def Domain.Neighborhood.descF (B : TAlgebra Tc) (b : Bool) (y : B.carrier.sys.Element) : B.carrier.sys.Element

The b-th successor operation f_b = k ∘ inj_b: f₀ via the 0-copy (inj₁), f₁ via the 1-copy (inj₂).

Equations

• Domain.Neighborhood.descF B b y = (↑B.str).toElementMap (bif b then Domain.Neighborhood.sinj2 y else Domain.Neighborhood.sinj1 y)

def Domain.Neighborhood.descVal (B : TAlgebra Tc) (z : B.carrier.sys.Element) : ExampleB.Str → B.carrier.sys.Element

The recursion φ(Λ)=z, φ(b·σ)=f_b(φ(σ)) on a finite string, with base value z.

Equations

• Domain.Neighborhood.descVal B z [] = z
• Domain.Neighborhood.descVal B z (b :: σ) = Domain.Neighborhood.descF B b (Domain.Neighborhood.descVal B z σ)

theorem Domain.Neighborhood.descF_mono (B : TAlgebra Tc) (b : Bool) {y y' : B.carrier.sys.Element} (h : y ≤ y') : descF B b y ≤ descF B b y'

theorem Domain.Neighborhood.descVal_mono_z (B : TAlgebra Tc) {z z' : B.carrier.sys.Element} (h : z ≤ z') (σ : ExampleB.Str) : descVal B z σ ≤ descVal B z' σ

theorem Domain.Neighborhood.descVal_append (B : TAlgebra Tc) (z : B.carrier.sys.Element) (σ ρ : ExampleB.Str) : descVal B z (σ ++ ρ) = descVal B (descVal B z ρ) σ

theorem Domain.Neighborhood.descMap_hcone (B : TAlgebra Tc) {σ τ : ExampleB.Str} (h : σ <+: τ) : descVal B B.carrier.sys.bot σ ≤ descVal B B.carrier.sys.bot τ

theorem Domain.Neighborhood.descMap_hsing (B : TAlgebra Tc) {σ τ : ExampleB.Str} (h : σ <+: τ) : descVal B B.carrier.sys.bot σ ≤ descVal B (descE B) τ

def Domain.Neighborhood.descMap (B : TAlgebra Tc) : ApproximableMap Example44.C B.carrier.sys

The homomorphism C → E. Built by liftC from the head-recursion: φ(σ⊥) = f_{σ}(⊥) and φ(σ) = f_{σ}(e), interpreting b₀b₁… ↦ f_{b₀}(f_{b₁}(…)).

Equations

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

@[simp]

theorem Domain.Neighborhood.descMap_strBot (B : TAlgebra Tc) (σ : ExampleB.Str) : (descMap B).toElementMap (Example44.strBot σ) = descVal B B.carrier.sys.bot σ

@[simp]

theorem Domain.Neighborhood.descMap_strElem (B : TAlgebra Tc) (σ : ExampleB.Str) : (descMap B).toElementMap (Example44.strElem σ) = descVal B (descE B) σ

theorem Domain.Neighborhood.C_bot_eq_strBot_nil : Example44.C.bot = Example44.strBot []

theorem Domain.Neighborhood.descMap_strict (B : TAlgebra Tc) : Exercise510.IsStrict (descMap B)

def Domain.Neighborhood.descStrict (B : TAlgebra Tc) : Category.Hom Cobj B.carrier

The bundled strict homomorphism C → E.

Equations

• Domain.Neighborhood.descStrict B = ⟨Domain.Neighborhood.descMap B, ⋯⟩

The homomorphism square and uniqueness

theorem Domain.Neighborhood.genKey (B : TAlgebra Tc) (g : ApproximableMap Example44.C B.carrier.sys) (b : Bool) (w : Example44.C.Element) : (↑B.str).toElementMap ((sumMap3 (ApproximableMap.idMap unitSys) g g).toElementMap (Example62C.toCC ((Example44.consMap b).toElementMap w))) = descF B b (g.toElementMap w)

The composite inj₀∘(...) of T(g) applied to a successor reduces to the operation f_b. The single computational step behind both existence and uniqueness, for an arbitrary g.

theorem Domain.Neighborhood.genKey0 (B : TAlgebra Tc) (g : ApproximableMap Example44.C B.carrier.sys) : (↑B.str).toElementMap ((sumMap3 (ApproximableMap.idMap unitSys) g g).toElementMap (Example62C.toCC (Example44.strElem []))) = descE B

T(g) on the terminator is the terminator; precomposed with k it is e.

theorem Domain.Neighborhood.genKeyBot (B : TAlgebra Tc) (g : ApproximableMap Example44.C B.carrier.sys) : (↑B.str).toElementMap ((sumMap3 (ApproximableMap.idMap unitSys) g g).toElementMap (Example62C.toCC (Example44.strBot []))) = B.carrier.sys.bot

T(g) on ⊥ is ⊥; precomposed with k it is ⊥ (both maps are strict).

theorem Domain.Neighborhood.ccEquiv_symm_comp : (ApproximableMap.ofIso Example62C.ccEquiv.symm).comp (ApproximableMap.ofIso Example62C.ccEquiv) = ApproximableMap.idMap Example44.C

theorem Domain.Neighborhood.ccEquiv_comp_symm : (ApproximableMap.ofIso Example62C.ccEquiv).comp (ApproximableMap.ofIso Example62C.ccEquiv.symm) = ApproximableMap.idMap (sum3 unitSys Example44.C Example44.C Example62C.unitSys_nonempty Example62C.C_nonempty Example62C.C_nonempty)

theorem Domain.Neighborhood.rec_determines (B : TAlgebra Tc) (g : ApproximableMap Example44.C B.carrier.sys) (hg : g = ((↑B.str).comp (sumMap3 (ApproximableMap.idMap unitSys) g g)).comp (ApproximableMap.ofIso Example62C.ccEquiv)) : g = descMap B

Any map satisfying the homomorphism recursion equals descMap. This is both the existence witness (descMap satisfies it) and the uniqueness driver.

theorem Domain.Neighborhood.descMap_satisfiesRec (B : TAlgebra Tc) : descMap B = ((↑B.str).comp (sumMap3 (ApproximableMap.idMap unitSys) (descMap B) (descMap B))).comp (ApproximableMap.ofIso Example62C.ccEquiv)

C's algebra map satisfies the recursion.

theorem Domain.Neighborhood.descComm (B : TAlgebra Tc) : (descMap B).comp (ApproximableMap.ofIso Example62C.ccEquiv.symm) = (↑B.str).comp (sumMap3 (ApproximableMap.idMap unitSys) (descMap B) (descMap B))

The homomorphism square, read off at the level of underlying approximable maps: desc ∘ i = k ∘ T(desc).

def Domain.Neighborhood.descAlgHom (B : TAlgebra Tc) : AlgHom Calg B

The descent homomorphism (C, i) → (E, k) as a T-algebra homomorphism.

Equations

• Domain.Neighborhood.descAlgHom B = { hom := Domain.Neighborhood.descStrict B, comm := ⋯ }

theorem Domain.Neighborhood.descAlgHom_uniq (B : TAlgebra Tc) (h' : AlgHom Calg B) : h' = descAlgHom B

Uniqueness. Any T-algebra homomorphism out of (C, i) equals descAlgHom.

def Domain.Neighborhood.CisInitial : IsInitial Calg

Exercise 6.17 (existence half) — (C, i) is an initial T-algebra for T(X) = 𝟙 + X + X. The descent map φ : C → E is the closed-form head-recursion φ(Λ) = e, φ(b·x) = f_b(φ x) (f_b = k ∘ inj_b), built choice-free via liftC; it is the unique T-algebra homomorphism, so C is determined (up to iso, Proposition 6.6) as the initial algebra of X ↦ 𝟙 + X + X.

Equations

• Domain.Neighborhood.CisInitial = { desc := Domain.Neighborhood.descAlgHom, uniq := ⋯ }