Lecture VI — Proposition 6.7 (Scott 1981, PRG-19): Lambek's lemma

Proposition 6.7. If i : T(D) → D is an initial T-algebra, then so is T(i) : T²(D) → T(D) and i is the isomorphism from T(D) to D.

We formalise the second (and decisive) half: the structure map of an initial algebra is an isomorphism. Writing A = (D, i), the functor turns i into a new algebra (T(D), T(i)) (tStr), and i itself is a homomorphism (T(D), T(i)) → (D, i) (strHom). Initiality supplies a homomorphism j : (D,i) → (T(D),T(i)), and the composite i ∘ j : (D,i) → (D,i) must be the identity (str_comp_desc). Functoriality then gives T(i) ∘ T(j) = T(i ∘ j) = I, and the homomorphism square for j yields j ∘ i = I. Hence i and j are mutually inverse: i is an isomorphism (lambek).

This is exactly Scott's remark that "if we are going to have initial algebras at all we have to satisfy the domain equation D ≅ T(D)".

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

def Domain.Neighborhood.tStr {Obj : Type u} [Category Obj] {T : Endofunctor Obj} (A : TAlgebra T) : TAlgebra T

For an algebra A = (D, i), the functor turns the structure map into a new T-algebra (T(D), T(i)).

Equations

• Domain.Neighborhood.tStr A = { carrier := T.obj A.carrier, str := T.map A.str }

def Domain.Neighborhood.strHom {Obj : Type u} [Category Obj] {T : Endofunctor Obj} (A : TAlgebra T) : AlgHom (tStr A) A

The structure map i : T(D) → D is itself a homomorphism (T(D), T(i)) → (D, i): the square i ∘ T(i) = i ∘ T(i) commutes trivially.

Equations

• Domain.Neighborhood.strHom A = { hom := A.str, comm := ⋯ }

theorem Domain.Neighborhood.str_comp_desc {Obj : Type u} [Category Obj] {T : Endofunctor Obj} (A : TAlgebra T) (hA : IsInitial A) : A.str ⊚ (hA.desc (tStr A)).hom = Category.id A.carrier

The composite i ∘ j of i with the descent homomorphism j : (D,i) → (T(D),T(i)) is the identity on D.

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

Proposition 6.7 (Lambek's lemma; Scott 1981, PRG-19). The structure map i : T(D) → D of an initial T-algebra is an isomorphism T(D) ≅ D, with inverse the descent homomorphism j.

Equations

• Domain.Neighborhood.lambek A hA = { hom := A.str, inv := (hA.desc (Domain.Neighborhood.tStr A)).hom, hom_inv_id := ⋯, inv_hom_id := ⋯ }