Lecture VI — Theorem 6.14 (Scott 1981, PRG-19): existence of initial

T-algebras

THEOREM 6.14. If the functor T is continuous on maps and monotone and continuous on domains, and if there is a set Γ such that {Γ} ◁ T({Γ}), then there exists an initial T-algebra.

Scott's proof iterates the functor from the generating system {Γ}. The assumption {Γ} ◁ T({Γ}) means T({Γ}) is a system over the same token set Γ; iterating, every Tⁿ({Γ}) is over Γ and Tⁿ({Γ}) ◁ Tⁿ⁺¹({Γ}). The colimit

𝒟 = ⋃ₙ Tⁿ({Γ})

is then a system over Γ with Tⁿ({Γ}) ◁ 𝒟, whence 𝒟 ◁ T(𝒟), and continuity on domains gives T(𝒟) = 𝒟 — the isomorphism 𝒟 ≅ T(𝒟) is the identity. So 𝒟 is a T-algebra, and:

• existence of homomorphisms out of 𝒟 is Theorem 6.9 (nonempty_algHom_of_continuousOnMaps);
• uniqueness is the ρₙ = iₙ ∘ jₙ projection-chain argument: T(ρₙ) = ρₙ₊₁ (monotone on domains), ⋃ₙ ρₙ = I_𝒟, and any homomorphism h is ⋃ₙ h∘ρₙ, the least fixed point of λh. k ∘ T(h).

The carrier-type subtlety

The abstract T : Endofunctor DomainObj need not preserve token types, so Tⁿ({Γ}) a priori live over different carriers. The hypothesis {Γ} ◁ T({Γ}) already pins T({Γ}) to Γ's carrier, and monotone on domains (Definition 6.13, MonotoneAt.carrier_eq) propagates the identification up the tower. We carry the carrier equalities explicitly and transport along them; the transport of the subdomain relation is the choice-free subsystem_cast.

Lean note: rw fragility on defeq-but-not-syntactic implicits

Throughout the uniqueness half, rw with explicit arguments at the ApproximableMap / NeighborhoodSystem level repeatedly failed with "did not find an occurrence of the pattern" even when the pattern was visibly present — because the implicit carriers/systems were defeq but not syntactically equal (colim s vs (colimAlg s).carrier.sys vs (objColim s).sys; the abbrev objColim vs the literal ⟨Tok, colim s⟩). Three fixes, used throughout gcomp_rho_succ/gcomp_eq:

• work at the categorical ⊚ / Category.assoc level, where the implicits are concrete DomainObjs rather than systems, so unification has nothing to get stuck on;
• prefer congrArg / calc term-mode proofs (e.g. congrArg (fun x => g.hom ⊚ x) (key_rho s n)), since calc bridges adjacent steps by defeq rather than by syntactic match;
• to rewrite with a lemma whose implicit is pinned to the "wrong" representation (e.g. comp_idMap, whose idMap arg is tied to g.hom's domain (colimAlg s).carrier.sys), first bind the fact via a have stated in the desired form (have e : g.hom.comp (idMap (colim s)) = g.hom := comp_idMap g.hom — the have unifies by defeq), then rw [← e].

Carrier-transport helpers

theorem Domain.Neighborhood.Theorem614.subsystem_cast {α β : Type w} (e : β = α) {D E : NeighborhoodSystem β} (h : D ◁ E) : e ▸ D ◁ e ▸ E

Transport a subsystem relation D ◁ E along a carrier-type equality β = α. Choice-free.

theorem Domain.Neighborhood.Theorem614.rec_trans {α β γ : Type w} (e : β = γ) (e' : γ = α) (x : NeighborhoodSystem β) : e' ▸ e ▸ x = ⋯ ▸ x

Transport composition for neighbourhood systems: e' ▸ (e ▸ x) = (e.trans e') ▸ x.

theorem Domain.Neighborhood.Theorem614.mem_cast {α β : Type w} (e : β = α) (V : NeighborhoodSystem β) (X : Set α) : (e ▸ V).mem X ↔ V.mem (⋯ ▸ X)

Membership in a transported system: (e ▸ V).mem X ↔ V.mem (e.symm ▸ X).

theorem Domain.Neighborhood.Theorem614.set_rec_trans {α β γ : Type w} (e : β = γ) (e' : γ = α) (X : Set β) : e' ▸ e ▸ X = ⋯ ▸ X

Transport composition for sets: e' ▸ (e ▸ X) = (e.trans e') ▸ X.

The setup bundle (hypotheses of Theorem 6.14)

structure Domain.Neighborhood.Theorem614.Setup : Type (w + 1)

The hypotheses of Theorem 6.14, bundled: a functor T that is continuous on maps, monotone and continuous on domains, together with a generating system Γ over a token type Tok such that {Γ} ◁ T({Γ}) (the carrier of T({Γ}) is identified with Tok by ceq, and hsub is Scott's {Γ} ◁ T({Γ})).

• T : Endofunctor DomainObj

  The functor.

• hmaps : ContinuousOnMaps self.T

  T is continuous on maps (Definition 6.8).

• hmono : MonotoneOnDomains self.T

  T is monotone on domains (Definition 6.13).

• hcont : ContinuousOnDomains self.T

  T is continuous on domains (Definition 6.13).

• Tok : Type w

  The token type of the generating system.

• Γ : NeighborhoodSystem self.Tok

  The generating system {Γ}.

• ceq : (self.T.obj { carrier := self.Tok, sys := self.Γ }).carrier = self.Tok

  T({Γ}) is a system over the same token type.

• hsub : self.Γ ◁ ⋯ ▸ (self.T.obj { carrier := self.Tok, sys := self.Γ }).sys

  Scott's hypothesis {Γ} ◁ T({Γ}).

The iterated functor tower Tⁿ({Γ})

def Domain.Neighborhood.Theorem614.iter (s : Setup) (n : ℕ) : (S : NeighborhoodSystem s.Tok) ×' (ceq : (s.T.obj { carrier := s.Tok, sys := S }).carrier = s.Tok) ×' S ◁ ceq ▸ (s.T.obj { carrier := s.Tok, sys := S }).sys

The iterated tower, as data: at level n, the system Tⁿ({Γ}) over Tok, the carrier identification (T.obj Tⁿ({Γ})).carrier = Tok, and the subdomain relation Tⁿ({Γ}) ◁ Tⁿ⁺¹({Γ}) (where Tⁿ⁺¹({Γ}) is the carrier-transport of T(Tⁿ({Γ}))). The successor step uses monotone on domains (MonotoneAt) to obtain the next carrier identification and subdomain relation. Choice-free.

Equations

• Domain.Neighborhood.Theorem614.iter s 0 = ⟨s.Γ, ⟨⋯, ⋯⟩⟩
• Domain.Neighborhood.Theorem614.iter s n.succ = ⟨⋯ ▸ (s.T.obj { carrier := s.Tok, sys := (Domain.Neighborhood.Theorem614.iter s n).fst }).sys, ⟨⋯, ⋯⟩⟩

def Domain.Neighborhood.Theorem614.Dsys (s : Setup) (n : ℕ) : NeighborhoodSystem s.Tok

Tⁿ({Γ}), the n-th system in the tower (over Tok).

Equations

• Domain.Neighborhood.Theorem614.Dsys s n = (Domain.Neighborhood.Theorem614.iter s n).fst

theorem Domain.Neighborhood.Theorem614.Dceq (s : Setup) (n : ℕ) : (s.T.obj { carrier := s.Tok, sys := Dsys s n }).carrier = s.Tok

The carrier identification (T.obj Tⁿ({Γ})).carrier = Tok.

theorem Domain.Neighborhood.Theorem614.Dsys_succ (s : Setup) (n : ℕ) : Dsys s (n + 1) = ⋯ ▸ (s.T.obj { carrier := s.Tok, sys := Dsys s n }).sys

Tⁿ⁺¹({Γ}) is the carrier-transport of T(Tⁿ({Γ})).

theorem Domain.Neighborhood.Theorem614.Dchain (s : Setup) (n : ℕ) : Dsys s n ◁ Dsys s (n + 1)

The basic subdomain step Tⁿ({Γ}) ◁ Tⁿ⁺¹({Γ}).

theorem Domain.Neighborhood.Theorem614.Dsys_master (s : Setup) (n : ℕ) : (Dsys s n).master = s.Γ.master

Every system in the tower has the same master Δ = Γ.

theorem Domain.Neighborhood.Theorem614.chain_le (s : Setup) {n m : ℕ} (h : n ≤ m) : Dsys s n ◁ Dsys s m

The tower is a ◁-chain: Tⁿ({Γ}) ◁ Tᵐ({Γ}) whenever n ≤ m.

The colimit 𝒟 = ⋃ₙ Tⁿ({Γ})

def Domain.Neighborhood.Theorem614.colim (s : Setup) : NeighborhoodSystem s.Tok

The colimit 𝒟 = ⋃ₙ Tⁿ({Γ}) as a neighbourhood system over Tok: a set is a neighbourhood of 𝒟 exactly when it is a neighbourhood of some Tⁿ({Γ}). Closure under consistent intersection uses that the tower is a chain (chain_le): any finite collection of neighbourhoods sits inside one level Tᴺ({Γ}), whose own inter_mem finishes the job.

Equations

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

@[simp]

theorem Domain.Neighborhood.Theorem614.mem_colim (s : Setup) {X : Set s.Tok} : (colim s).mem X ↔ ∃ (n : ℕ), (Dsys s n).mem X

@[simp]

theorem Domain.Neighborhood.Theorem614.colim_master (s : Setup) : (colim s).master = s.Γ.master

theorem Domain.Neighborhood.Theorem614.Dsys_sub_colim (s : Setup) (n : ℕ) : Dsys s n ◁ colim s

Each level of the tower is a subdomain of the colimit: Tⁿ({Γ}) ◁ 𝒟.

T(𝒟) and the relation 𝒟 ◁ T(𝒟)

theorem Domain.Neighborhood.Theorem614.colimCeq (s : Setup) : (s.T.obj { carrier := s.Tok, sys := colim s }).carrier = s.Tok

The carrier identification (T.obj 𝒟).carrier = Tok, from MonotoneAt of T⁰({Γ}) ◁ 𝒟.

def Domain.Neighborhood.Theorem614.Tcolim (s : Setup) : NeighborhoodSystem s.Tok

T(𝒟), the image of the colimit, as a system over Tok (via colimCeq).

Equations

• Domain.Neighborhood.Theorem614.Tcolim s = ⋯ ▸ (s.T.obj { carrier := s.Tok, sys := Domain.Neighborhood.Theorem614.colim s }).sys

theorem Domain.Neighborhood.Theorem614.Dsys_sub_Tcolim (s : Setup) (n : ℕ) : Dsys s (n + 1) ◁ Tcolim s

Tⁿ⁺¹({Γ}) ◁ T(𝒟): applying monotone on domains to Tⁿ({Γ}) ◁ 𝒟 and transporting.

theorem Domain.Neighborhood.Theorem614.Tcolim_master (s : Setup) : (Tcolim s).master = s.Γ.master

T(𝒟) and 𝒟 share the master Δ = Γ.

theorem Domain.Neighborhood.Theorem614.colim_sub_Tcolim (s : Setup) {X : Set s.Tok} (hX : (colim s).mem X) : (Tcolim s).mem X

The easy half of T(𝒟) = 𝒟: every neighbourhood of 𝒟 is a neighbourhood of T(𝒟) (𝒟 ⊆ T(𝒟)), since Tⁿ({Γ}) ◁ Tⁿ⁺¹({Γ}) ◁ T(𝒟).

theorem Domain.Neighborhood.Theorem614.Tcolim_sub_colim (s : Setup) {X : Set s.Tok} (hX : (Tcolim s).mem X) : (colim s).mem X

The continuity step (the hard half of T(𝒟) = 𝒟). Every neighbourhood of T(𝒟) is a neighbourhood of 𝒟. This is exactly Scott's T(𝒟) = T(⋃ₙ Tⁿ({Γ})) = ⋃ₙ Tⁿ⁺¹({Γ}) = 𝒟, obtained from continuity on domains applied to the directed family {Tⁿ({Γ})}.

theorem Domain.Neighborhood.Theorem614.Tcolim_eq_colim (s : Setup) : Tcolim s = colim s

T(𝒟) = 𝒟 (Scott's 𝒟 = T(𝒟)): the two systems have the same neighbourhoods (mutual inclusion via colim_sub_Tcolim/Tcolim_sub_colim) and the same master.

𝒟 is a T-algebra: the iso 𝒟 ≅ T(𝒟) is the identity

theorem Domain.Neighborhood.Theorem614.domainObj_ext {α c : Type w} (σ : NeighborhoodSystem c) (e : c = α) {V : NeighborhoodSystem α} (h : e ▸ σ = V) : { carrier := c, sys := σ } = { carrier := α, sys := V }

A DomainObj equality from a carrier equality and a transported-system equality.

def Domain.Neighborhood.Theorem614.isoOfEq {Obj : Type u_1} [Category Obj] {X Y : Obj} (h : X = Y) : Iso X Y

The identity isomorphism induced by an object equality in any category.

Equations

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

theorem Domain.Neighborhood.Theorem614.colimObj_eq (s : Setup) : s.T.obj { carrier := s.Tok, sys := colim s } = { carrier := s.Tok, sys := colim s }

T(𝒟) ≅ 𝒟 is the identity, packaged as a DomainObj equality T(𝒟) = 𝒟.

def Domain.Neighborhood.Theorem614.colimIso (s : Setup) : Iso (s.T.obj { carrier := s.Tok, sys := colim s }) { carrier := s.Tok, sys := colim s }

The isomorphism T(𝒟) ≅ 𝒟 making 𝒟 a T-algebra (the identity, since T(𝒟) = 𝒟).

Equations

• Domain.Neighborhood.Theorem614.colimIso s = Domain.Neighborhood.Theorem614.isoOfEq ⋯

def Domain.Neighborhood.Theorem614.colimAlg (s : Setup) : TAlgebra s.T

The colimit 𝒟 as a T-algebra, with structure map the iso T(𝒟) → 𝒟.

Equations

• Domain.Neighborhood.Theorem614.colimAlg s = { carrier := { carrier := s.Tok, sys := Domain.Neighborhood.Theorem614.colim s }, str := (Domain.Neighborhood.Theorem614.colimIso s).hom }

Existence of homomorphisms (Theorem 6.9)

theorem Domain.Neighborhood.Theorem614.nonempty_strict_algHom (s : Setup) (B : TAlgebra s.T) (hk : Exercise510.IsStrict B.str) : Nonempty { g : AlgHom (colimAlg s) B // Exercise510.IsStrict g.hom }

Existence (Theorem 6.9 applied to 𝒟 ≅ T(𝒟)). For any T-algebra B with a strict structure map, there is a strict homomorphism 𝒟 → B.

theorem Domain.Neighborhood.Theorem614.nonempty_algHom (s : Setup) (B : TAlgebra s.T) (hk : Exercise510.IsStrict B.str) : Nonempty (AlgHom (colimAlg s) B)

Existence (Theorem 6.9 applied to 𝒟 ≅ T(𝒟)). For any T-algebra B with a strict structure map, there is a homomorphism 𝒟 → B.

The projection chain ρₙ = iₙ ∘ jₙ and ⋃ₙ ρₙ = I_𝒟

def Domain.Neighborhood.Theorem614.rho (s : Setup) (n : ℕ) : ApproximableMap (colim s) (colim s)

ρₙ = iₙ ∘ jₙ : 𝒟 → 𝒟, the retraction onto Tⁿ({Γ}) (Proposition 6.12's projection pair for Tⁿ({Γ}) ◁ 𝒟).

Equations

• Domain.Neighborhood.Theorem614.rho s n = ⋯.inj.comp ⋯.proj

theorem Domain.Neighborhood.Theorem614.rho_rel (s : Setup) (n : ℕ) {X Y : Set s.Tok} : (rho s n).rel X Y ↔ (colim s).mem X ∧ (colim s).mem Y ∧ ∃ (z : Set s.Tok), (Dsys s n).mem z ∧ X ⊆ z ∧ z ⊆ Y

Scott's relational description X ρₙ Y ↔ ∃ z ∈ Tⁿ({Γ}), X ⊆ z ⊆ Y.

theorem Domain.Neighborhood.Theorem614.rho_mono (s : Setup) {n m : ℕ} (h : n ≤ m) {X Y : Set s.Tok} (hr : (rho s n).rel X Y) : (rho s m).rel X Y

ρₙ ⊆ ρₘ for n ≤ m (the projection chain is increasing).

def Domain.Neighborhood.Theorem614.iSupRho (s : Setup) : ApproximableMap (colim s) (colim s)

The pointwise union ⋃ₙ ρₙ (directed, since the chain is increasing).

Equations

• Domain.Neighborhood.Theorem614.iSupRho s = Domain.Neighborhood.ApproximableMap.iSupMap (Domain.Neighborhood.Theorem614.rho s) ⋯

theorem Domain.Neighborhood.Theorem614.iSupRho_eq_id (s : Setup) : iSupRho s = ApproximableMap.idMap (colim s)

⋃ₙ ρₙ = I_𝒟 (Scott's key identity for uniqueness). The forward inclusion uses X ⊆ z ⊆ Y ⟹ X ⊆ Y; the reverse factors the identity step X ⊆ X ⊆ Y through the level witnessing X ∈ 𝒟.

Theorem 6.14 — the existence half (the canonical solution and its

homomorphisms)

theorem Domain.Neighborhood.Theorem614.exists_algebra_with_hom (s : Setup) : ∃ (A : TAlgebra s.T), Nonempty (Iso (s.T.obj A.carrier) A.carrier) ∧ ∀ (B : TAlgebra s.T), Exercise510.IsStrict B.str → Nonempty (AlgHom A B)

Theorem 6.14 (Scott 1981, PRG-19) — the canonical fixed point. Under the hypotheses (continuous on maps, monotone and continuous on domains, with a generating set {Γ} ◁ T({Γ})), the iterated colimit 𝒟 = ⋃ₙ Tⁿ({Γ}) is a T-algebra whose structure map is an isomorphism T(𝒟) ≅ 𝒟 (the identity, since T(𝒟) = 𝒟), and there is a homomorphism from 𝒟 into every T-algebra with a strict structure map (Theorem 6.9). This is Scott's existence of the initial T-algebra.

Theorem 6.14 — the uniqueness half (T(ρₙ) = ρₙ₊₁, then g = ⋃ₙ g∘ρₙ)

Scott shows homomorphisms out of 𝒟 are unique by showing they are determined on the finite elements. Concretely, the projection chain ρₙ = iₙ ∘ jₙ satisfies T(ρₙ) = ρₙ₊₁ (because T is monotone on domains, so it carries the projection pair iₙ, jₙ to iₙ₊₁, jₙ₊₁) and ⋃ₙ ρₙ = I_𝒟. For any homomorphism g : 𝒟 → E, the sequence gₙ = g ∘ ρₙ is then independent of g: g₀ = ⊥ (because g is strict and ρ₀ = ⊥), and gₙ₊₁ = k ∘ T(gₙ) ∘ j by the homomorphism square; so g = ⋃ₙ gₙ is forced.

theorem Domain.Neighborhood.Theorem614.cat_comp_eq {X Y Z : DomainObj} (g : Category.Hom Y Z) (f : Category.Hom X Y) : g ⊚ f = ApproximableMap.comp g f

In the category of domains, ⊚ (categorical composition) is ApproximableMap.comp.

@[reducible, inline]

abbrev Domain.Neighborhood.Theorem614.objColim (s : Setup) : DomainObj

The colimit 𝒟 as a category object ⟨Tok, 𝒟⟩.

Equations

• Domain.Neighborhood.Theorem614.objColim s = { carrier := s.Tok, sys := Domain.Neighborhood.Theorem614.colim s }

@[reducible, inline]

abbrev Domain.Neighborhood.Theorem614.objDsys (s : Setup) (n : ℕ) : DomainObj

The n-th tower system Tⁿ({Γ}) as a category object ⟨Tok, Tⁿ({Γ})⟩.

Equations

• Domain.Neighborhood.Theorem614.objDsys s n = { carrier := s.Tok, sys := Domain.Neighborhood.Theorem614.Dsys s n }

@[reducible, inline]

abbrev Domain.Neighborhood.Theorem614.tmapRho (s : Setup) (n : ℕ) : ApproximableMap (s.T.obj (objColim s)).sys (s.T.obj (objColim s)).sys

T(ρₙ) as an endomorphism of T(𝒟), with the category objects pinned (they cannot be inferred from rho s n's ApproximableMap type alone).

Equations

• Domain.Neighborhood.Theorem614.tmapRho s n = s.T.map (Domain.Neighborhood.Theorem614.rho s n)

theorem Domain.Neighborhood.Theorem614.transport_heq {Obj : Type u_1} [Category Obj] {X Y : Obj} (e : X = Y) (f : Category.Hom X X) : e ▸ f ≍ f

Transport of a Hom X X along an object equality is heterogeneously equal to itself.

theorem Domain.Neighborhood.Theorem614.isoOfEq_conj {Obj : Type u_1} [Category Obj] {X Y : Obj} (e : X = Y) (f : Category.Hom X X) : (isoOfEq e).hom ⊚ f ⊚ (isoOfEq e).inv = e ▸ f

Conjugation by the identity isomorphism isoOfEq e is the object-transport along e.

theorem Domain.Neighborhood.Theorem614.map_comp_proj_heq {Tok Pc Qc : Type w} (cn : Pc = Tok) (cc : Qc = Tok) {Ps : NeighborhoodSystem Pc} {Qs : NeighborhoodSystem Qc} (ce : Qc = Pc) (sub : Ps ◁ ce ▸ Qs) {Dn1 Col : NeighborhoodSystem Tok} (hDn1 : cn ▸ Ps = Dn1) (hCol : cc ▸ Qs = Col) (hsub' : Dn1 ◁ Col) (Tmi : ApproximableMap Ps Qs) (Tmj : ApproximableMap Qs Ps) (hi : Tmi ≍ sub.inj) (hj : Tmj ≍ sub.proj) : Tmi.comp Tmj ≍ hsub'.inj.comp hsub'.proj

The carrier-transport core of T(ρₙ) = ρₙ₊₁. Given the monotone-on-domains data for a subsystem (its injection Tmi/projection Tmj are heterogeneously equal to the canonical 6.12 pair sub.inj/sub.proj of the image subsystem sub : Ps ◁ ce ▸ Qs), the composite Tmi ∘ Tmj is — after carrying the functor-image carriers Pc, Qc down to Tok — exactly the projection iₙ₊₁ ∘ jₙ₊₁ of the next subsystem hsub' : Dn1 ◁ Col. Proved by substing the carrier equalities, after which proof-irrelevance identifies the two subsystem proofs.

theorem Domain.Neighborhood.Theorem614.map_rho_heq (s : Setup) (n : ℕ) : tmapRho s n ≍ rho s (n + 1)

T(ρₙ) = ρₙ₊₁, heterogeneously. The image T(ρₙ) of the n-th projection, living over T(𝒟)'s carrier, is heterogeneously equal to the (n+1)-st projection ρₙ₊₁ over Tok.

theorem Domain.Neighborhood.Theorem614.key_rho (s : Setup) (n : ℕ) : rho s (n + 1) = (colimIso s).hom ⊚ tmapRho s n ⊚ (colimIso s).inv

ρₙ₊₁ = i ∘ T(ρₙ) ∘ j (Scott's T(ρₙ) = ρₙ₊₁, conjugated by the structure iso). Since the iso 𝒟 ≅ T(𝒟) is the identity, this is the carrier transport of T(ρₙ); combined with map_rho_heq it pins ρₙ₊₁.

The g-independent fixed-point recursion

theorem Domain.Neighborhood.Theorem614.strict_rel_master {β₀ β₁ : Type w} {V₀ : NeighborhoodSystem β₀} {V₁ : NeighborhoodSystem β₁} {g : ApproximableMap V₀ V₁} (hg : Exercise510.IsStrict g) {Z : Set β₁} : g.rel V₀.master Z ↔ Z = V₁.master

For a strict map g, g(⊥) = ⊥ relationally: g sends Δ only to Δ.

@[simp]

theorem Domain.Neighborhood.Theorem614.Dsys_zero (s : Setup) : Dsys s 0 = s.Γ

Dsys s 0 = Γ (the base of the tower).

theorem Domain.Neighborhood.Theorem614.rho_zero_rel (s : Setup) (hΓ : ∀ (X : Set s.Tok), s.Γ.mem X → X = s.Γ.master) {X Y : Set s.Tok} : (rho s 0).rel X Y ↔ (colim s).mem X ∧ Y = (colim s).master

ρ₀ = ⊥ when {Γ} is the trivial one-point system: ρ₀ relates X only to the master. This is where Scott's {Γ} (a one-point domain) is used.

theorem Domain.Neighborhood.Theorem614.gcomp_rho_zero_rel (s : Setup) (hΓ : ∀ (X : Set s.Tok), s.Γ.mem X → X = s.Γ.master) (B : TAlgebra s.T) {g : ApproximableMap (colim s) B.carrier.sys} (hg : Exercise510.IsStrict g) {X : Set s.Tok} {Z : Set B.carrier.carrier} : (g.comp (rho s 0)).rel X Z ↔ (colim s).mem X ∧ Z = B.carrier.sys.master

For a strict homomorphism g, the base g ∘ ρ₀ is the least map: it relates X only to the master of E, independent of g.

theorem Domain.Neighborhood.Theorem614.gcomp_rho_zero_indep (s : Setup) (hΓ : ∀ (X : Set s.Tok), s.Γ.mem X → X = s.Γ.master) (B : TAlgebra s.T) {g g' : ApproximableMap (colim s) B.carrier.sys} (hg : Exercise510.IsStrict g) (hg' : Exercise510.IsStrict g') : g.comp (rho s 0) = g'.comp (rho s 0)

The base case of g-independence: any two strict maps agree after ∘ ρ₀.

theorem Domain.Neighborhood.Theorem614.gcomp_rho_succ (s : Setup) (B : TAlgebra s.T) (g : AlgHom (colimAlg s) B) (n : ℕ) : ApproximableMap.comp g.hom (rho s (n + 1)) = ApproximableMap.comp B.str (ApproximableMap.comp (s.T.map (ApproximableMap.comp g.hom (rho s n))) (colimIso s).inv)

The fixed-point recursion gₙ₊₁ = k ∘ T(gₙ) ∘ j. Using key_rho (ρₙ₊₁ = i∘T(ρₙ)∘j) and the homomorphism square g ∘ i = k ∘ T(g).

theorem Domain.Neighborhood.Theorem614.gcomp_rho_indep (s : Setup) (hΓ : ∀ (X : Set s.Tok), s.Γ.mem X → X = s.Γ.master) (B : TAlgebra s.T) (g g' : AlgHom (colimAlg s) B) (hg : Exercise510.IsStrict g.hom) (hg' : Exercise510.IsStrict g'.hom) (n : ℕ) : ApproximableMap.comp g.hom (rho s n) = ApproximableMap.comp g'.hom (rho s n)

g-independence of gₙ = g ∘ ρₙ. For any two strict homomorphisms into the same algebra, g ∘ ρₙ = g' ∘ ρₙ for all n — the sequence is determined by the recursion, not by g.

Uniqueness and initiality (among strict algebras)

theorem Domain.Neighborhood.Theorem614.algHom_ext {Obj : Type u_1} [Category Obj] {T : Endofunctor Obj} {A B : TAlgebra T} {g g' : AlgHom A B} (h : g.hom = g'.hom) : g = g'

Two algebra homomorphisms with equal underlying maps are equal (the commuting square is a Prop).

theorem Domain.Neighborhood.Theorem614.gcomp_eq (s : Setup) (hΓ : ∀ (X : Set s.Tok), s.Γ.mem X → X = s.Γ.master) (B : TAlgebra s.T) (g g' : AlgHom (colimAlg s) B) (hg : Exercise510.IsStrict g.hom) (hg' : Exercise510.IsStrict g'.hom) : g.hom = g'.hom

The underlying maps of two strict homomorphisms coincide: g = g ∘ I = g ∘ ⋃ₙ ρₙ = ⋃ₙ (g ∘ ρₙ), and the latter is g-independent.

theorem Domain.Neighborhood.Theorem614.algHom_unique (s : Setup) (hΓ : ∀ (X : Set s.Tok), s.Γ.mem X → X = s.Γ.master) (B : TAlgebra s.T) (g g' : AlgHom (colimAlg s) B) (hg : Exercise510.IsStrict g.hom) (hg' : Exercise510.IsStrict g'.hom) : g = g'

Uniqueness of strict homomorphisms out of 𝒟. Any two strict T-algebra homomorphisms from the canonical solution into the same algebra are equal.

theorem Domain.Neighborhood.Theorem614.exists_unique_strict_algHom (s : Setup) (hΓ : ∀ (X : Set s.Tok), s.Γ.mem X → X = s.Γ.master) (B : TAlgebra s.T) (hk : Exercise510.IsStrict B.str) : ∃ (g : AlgHom (colimAlg s) B), Exercise510.IsStrict g.hom ∧ ∀ (g' : AlgHom (colimAlg s) B), Exercise510.IsStrict g'.hom → g' = g

Theorem 6.14 (Scott 1981, PRG-19) — initial T-algebra. When {Γ} is the one-point generating system, the canonical solution 𝒟 = ⋃ₙ Tⁿ({Γ}) is the initial T-algebra among the strict algebras: for every T-algebra B with a strict structure map there is a unique strict homomorphism 𝒟 → B. (Existence is Theorem 6.9; uniqueness is the ρₙ projection-chain argument.)