Lecture VI — Proposition 6.6 (Scott 1981, PRG-19): initial algebras are uniquely

isomorphic

Proposition 6.6. Any two initial T-algebras are uniquely isomorphic.

The proof is the standard diagram chase. If A and B are both initial, initiality gives unique homomorphisms f : A → B and g : B → A. Their composites g ∘ f : A → A and f ∘ g : B → B are homomorphisms, and by uniqueness of homomorphisms out of an initial algebra they must equal the identity homomorphisms. Hence the underlying morphisms of f and g are mutually inverse, giving an isomorphism A.carrier ≅ B.carrier. The isomorphism is unique in that the homomorphism A → B realising it is the only one (iso_hom_unique).

Choice-free (#print axioms ⊆ {propext, Quot.sound}).

theorem Domain.Neighborhood.comp_desc_eq_id {Obj : Type u} [Category Obj] {T : Endofunctor Obj} {A B : TAlgebra T} (hA : IsInitial A) (hB : IsInitial B) : (hB.desc A).comp (hA.desc B) = AlgHom.id A

Composing the two unique homomorphisms A → B → A gives the identity homomorphism on the initial algebra A.

def Domain.Neighborhood.initialIso {Obj : Type u} [Category Obj] {T : Endofunctor Obj} {A B : TAlgebra T} (hA : IsInitial A) (hB : IsInitial B) : Iso A.carrier B.carrier

Proposition 6.6 (Scott 1981, PRG-19). Any two initial T-algebras have isomorphic carriers; the isomorphism is built from the unique homomorphisms in both directions.

Equations

• Domain.Neighborhood.initialIso hA hB = { hom := (hA.desc B).hom, inv := (hB.desc A).hom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

theorem Domain.Neighborhood.iso_hom_unique {Obj : Type u} [Category Obj] {T : Endofunctor Obj} {A B : TAlgebra T} (hA : IsInitial A) (h : AlgHom A B) : h = hA.desc B

The isomorphism of Proposition 6.6 is unique: the homomorphism A → B realising it is the only homomorphism between the two initial algebras.