Exercise 6.17 part 2 (Scott 1981, PRG-19) — the generalization Cₐ ≅ 𝟙 + Σₐ Cₐ

Example 6.2 / Exercise 6.17 ask for the generalization of C corresponding to Scott's A ≅ Aⁿ + Aⁿ: replace the two-letter alphabet {0,1} of C (C ≅ 𝟙 + C + C) by an arbitrary alphabet A. The domain Cₐ of finite or infinite A-sequences then satisfies the domain equation Cₐ ≅ 𝟙 + Σ_{a:A} Cₐ (the A-indexed separated sum of copies of Cₐ). Instantiating A := Fin n gives Cₙ ≅ 𝟙 + n·Cₙ; A := Bool recovers Example 6.2's C.

This module mirrors, generically over an alphabet A with decidable equality, the binary development of Example44 (the domain), Example62/Example62C (the sum and the isomorphism) and Exercise617 (initiality).

Stage 1 (this section): the generic domain Cₐ

Strn A = List A; cones coneN σ = σA*; the neighbourhood system Cn = {σA*} ∪ {{σ}}; the total elements strElemN σ and partial elements strBotN σ; and the successors consMapN a : Cₐ → Cₐ prepending the letter a. Everything is the alphabet-generic copy of Example44, and the data (Cn, consMapN) stays choice-free.

@[reducible, inline]

abbrev Domain.Neighborhood.Exercise617Gen.Strn (A : Type) : Type

The token type A* of finite A-strings.

Equations

• Domain.Neighborhood.Exercise617Gen.Strn A = List A

def Domain.Neighborhood.Exercise617Gen.coneN {A : Type} (σ : Strn A) : Set (Strn A)

The cone σA*: all extensions of σ.

Equations

• Domain.Neighborhood.Exercise617Gen.coneN σ = {w : Domain.Neighborhood.Exercise617Gen.Strn A | σ <+: w}

@[simp]

theorem Domain.Neighborhood.Exercise617Gen.mem_coneN {A : Type} {σ w : Strn A} : w ∈ coneN σ ↔ σ <+: w

theorem Domain.Neighborhood.Exercise617Gen.coneN_nil {A : Type} : coneN [] = Set.univ

theorem Domain.Neighborhood.Exercise617Gen.coneN_subset_coneN {A : Type} {σ τ : Strn A} : coneN σ ⊆ coneN τ ↔ τ <+: σ

theorem Domain.Neighborhood.Exercise617Gen.coneN_injective {A : Type} {σ τ : Strn A} (h : coneN σ = coneN τ) : σ = τ

theorem Domain.Neighborhood.Exercise617Gen.coneN_trichotomy {A : Type} (σ τ : Strn A) : coneN σ ⊆ coneN τ ∨ coneN τ ⊆ coneN σ ∨ coneN σ ∩ coneN τ = ∅

def Domain.Neighborhood.Exercise617Gen.memCn {A : Type} (X : Set (Strn A)) : Prop

Membership in Cₐ: a cone σA* or a singleton {σ}.

Equations

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

theorem Domain.Neighborhood.Exercise617Gen.memCn_coneN {A : Type} (σ : Strn A) : memCn (coneN σ)

theorem Domain.Neighborhood.Exercise617Gen.memCn_singleton {A : Type} (σ : Strn A) : memCn {σ}

theorem Domain.Neighborhood.Exercise617Gen.singleton_subset_coneN {A : Type} {σ τ : Strn A} : {τ} ⊆ coneN σ ↔ σ <+: τ

theorem Domain.Neighborhood.Exercise617Gen.singleton_coneN_nd {A : Type} (σ τ : Strn A) : {τ} ⊆ coneN σ ∨ coneN σ ⊆ {τ} ∨ {τ} ∩ coneN σ = ∅

theorem Domain.Neighborhood.Exercise617Gen.nestedOrDisjointN {A : Type} : NestedOrDisjoint memCn

def Domain.Neighborhood.Exercise617Gen.Cn (A : Type) : NeighborhoodSystem (Strn A)

The generic domain Cₐ of finite-or-infinite A-sequences.

Equations

• Domain.Neighborhood.Exercise617Gen.Cn A = Domain.Neighborhood.NeighborhoodSystem.ofNestedOrDisjoint Domain.Neighborhood.Exercise617Gen.memCn Set.univ ⋯ ⋯ ⋯

@[simp]

theorem Domain.Neighborhood.Exercise617Gen.Cn_mem {A : Type} {X : Set (Strn A)} : (Cn A).mem X ↔ memCn X

@[simp]

theorem Domain.Neighborhood.Exercise617Gen.Cn_master {A : Type} : (Cn A).master = Set.univ

theorem Domain.Neighborhood.Exercise617Gen.Cn_nonempty {A : Type} (X : Set (Strn A)) : (Cn A).mem X → X.Nonempty

Cₐ is ∅-free: every neighbourhood is non-empty (cones and singletons are inhabited).

def Domain.Neighborhood.Exercise617Gen.strBotN {A : Type} (σ : Strn A) : (Cn A).Element

The partial element σ⊥ = ↑σA*.

Equations

• Domain.Neighborhood.Exercise617Gen.strBotN σ = (Domain.Neighborhood.Exercise617Gen.Cn A).principal ⋯

def Domain.Neighborhood.Exercise617Gen.strElemN {A : Type} (σ : Strn A) : (Cn A).Element

The total element σ = ↑{σ}.

Equations

• Domain.Neighborhood.Exercise617Gen.strElemN σ = (Domain.Neighborhood.Exercise617Gen.Cn A).principal ⋯

Prepending a letter: the successors x ↦ a·x.

def Domain.Neighborhood.Exercise617Gen.prependN {A : Type} (σ : Strn A) (X : Set (Strn A)) : Set (Strn A)

σX = {στ ∣ τ ∈ X}.

Equations

• Domain.Neighborhood.Exercise617Gen.prependN σ X = {w : Domain.Neighborhood.Exercise617Gen.Strn A | ∃ τ ∈ X, w = σ ++ τ}

@[simp]

theorem Domain.Neighborhood.Exercise617Gen.mem_prependN {A : Type} {σ : Strn A} {X : Set (Strn A)} {w : Strn A} : w ∈ prependN σ X ↔ ∃ τ ∈ X, w = σ ++ τ

theorem Domain.Neighborhood.Exercise617Gen.prependN_coneN {A : Type} (σ ρ : Strn A) : prependN σ (coneN ρ) = coneN (σ ++ ρ)

theorem Domain.Neighborhood.Exercise617Gen.prependN_singleton {A : Type} (σ τ : Strn A) : prependN σ {τ} = {σ ++ τ}

theorem Domain.Neighborhood.Exercise617Gen.prependN_mono {A : Type} (σ : Strn A) {X X' : Set (Strn A)} (h : X' ⊆ X) : prependN σ X' ⊆ prependN σ X

theorem Domain.Neighborhood.Exercise617Gen.memCn_prependN {A : Type} (σ : Strn A) {X : Set (Strn A)} (hX : memCn X) : memCn (prependN σ X)

def Domain.Neighborhood.Exercise617Gen.consMapN {A : Type} (a : A) : ApproximableMap (Cn A) (Cn A)

The successor x ↦ a·x prepending the letter a: X (a·x) Y ↔ aX ⊆ Y.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise617Gen.consMapN_rel {A : Type} {a : A} {X Y : Set (Strn A)} : (consMapN a).rel X Y ↔ memCn X ∧ memCn Y ∧ prependN [a] X ⊆ Y

theorem Domain.Neighborhood.Exercise617Gen.consMapN_strBot {A : Type} (a : A) (σ : Strn A) : (consMapN a).toElementMap (strBotN σ) = strBotN (a :: σ)

theorem Domain.Neighborhood.Exercise617Gen.consMapN_strElem {A : Type} (a : A) (σ : Strn A) : (consMapN a).toElementMap (strElemN σ) = strElemN (a :: σ)

Stage 2: the A-indexed separated sum Tsig(X) = 𝟙 + Σ_{a:A} X

The right-hand side of the generalized domain equation. Tokens are Option (Unit ⊕ (A × β)): a fresh basepoint Λ = none, the lone 𝟙-token tu = some (inl ()), and the A-indexed family of tagged copies tc a t = some (inr (a, t)). This is the alphabet-generic analogue of Example62C's three-way sum3 unitSys C C (= 𝟙 + C + C), the index Bool being replaced by A.

@[reducible, inline]

abbrev Domain.Neighborhood.Exercise617Gen.SigTok (A : Type) (β : Type v) : Type v

Tokens of the indexed sum 𝟙 + Σ_a β.

Equations

• Domain.Neighborhood.Exercise617Gen.SigTok A β = Option (Unit ⊕ A × β)

def Domain.Neighborhood.Exercise617Gen.tu {A : Type} {β : Type v} : SigTok A β

The lone 𝟙-token.

Equations

• Domain.Neighborhood.Exercise617Gen.tu = some (Sum.inl ())

def Domain.Neighborhood.Exercise617Gen.tc {A : Type} {β : Type v} (a : A) (t : β) : SigTok A β

The token t in the a-indexed copy.

Equations

• Domain.Neighborhood.Exercise617Gen.tc a t = some (Sum.inr (a, t))

def Domain.Neighborhood.Exercise617Gen.jU {A : Type} {β : Type v} : Set (SigTok A β)

The 𝟙-copy neighbourhood (the image of univ : Set Unit).

Equations

• Domain.Neighborhood.Exercise617Gen.jU = {Domain.Neighborhood.Exercise617Gen.tu}

def Domain.Neighborhood.Exercise617Gen.jc {A : Type} {β : Type v} (a : A) (X : Set β) : Set (SigTok A β)

The a-indexed tagged copy aX.

Equations

• Domain.Neighborhood.Exercise617Gen.jc a X = {w : Domain.Neighborhood.Exercise617Gen.SigTok A β | ∃ (t : β), w = Domain.Neighborhood.Exercise617Gen.tc a t ∧ t ∈ X}

theorem Domain.Neighborhood.Exercise617Gen.tc_injective {A : Type} {β : Type v} {a a' : A} {t t' : β} (h : tc a t = tc a' t') : a = a' ∧ t = t'

@[simp]

theorem Domain.Neighborhood.Exercise617Gen.tc_mem_jc {A : Type} {β : Type v} {a : A} {X : Set β} {t : β} : tc a t ∈ jc a X ↔ t ∈ X

@[simp]

theorem Domain.Neighborhood.Exercise617Gen.mem_jU {A : Type} {β : Type v} {w : SigTok A β} : w ∈ jU ↔ w = tu

theorem Domain.Neighborhood.Exercise617Gen.none_not_mem_jU {A : Type} {β : Type v} : none ∉ jU

@[simp]

theorem Domain.Neighborhood.Exercise617Gen.none_not_mem_jc {A : Type} {β : Type v} {a : A} {X : Set β} : none ∉ jc a X

@[simp]

theorem Domain.Neighborhood.Exercise617Gen.tu_not_mem_jc {A : Type} {β : Type v} {a : A} {X : Set β} : tu ∉ jc a X

theorem Domain.Neighborhood.Exercise617Gen.tc_not_mem_jU {A : Type} {β : Type v} {a : A} {t : β} : tc a t ∉ jU

theorem Domain.Neighborhood.Exercise617Gen.tc_mem_jc_ne {A : Type} {β : Type v} {a a' : A} (h : a ≠ a') {X : Set β} {t : β} : tc a t ∉ jc a' X

theorem Domain.Neighborhood.Exercise617Gen.jc_inter_jc_same {A : Type} {β : Type v} (a : A) (X X' : Set β) : jc a X ∩ jc a X' = jc a (X ∩ X')

theorem Domain.Neighborhood.Exercise617Gen.jc_inter_jc_ne {A : Type} {β : Type v} {a a' : A} (h : a ≠ a') (X X' : Set β) : jc a X ∩ jc a' X' = ∅

theorem Domain.Neighborhood.Exercise617Gen.jU_inter_jc {A : Type} {β : Type v} (a : A) (X : Set β) : jU ∩ jc a X = ∅

theorem Domain.Neighborhood.Exercise617Gen.jU_nonempty {A : Type} {β : Type v} : jU.Nonempty

theorem Domain.Neighborhood.Exercise617Gen.jc_nonempty {A : Type} {β : Type v} {a : A} {X : Set β} (hX : X.Nonempty) : (jc a X).Nonempty

theorem Domain.Neighborhood.Exercise617Gen.jc_subset_jc {A : Type} {β : Type v} {a : A} {X X' : Set β} : jc a X ⊆ jc a X' ↔ X ⊆ X'

theorem Domain.Neighborhood.Exercise617Gen.jc_injective {A : Type} {β : Type v} {a : A} {X X' : Set β} (h : jc a X = jc a X') : X = X'

theorem Domain.Neighborhood.Exercise617Gen.jc_eq_jc {A : Type} {β : Type v} {a a' : A} {X X' : Set β} (hXne : X.Nonempty) (heq : jc a X = jc a' X') : a = a' ∧ X = X'

Tagged copies determine both index and set: aX = a'X' (with X non-empty) forces a=a', X=X'.

def Domain.Neighborhood.Exercise617Gen.masterSig {A : Type} {β : Type v} (V : NeighborhoodSystem β) : Set (SigTok A β)

The master neighbourhood {Λ} ∪ {tu} ∪ ⋃_a aΔ.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise617Gen.none_mem_masterSig {A : Type} {β : Type v} {V : NeighborhoodSystem β} : none ∈ masterSig V

@[simp]

theorem Domain.Neighborhood.Exercise617Gen.tu_mem_masterSig {A : Type} {β : Type v} {V : NeighborhoodSystem β} : tu ∈ masterSig V

theorem Domain.Neighborhood.Exercise617Gen.jU_subset_masterSig {A : Type} {β : Type v} {V : NeighborhoodSystem β} : jU ⊆ masterSig V

theorem Domain.Neighborhood.Exercise617Gen.jc_subset_masterSig {A : Type} {β : Type v} {V : NeighborhoodSystem β} {a : A} {X : Set β} (hX : V.mem X) : jc a X ⊆ masterSig V

theorem Domain.Neighborhood.Exercise617Gen.masterSig_inter_jU {A : Type} {β : Type v} {V : NeighborhoodSystem β} : masterSig V ∩ jU = jU

theorem Domain.Neighborhood.Exercise617Gen.masterSig_inter_jc {A : Type} {β : Type v} {V : NeighborhoodSystem β} {a : A} {X : Set β} (hX : V.mem X) : masterSig V ∩ jc a X = jc a X

theorem Domain.Neighborhood.Exercise617Gen.eq_masterSig_of_subset {A : Type} {β : Type v} {V : NeighborhoodSystem β} {W : Set (SigTok A β)} (hsub : masterSig V ⊆ W) (hsub' : W ⊆ masterSig V) : W = masterSig V

def Domain.Neighborhood.Exercise617Gen.sumSig {β : Type v} (A : Type) [DecidableEq A] (V : NeighborhoodSystem β) (h : ∀ (X : Set β), V.mem X → X.Nonempty) : NeighborhoodSystem (SigTok A β)

The A-indexed separated sum 𝟙 + Σ_a V over {Λ} ∪ {tu} ∪ ⋃_a aΔ, under the standing assumption that no neighbourhood of V is empty. The alphabet-generic analogue of sum3 unitSys V V (Example 6.2).

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise617Gen.sumSig_master {A : Type} [DecidableEq A] {β : Type v} {V : NeighborhoodSystem β} {h : ∀ (X : Set β), V.mem X → X.Nonempty} : (sumSig A V h).master = masterSig V

theorem Domain.Neighborhood.Exercise617Gen.sumSig_nonempty {A : Type} [DecidableEq A] {β : Type v} {V : NeighborhoodSystem β} {h : ∀ (X : Set β), V.mem X → X.Nonempty} (W : Set (SigTok A β)) : (sumSig A V h).mem W → W.Nonempty

Shape lemmas: no nesting through the wrong tag.

theorem Domain.Neighborhood.Exercise617Gen.mem_subset_jc_inv {A : Type} [DecidableEq A] {β : Type v} {V : NeighborhoodSystem β} {h : ∀ (X : Set β), V.mem X → X.Nonempty} {W : Set (SigTok A β)} {a : A} {X : Set β} (hW : (sumSig A V h).mem W) (hsub : W ⊆ jc a X) : ∃ (X₂ : Set β), V.mem X₂ ∧ W = jc a X₂

A sumSig-neighbourhood contained in an a-copy aX is itself an a-copy.

theorem Domain.Neighborhood.Exercise617Gen.mem_subset_jU_inv {A : Type} [DecidableEq A] {β : Type v} {V : NeighborhoodSystem β} {h : ∀ (X : Set β), V.mem X → X.Nonempty} {W : Set (SigTok A β)} (hW : (sumSig A V h).mem W) (hsub : W ⊆ jU) : W = jU

A sumSig-neighbourhood contained in the 𝟙-copy jU is jU.

The canonical injections 𝟙 ↪ 𝟙+Σ_a V and V ↪ 𝟙+Σ_a V (the a-th

copy).

def Domain.Neighborhood.Exercise617Gen.sinjU {A : Type} [DecidableEq A] {β : Type v} {V : NeighborhoodSystem β} {h : ∀ (X : Set β), V.mem X → X.Nonempty} : (sumSig A V h).Element

The basepoint/𝟙-injection: the image of the unique point of 𝟙. Its proper neighbourhood is the 𝟙-copy jU.

Equations

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

def Domain.Neighborhood.Exercise617Gen.sinjC {A : Type} [DecidableEq A] {β : Type v} {V : NeighborhoodSystem β} {h : ∀ (X : Set β), V.mem X → X.Nonempty} (a : A) (x : V.Element) : (sumSig A V h).Element

The a-th copy injection V ↪ 𝟙+Σ_a V: send x∈|V| to the sum element whose proper neighbourhoods are the a-copies aX with X∈x.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise617Gen.sinjU_mem_jU {A : Type} [DecidableEq A] {β : Type v} {V : NeighborhoodSystem β} {h : ∀ (X : Set β), V.mem X → X.Nonempty} : sinjU.mem jU

@[simp]

theorem Domain.Neighborhood.Exercise617Gen.sinjC_mem_jc {A : Type} [DecidableEq A] {β : Type v} {V : NeighborhoodSystem β} {h : ∀ (X : Set β), V.mem X → X.Nonempty} {a : A} {x : V.Element} {X : Set β} (hX : V.mem X) : (sinjC a x).mem (jc a X) ↔ x.mem X

theorem Domain.Neighborhood.Exercise617Gen.sinjC_mono {A : Type} [DecidableEq A] {β : Type v} {V : NeighborhoodSystem β} {h : ∀ (X : Set β), V.mem X → X.Nonempty} {a : A} {x x' : V.Element} (hxle : x ≤ x') : sinjC a x ≤ sinjC a x'

The sum map Σ f = I_𝟙 + Σ_a f and its functoriality.

def Domain.Neighborhood.Exercise617Gen.sumMapSig {A : Type} [DecidableEq A] {β₀ β₁ : Type v} {V₀ : NeighborhoodSystem β₀} {V₁ : NeighborhoodSystem β₁} {h₀ : ∀ (X : Set β₀), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β₁), V₁.mem Y → Y.Nonempty} (f : ApproximableMap V₀ V₁) : ApproximableMap (sumSig A V₀ h₀) (sumSig A V₁ h₁)

The indexed sum map Σf = I_𝟙 + Σ_a f acting as the identity on the 𝟙-summand and as f on each a-copy. The generic analogue of sumMap3 (idMap unitSys) f f.

Equations

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

theorem Domain.Neighborhood.Exercise617Gen.isStrict_sumMapSig {A : Type} [DecidableEq A] {β₀ β₁ : Type v} {V₀ : NeighborhoodSystem β₀} {V₁ : NeighborhoodSystem β₁} {h₀ : ∀ (X : Set β₀), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β₁), V₁.mem Y → Y.Nonempty} (f : ApproximableMap V₀ V₁) : Exercise510.IsStrict (sumMapSig f)

The sum map is strict: it sends ⊥ = master only to master.

@[simp]

theorem Domain.Neighborhood.Exercise617Gen.sumMapSig_rel {A : Type} [DecidableEq A] {β₀ β₁ : Type v} {V₀ : NeighborhoodSystem β₀} {V₁ : NeighborhoodSystem β₁} {h₀ : ∀ (X : Set β₀), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β₁), V₁.mem Y → Y.Nonempty} {f : ApproximableMap V₀ V₁} {W : Set (SigTok A β₀)} {W' : Set (SigTok A β₁)} : (sumMapSig f).rel W W' ↔ (sumSig A V₀ h₀).mem W ∧ (sumSig A V₁ h₁).mem W' ∧ (W' = masterSig V₁ ∨ W = jU ∧ W' = jU ∨ ∃ (a : A) (X : Set β₀) (Y' : Set β₁), W = jc a X ∧ W' = jc a Y' ∧ f.rel X Y')

theorem Domain.Neighborhood.Exercise617Gen.sumMapSig_sinjU {A : Type} [DecidableEq A] {β₀ β₁ : Type v} {V₀ : NeighborhoodSystem β₀} {V₁ : NeighborhoodSystem β₁} {h₀ : ∀ (X : Set β₀), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β₁), V₁.mem Y → Y.Nonempty} (f : ApproximableMap V₀ V₁) : (sumMapSig f).toElementMap sinjU = sinjU

Σf fixes the basepoint injection.

theorem Domain.Neighborhood.Exercise617Gen.sumMapSig_sinjC {A : Type} [DecidableEq A] {β₀ β₁ : Type v} {V₀ : NeighborhoodSystem β₀} {V₁ : NeighborhoodSystem β₁} {h₀ : ∀ (X : Set β₀), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β₁), V₁.mem Y → Y.Nonempty} (f : ApproximableMap V₀ V₁) (a : A) (x : V₀.Element) : (sumMapSig f).toElementMap (sinjC a x) = sinjC a (f.toElementMap x)

Σf on the a-copy injection: (Σf)(inj_a x) = inj_a (f x).

theorem Domain.Neighborhood.Exercise617Gen.sumMapSig_id {A : Type} [DecidableEq A] {β₀ : Type v} {V₀ : NeighborhoodSystem β₀} {h₀ : ∀ (X : Set β₀), V₀.mem X → X.Nonempty} : sumMapSig (ApproximableMap.idMap V₀) = ApproximableMap.idMap (sumSig A V₀ h₀)

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

theorem Domain.Neighborhood.Exercise617Gen.sumMapSig_comp {A : Type} [DecidableEq A] {β₀ β₁ β₂ : Type v} {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₂) (f : ApproximableMap V₀ V₁) : sumMapSig (g.comp f) = (sumMapSig g).comp (sumMapSig f)

Functoriality (composition): Σ(g∘f) = Σg ∘ Σf.

The endofunctor Tsig(X) = 𝟙 + Σ_a X on the ∅-free category.

def Domain.Neighborhood.Exercise617Gen.tsigObj (A : Type) [DecidableEq A] (D : StrictDomainObj) : StrictDomainObj

Tsig on objects: Tsig(D) = 𝟙 + Σ_a D, again ∅-free (sumSig_nonempty).

Equations

• Domain.Neighborhood.Exercise617Gen.tsigObj A D = { carrier := Domain.Neighborhood.Exercise617Gen.SigTok A D.carrier, sys := Domain.Neighborhood.Exercise617Gen.sumSig A D.sys ⋯, nonempty := ⋯ }

@[simp]

theorem Domain.Neighborhood.Exercise617Gen.tsigObj_sys (A : Type) [DecidableEq A] (D : StrictDomainObj) : (tsigObj A D).sys = sumSig A D.sys ⋯

def Domain.Neighborhood.Exercise617Gen.tsigMapHom (A : Type) [DecidableEq A] {D E : StrictDomainObj} (f : Category.Hom D E) : Category.Hom (tsigObj A D) (tsigObj A E)

Tsig on maps: Tsig(f) = I_𝟙 + Σ_a f, strict by isStrict_sumMapSig.

Equations

• Domain.Neighborhood.Exercise617Gen.tsigMapHom A f = ⟨Domain.Neighborhood.Exercise617Gen.sumMapSig ↑f, ⋯⟩

@[simp]

theorem Domain.Neighborhood.Exercise617Gen.tsigMapHom_val (A : Type) [DecidableEq A] {D E : StrictDomainObj} (f : Category.Hom D E) : ↑(tsigMapHom A f) = sumMapSig ↑f

def Domain.Neighborhood.Exercise617Gen.Tsig (A : Type) [DecidableEq A] : Endofunctor StrictDomainObj

The functor Tsig(X) = 𝟙 + Σ_{a:A} X on the category of ∅-free domains and strict maps.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise617Gen.Tsig_obj (A : Type) [DecidableEq A] (D : StrictDomainObj) : (Tsig A).obj D = tsigObj A D

@[simp]

theorem Domain.Neighborhood.Exercise617Gen.Tsig_map_val (A : Type) [DecidableEq A] {D E : StrictDomainObj} (f : Category.Hom D E) : ↑((Tsig A).map f) = sumMapSig ↑f

Stage 3: the domain equation Cₐ ≅ 𝟙 + Σ_a Cₐ.

The alphabet-generic analogue of Example62C (C ≅ 𝟙 + C + C). Prepending the letter a to a neighbourhood gives embA a X; a Cₐ-neighbourhood is the master, the terminator {Λ}, or some a-copy aX, exactly the shapes of the A-indexed sum 𝟙 + Σ_a Cₐ.

def Domain.Neighborhood.Exercise617Gen.embA {A : Type} (a : A) (X : Set (Strn A)) : Set (Strn A)

aX = {a :: w' ∣ w' ∈ X}: the a-prefixed copy of a neighbourhood.

Equations

• Domain.Neighborhood.Exercise617Gen.embA a X = {w : Domain.Neighborhood.Exercise617Gen.Strn A | ∃ (w' : List A), w = a :: w' ∧ w' ∈ X}

@[simp]

theorem Domain.Neighborhood.Exercise617Gen.mem_embA {A : Type} {a : A} {X : Set (Strn A)} {w : Strn A} : w ∈ embA a X ↔ ∃ (w' : List A), w = a :: w' ∧ w' ∈ X

theorem Domain.Neighborhood.Exercise617Gen.embA_eq_prependN {A : Type} (a : A) (X : Set (Strn A)) : embA a X = prependN [a] X

theorem Domain.Neighborhood.Exercise617Gen.embA_coneN {A : Type} (a : A) (σ : Strn A) : embA a (coneN σ) = coneN (a :: σ)

theorem Domain.Neighborhood.Exercise617Gen.embA_singleton {A : Type} (a : A) (σ : Strn A) : embA a {σ} = {a :: σ}

theorem Domain.Neighborhood.Exercise617Gen.memCn_embA {A : Type} (a : A) {X : Set (Strn A)} (hX : memCn X) : memCn (embA a X)

theorem Domain.Neighborhood.Exercise617Gen.nil_not_mem_embA {A : Type} {a : A} {X : Set (Strn A)} : [] ∉ embA a X

theorem Domain.Neighborhood.Exercise617Gen.embA_ne_univ {A : Type} (a : A) (X : Set (Strn A)) : embA a X ≠ Set.univ

theorem Domain.Neighborhood.Exercise617Gen.embA_inter {A : Type} (a : A) (X X' : Set (Strn A)) : embA a X ∩ embA a X' = embA a (X ∩ X')

theorem Domain.Neighborhood.Exercise617Gen.embA_inter_ne {A : Type} {a a' : A} (h : a ≠ a') (X Y : Set (Strn A)) : embA a X ∩ embA a' Y = ∅

theorem Domain.Neighborhood.Exercise617Gen.embA_subset {A : Type} {a : A} {X X' : Set (Strn A)} : embA a X ⊆ embA a X' ↔ X ⊆ X'

theorem Domain.Neighborhood.Exercise617Gen.embA_injective {A : Type} {a : A} {X X' : Set (Strn A)} (h : embA a X = embA a X') : X = X'

theorem Domain.Neighborhood.Exercise617Gen.embA_nonempty {A : Type} {a : A} {X : Set (Strn A)} (hX : X.Nonempty) : (embA a X).Nonempty

theorem Domain.Neighborhood.Exercise617Gen.memCn_embA_inv {A : Type} {a : A} {W : Set (Strn A)} (h : memCn (embA a W)) : memCn W

theorem Domain.Neighborhood.Exercise617Gen.embA_ne {A : Type} {a a' : A} (h : a ≠ a') {X Y : Set (Strn A)} (hX : X.Nonempty) : embA a X ≠ embA a' Y

theorem Domain.Neighborhood.Exercise617Gen.singleton_nil_inter_embA {A : Type} (a : A) (X : Set (Strn A)) : {[]} ∩ embA a X = ∅

theorem Domain.Neighborhood.Exercise617Gen.singleton_nil_ne_univ {A : Type} [Inhabited A] : {[]} ≠ Set.univ

theorem Domain.Neighborhood.Exercise617Gen.singleton_nil_ne_embA {A : Type} (a : A) (X : Set (Strn A)) : {[]} ≠ embA a X

theorem Domain.Neighborhood.Exercise617Gen.memCn_cases {A : Type} {W : Set (Strn A)} (hW : memCn W) : W = Set.univ ∨ W = {[]} ∨ ∃ (a : A) (X : Set (Strn A)), memCn X ∧ W = embA a X

The shape of a Cₐ-neighbourhood. Every neighbourhood is the master Σ*, the terminator {Λ}, or an a-copy aX with X ∈ Cₐ.

The sum target 𝟙 + Σ_a Cₐ and its inversion lemmas.

@[reducible, inline]

abbrev Domain.Neighborhood.Exercise617Gen.CCn (A : Type) [DecidableEq A] : NeighborhoodSystem (SigTok A (Strn A))

The right-hand side of the domain equation: the A-indexed sum 𝟙 + Σ_a Cₐ.

Equations

• Domain.Neighborhood.Exercise617Gen.CCn A = Domain.Neighborhood.Exercise617Gen.sumSig A (Domain.Neighborhood.Exercise617Gen.Cn A) ⋯

theorem Domain.Neighborhood.Exercise617Gen.sumSig_mem_jc_inv {A : Type} [DecidableEq A] {a : A} {X : Set (Strn A)} (h : (CCn A).mem (jc a X)) : (Cn A).mem X

The forward half toCC : |Cₐ| → |𝟙 + Σ_a Cₐ|.

def Domain.Neighborhood.Exercise617Gen.toCC {A : Type} [DecidableEq A] (x : (Cn A).Element) : (CCn A).Element

Forward half of Cₐ ≅ 𝟙 + Σ_a Cₐ. Records, for each branch, whether x finishes at Λ (the 𝟙-summand) or reaches the a-copy aX (the a-th summand).

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise617Gen.toCC_mem_jU {A : Type} [DecidableEq A] {x : (Cn A).Element} : (toCC x).mem jU ↔ x.mem {[]}

theorem Domain.Neighborhood.Exercise617Gen.toCC_mem_jc {A : Type} [DecidableEq A] {x : (Cn A).Element} {a : A} {X : Set (Strn A)} (hX : (Cn A).mem X) : (toCC x).mem (jc a X) ↔ x.mem (embA a X)

theorem Domain.Neighborhood.Exercise617Gen.embA_eq_embA {A : Type} {a a' : A} {X X' : Set (Strn A)} (hXne : X.Nonempty) (h : embA a X = embA a' X') : a = a' ∧ X = X'

Prefixed copies determine index and set: aX = a'X' (with X non-empty) forces a=a', X=X'.

The inverse half fromCC : |𝟙 + Σ_a Cₐ| → |Cₐ|.

def Domain.Neighborhood.Exercise617Gen.fromCC {A : Type} [DecidableEq A] (s : (CCn A).Element) : (Cn A).Element

Inverse half of Cₐ ≅ 𝟙 + Σ_a Cₐ.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise617Gen.fromCC_mem_nil {A : Type} [DecidableEq A] [Inhabited A] {s : (CCn A).Element} : (fromCC s).mem {[]} ↔ s.mem jU

theorem Domain.Neighborhood.Exercise617Gen.fromCC_mem_embA {A : Type} [DecidableEq A] {s : (CCn A).Element} {a : A} {X : Set (Strn A)} (hX : (Cn A).mem X) : (fromCC s).mem (embA a X) ↔ s.mem (jc a X)

The two halves are mutually inverse.

theorem Domain.Neighborhood.Exercise617Gen.fromCC_toCC {A : Type} [DecidableEq A] (x : (Cn A).Element) : fromCC (toCC x) = x

theorem Domain.Neighborhood.Exercise617Gen.toCC_fromCC {A : Type} [DecidableEq A] [Inhabited A] (s : (CCn A).Element) : toCC (fromCC s) = s

def Domain.Neighborhood.Exercise617Gen.ccEquiv {A : Type} [DecidableEq A] [Inhabited A] : (Cn A).Element ≃o (CCn A).Element

The isomorphism |Cₐ| ≃o |𝟙 + Σ_a Cₐ|.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise617Gen.ccEquiv_apply {A : Type} [DecidableEq A] [Inhabited A] (x : (Cn A).Element) : ccEquiv x = toCC x

Bridging the isomorphism to the successors consMapN.

theorem Domain.Neighborhood.Exercise617Gen.consMapN_mem_embA {A : Type} {a : A} {z : (Cn A).Element} {X : Set (Strn A)} (hX : (Cn A).mem X) : ((consMapN a).toElementMap z).mem (embA a X) ↔ z.mem X

theorem Domain.Neighborhood.Exercise617Gen.consMapN_not_mem_embA_ne {A : Type} {a c : A} (hac : a ≠ c) {z : (Cn A).Element} {X : Set (Strn A)} : ¬((consMapN a).toElementMap z).mem (embA c X)

theorem Domain.Neighborhood.Exercise617Gen.consMapN_not_mem_nil {A : Type} {a : A} {z : (Cn A).Element} : ¬((consMapN a).toElementMap z).mem {[]}

theorem Domain.Neighborhood.Exercise617Gen.toCC_consMapN {A : Type} [DecidableEq A] (a : A) (z : (Cn A).Element) : toCC ((consMapN a).toElementMap z) = sinjC a z

toCC ∘ (a·) = inj_a. Prepending the letter a to z is, across Cₐ ≅ 𝟙+Σ_a Cₐ, the injection of z into the a-th summand.

theorem Domain.Neighborhood.Exercise617Gen.toCC_strElemN_nil {A : Type} [DecidableEq A] : toCC (strElemN []) = sinjU

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

Cₐ as a Tsig-algebra.

def Domain.Neighborhood.Exercise617Gen.Cnobj (A : Type) : StrictDomainObj

Cₐ as an object of the ∅-free category.

Equations

• Domain.Neighborhood.Exercise617Gen.Cnobj A = { carrier := Domain.Neighborhood.Exercise617Gen.Strn A, sys := Domain.Neighborhood.Exercise617Gen.Cn A, nonempty := ⋯ }

@[simp]

theorem Domain.Neighborhood.Exercise617Gen.Cnobj_sys (A : Type) : (Cnobj A).sys = Cn A

def Domain.Neighborhood.Exercise617Gen.cnStr {A : Type} [DecidableEq A] [Inhabited A] : Category.Hom ((Tsig A).obj (Cnobj A)) (Cnobj A)

The Tsig-algebra structure on Cₐ. The structure map i : 𝟙+Σ_a Cₐ → Cₐ is the inverse of the domain-equation isomorphism ccEquiv, strict by isStrict_ofIso.

Equations

• Domain.Neighborhood.Exercise617Gen.cnStr = ⟨Domain.Neighborhood.ApproximableMap.ofIso Domain.Neighborhood.Exercise617Gen.ccEquiv.symm, ⋯⟩

def Domain.Neighborhood.Exercise617Gen.Cnalg (A : Type) [DecidableEq A] [Inhabited A] : TAlgebra (Tsig A)

Cₐ is a Tsig-algebra for Tsig(X) = 𝟙 + Σ_a X.

Equations

• Domain.Neighborhood.Exercise617Gen.Cnalg A = { carrier := Domain.Neighborhood.Exercise617Gen.Cnobj A, str := Domain.Neighborhood.Exercise617Gen.cnStr }

The liftCn combinator: an approximable map out of Cₐ (generic

Exercise419.liftC).

theorem Domain.Neighborhood.Exercise617Gen.not_coneN_subset_singleton {A : Type} [Inhabited A] (τ σ : Strn A) : ¬coneN τ ⊆ {σ}

A cone is never contained in a singleton: it has the two distinct elements τ and τ·default.

theorem Domain.Neighborhood.Exercise617Gen.coneN_ne_singleton {A : Type} [Inhabited A] (τ σ : Strn A) : coneN τ ≠ {σ}

def Domain.Neighborhood.Exercise617Gen.liftCn {A : Type} [Inhabited A] {β : Type} (V : NeighborhoodSystem β) (coneVal singVal : Strn A → V.Element) (hcone : ∀ {σ τ : Strn A}, σ <+: τ → coneVal σ ≤ coneVal τ) (hsing : ∀ {σ τ : Strn A}, σ <+: τ → coneVal σ ≤ singVal τ) : ApproximableMap (Cn A) V

A map Cₐ → V determined by its value coneVal σ on each partial element σ⊥ and singVal σ on each total element σ. (The alphabet-generic copy of Exercise419.liftC.)

Equations

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

theorem Domain.Neighborhood.Exercise617Gen.liftCn_strBot {A : Type} [Inhabited A] {β : Type} (V : NeighborhoodSystem β) (coneVal singVal : Strn A → V.Element) (hcone : ∀ {σ τ : Strn A}, σ <+: τ → coneVal σ ≤ coneVal τ) (hsing : ∀ {σ τ : Strn A}, σ <+: τ → coneVal σ ≤ singVal τ) (σ : Strn A) : (liftCn V coneVal singVal ⋯ ⋯).toElementMap (strBotN σ) = coneVal σ

theorem Domain.Neighborhood.Exercise617Gen.liftCn_strElem {A : Type} [Inhabited A] {β : Type} (V : NeighborhoodSystem β) (coneVal singVal : Strn A → V.Element) (hcone : ∀ {σ τ : Strn A}, σ <+: τ → coneVal σ ≤ coneVal τ) (hsing : ∀ {σ τ : Strn A}, σ <+: τ → coneVal σ ≤ singVal τ) (σ : Strn A) : (liftCn V coneVal singVal ⋯ ⋯).toElementMap (strElemN σ) = singVal σ

theorem Domain.Neighborhood.Exercise617Gen.map_ext_Cn {A β : Type} {V : NeighborhoodSystem β} {f g : ApproximableMap (Cn A) V} (hbot : ∀ (σ : Strn A), f.toElementMap (strBotN σ) = g.toElementMap (strBotN σ)) (helem : ∀ (σ : Strn A), f.toElementMap (strElemN σ) = g.toElementMap (strElemN σ)) : f = g

Two maps out of Cₐ agree once they agree on every σ⊥ and σ (generic Exercise516.map_ext_C).

Initiality of (Cₐ, i): the unique homomorphism into any Tsig-algebra.

def Domain.Neighborhood.Exercise617Gen.descE {A : Type} [DecidableEq A] (B : TAlgebra (Tsig A)) : B.carrier.sys.Element

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

Equations

• Domain.Neighborhood.Exercise617Gen.descE B = (↑B.str).toElementMap Domain.Neighborhood.Exercise617Gen.sinjU

def Domain.Neighborhood.Exercise617Gen.descF {A : Type} [DecidableEq A] (B : TAlgebra (Tsig A)) (a : A) (y : B.carrier.sys.Element) : B.carrier.sys.Element

The a-th successor operation f_a = k ∘ inj_a.

Equations

• Domain.Neighborhood.Exercise617Gen.descF B a y = (↑B.str).toElementMap (Domain.Neighborhood.Exercise617Gen.sinjC a y)

def Domain.Neighborhood.Exercise617Gen.descVal {A : Type} [DecidableEq A] (B : TAlgebra (Tsig A)) (z : B.carrier.sys.Element) : Strn A → B.carrier.sys.Element

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

Equations

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

theorem Domain.Neighborhood.Exercise617Gen.descF_mono {A : Type} [DecidableEq A] (B : TAlgebra (Tsig A)) (a : A) {y y' : B.carrier.sys.Element} (h : y ≤ y') : descF B a y ≤ descF B a y'

theorem Domain.Neighborhood.Exercise617Gen.descVal_mono_z {A : Type} [DecidableEq A] (B : TAlgebra (Tsig A)) {z z' : B.carrier.sys.Element} (h : z ≤ z') (σ : Strn A) : descVal B z σ ≤ descVal B z' σ

theorem Domain.Neighborhood.Exercise617Gen.descVal_append {A : Type} [DecidableEq A] (B : TAlgebra (Tsig A)) (z : B.carrier.sys.Element) (σ ρ : Strn A) : descVal B z (σ ++ ρ) = descVal B (descVal B z ρ) σ

theorem Domain.Neighborhood.Exercise617Gen.descMap_hcone {A : Type} [DecidableEq A] (B : TAlgebra (Tsig A)) {σ τ : Strn A} (h : σ <+: τ) : descVal B B.carrier.sys.bot σ ≤ descVal B B.carrier.sys.bot τ

theorem Domain.Neighborhood.Exercise617Gen.descMap_hsing {A : Type} [DecidableEq A] (B : TAlgebra (Tsig A)) {σ τ : Strn A} (h : σ <+: τ) : descVal B B.carrier.sys.bot σ ≤ descVal B (descE B) τ

def Domain.Neighborhood.Exercise617Gen.descMap {A : Type} [DecidableEq A] [Inhabited A] (B : TAlgebra (Tsig A)) : ApproximableMap (Cn A) B.carrier.sys

The homomorphism Cₐ → E, built by liftCn from the head-recursion.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise617Gen.descMap_strBot {A : Type} [DecidableEq A] [Inhabited A] (B : TAlgebra (Tsig A)) (σ : Strn A) : (descMap B).toElementMap (strBotN σ) = descVal B B.carrier.sys.bot σ

@[simp]

theorem Domain.Neighborhood.Exercise617Gen.descMap_strElem {A : Type} [DecidableEq A] [Inhabited A] (B : TAlgebra (Tsig A)) (σ : Strn A) : (descMap B).toElementMap (strElemN σ) = descVal B (descE B) σ

theorem Domain.Neighborhood.Exercise617Gen.Cn_bot_eq_strBotN_nil {A : Type} : (Cn A).bot = strBotN []

theorem Domain.Neighborhood.Exercise617Gen.descMap_strict {A : Type} [DecidableEq A] [Inhabited A] (B : TAlgebra (Tsig A)) : Exercise510.IsStrict (descMap B)

def Domain.Neighborhood.Exercise617Gen.descStrict {A : Type} [DecidableEq A] [Inhabited A] (B : TAlgebra (Tsig A)) : Category.Hom (Cnobj A) B.carrier

The bundled strict homomorphism Cₐ → E.

Equations

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

The homomorphism square and uniqueness.

theorem Domain.Neighborhood.Exercise617Gen.genKey {A : Type} [DecidableEq A] (B : TAlgebra (Tsig A)) (g : ApproximableMap (Cn A) B.carrier.sys) (a : A) (w : (Cn A).Element) : (↑B.str).toElementMap ((sumMapSig g).toElementMap (toCC ((consMapN a).toElementMap w))) = descF B a (g.toElementMap w)

theorem Domain.Neighborhood.Exercise617Gen.genKey0 {A : Type} [DecidableEq A] (B : TAlgebra (Tsig A)) (g : ApproximableMap (Cn A) B.carrier.sys) : (↑B.str).toElementMap ((sumMapSig g).toElementMap (toCC (strElemN []))) = descE B

theorem Domain.Neighborhood.Exercise617Gen.genKeyBot {A : Type} [DecidableEq A] [Inhabited A] (B : TAlgebra (Tsig A)) (g : ApproximableMap (Cn A) B.carrier.sys) : (↑B.str).toElementMap ((sumMapSig g).toElementMap (toCC (strBotN []))) = B.carrier.sys.bot

theorem Domain.Neighborhood.Exercise617Gen.ccEquiv_symm_comp {A : Type} [DecidableEq A] [Inhabited A] : (ApproximableMap.ofIso ccEquiv.symm).comp (ApproximableMap.ofIso ccEquiv) = ApproximableMap.idMap (Cn A)

theorem Domain.Neighborhood.Exercise617Gen.ccEquiv_comp_symm {A : Type} [DecidableEq A] [Inhabited A] : (ApproximableMap.ofIso ccEquiv).comp (ApproximableMap.ofIso ccEquiv.symm) = ApproximableMap.idMap (CCn A)

theorem Domain.Neighborhood.Exercise617Gen.rec_determines {A : Type} [DecidableEq A] [Inhabited A] (B : TAlgebra (Tsig A)) (g : ApproximableMap (Cn A) B.carrier.sys) (hg : g = ((↑B.str).comp (sumMapSig g)).comp (ApproximableMap.ofIso ccEquiv)) : g = descMap B

Any map satisfying the homomorphism recursion equals descMap.

theorem Domain.Neighborhood.Exercise617Gen.descMap_satisfiesRec {A : Type} [DecidableEq A] [Inhabited A] (B : TAlgebra (Tsig A)) : descMap B = ((↑B.str).comp (sumMapSig (descMap B))).comp (ApproximableMap.ofIso ccEquiv)

Cₐ's algebra map satisfies the recursion.

theorem Domain.Neighborhood.Exercise617Gen.descComm {A : Type} [DecidableEq A] [Inhabited A] (B : TAlgebra (Tsig A)) : (descMap B).comp (ApproximableMap.ofIso ccEquiv.symm) = (↑B.str).comp (sumMapSig (descMap B))

The homomorphism square desc ∘ i = k ∘ T(desc).

def Domain.Neighborhood.Exercise617Gen.descAlgHom {A : Type} [DecidableEq A] [Inhabited A] (B : TAlgebra (Tsig A)) : AlgHom (Cnalg A) B

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

Equations

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

theorem Domain.Neighborhood.Exercise617Gen.descAlgHom_uniq {A : Type} [DecidableEq A] [Inhabited A] (B : TAlgebra (Tsig A)) (h' : AlgHom (Cnalg A) B) : h' = descAlgHom B

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

def Domain.Neighborhood.Exercise617Gen.CnisInitial (A : Type) [DecidableEq A] [Inhabited A] : IsInitial (Cnalg A)

Exercise 6.17 part 2 — (Cₐ, i) is an initial Tsig-algebra for Tsig(X) = 𝟙 + Σ_a X. The descent map φ : Cₐ → E is the closed-form head-recursion φ(Λ) = e, φ(a·x) = f_a(φ x) (f_a = k ∘ inj_a), built choice-free via liftCn; it is the unique Tsig-algebra homomorphism, so Cₐ is the initial algebra of X ↦ 𝟙 + Σ_a X.

Equations

• Domain.Neighborhood.Exercise617Gen.CnisInitial A = { desc := Domain.Neighborhood.Exercise617Gen.descAlgHom, uniq := ⋯ }

theorem Domain.Neighborhood.Exercise617Gen.Cn_domain_equation (A : Type) [DecidableEq A] [Inhabited A] : Cn A ≅ᴰ CCn A

Exercise 6.17 part 2 — the domain equation Cₐ ≅ 𝟙 + Σ_a Cₐ.

Instantiation: Cₙ ≅ 𝟙 + n·Cₙ over the n-letter alphabet Fin (n+1).

Taking A := Fin (n+1) recovers Scott's Cₙ: the domain of finite-or-infinite sequences over an (n+1)-letter alphabet, satisfying Cₙ ≅ 𝟙 + (n+1)·Cₙ. (For n = 1, Fin 2 ≃ Bool recovers Example 6.2's C ≅ 𝟙 + C + C.)

theorem Domain.Neighborhood.Exercise617Gen.Cfin_domain_equation (n : ℕ) : Cn (Fin (n + 1)) ≅ᴰ CCn (Fin (n + 1))

Cₙ ≅ 𝟙 + (n+1)·Cₙ over the alphabet Fin (n+1).

def Domain.Neighborhood.Exercise617Gen.CfinIsInitial (n : ℕ) : IsInitial (Cnalg (Fin (n + 1)))

Cₙ is the initial algebra of X ↦ 𝟙 + Σ_{Fin (n+1)} X.

Equations

• Domain.Neighborhood.Exercise617Gen.CfinIsInitial n = Domain.Neighborhood.Exercise617Gen.CnisInitial (Fin (n + 1))