Free objects

(1)

Adjunctions

(2)

Recall:

Term algebras

Theorem: For any S-sorted set X of variables, Σ-algebra A and valuation

v : X → |A|, there is a unique Σ-homomorphism v^# : T_Σ(X) → A that extends v, so that

id_{X ,→|T}_Σ_{(X )|};v^# = v

X |T_Σ(X)|

|A|

T_Σ(X)

A -

HH

HH H

j ? ?

id_{X ,→|T}_Σ_{(X )|}

v |v^#| ∃! v^#

Set^S Alg(Σ)

(3)

Free objects

Consider any functor G : K⁰ → K

Definition: Given an object A ∈ |K|, a free object over A w.r.t. G is a K⁰-object A⁰ ∈ |K⁰| together with a K-morphism η_A: A → G(A⁰) (called unit morphism) such that given any K⁰-object B⁰ ∈ |K⁰| with K-morphism f : A → G(B⁰), for a unique K⁰-morphism f^#: A⁰ → B⁰ we have

η_A;G(f^#) = f

Paradigmatic example:

Term algebra T_Σ(X) with unit id_{X ,→|T}_Σ_{(X )|}: X → |T_Σ(X)| is free over X ∈ |Set^S| w.r.t. the carrier functor | | : Alg(Σ) → Set^S

G

K K⁰

A η_A - G(A⁰) A⁰

B⁰ G(B⁰)

H

HH

HHj f

? ?

∃! f^# G(f^#)

(4)

Free objects

η_A;G(f^#) = f

G

K K⁰

A η_A - G(A⁰) A⁰

B⁰ G(B⁰)

H

HH

HHj f

? ?

∃! f^# G(f^#)

(5)

Free objects

η_A;G(f^#) = f

G

K K⁰

A η_A - G(A⁰) A⁰

B⁰ G(B⁰)

H

HH

HHj f

? ?

∃! f^# G(f^#)

(6)

Free objects

η_A;G(f^#) = f

G

K K⁰

A η_A - G(A⁰) A⁰

B⁰ G(B⁰)

H

HH

HHj f

? ?

∃! f^# G(f^#)

(7)

Free objects

η_A;G(f^#) = f

G

K K⁰

A η_A - G(A⁰) A⁰

B⁰ G(B⁰)

H

HH

HHj f

? ?

∃! f^# G(f^#)

(8)

Free objects

η_A;G(f^#) = f

G

K K⁰

A η_A - G(A⁰) A⁰

B⁰ G(B⁰)

H

HH

HHj f

? ?

∃! f^# G(f^#)

(9)

Free objects

η_A;G(f^#) = f

G

K K⁰

A η_A - G(A⁰) A⁰

B⁰ G(B⁰)

H

HH

HHj f

? ?

∃! f^# G(f^#)

(10)

Examples

• Consider inclusion i : Int ,→ Real, viewing Int and Real as (thin) categories, and i as a functor between them. For any real r ∈ Real, the ceiling of r,

dre ∈ Int is free over r w.r.t. i.

(11)

Examples

i

Real Int

r ≤ - dre dre

k k

H

HH

HHHj

≤

? ?

≤

(12)

Examples

i

Real Int

r ≤ - dre dre

k k

H

HH

HHHj

≤

? ?

≤

(13)

Examples

i

Real Int

r ≤ - dre dre

k k

H

HH

HHHj

≤

? ?

≤

(14)

Examples

i

Real Int

r ≤ - dre dre

k k

H

HH

HHHj

≤

? ?

≤

(15)

Examples

What about free objects w.r.t. the inclusion of rationals into reals?

(16)

Examples

• For any set X ∈ |Set|, the “free monoid” List(X) = hX∗, b, i is free over X w.r.t. | | : Monoid → Set.

Set | | Monoid

X - X∗ hX∗, b , i

sing_X

hM, ;, ei M

H

HH

HHHj f

? ?

f^# f^#

(17)

Examples

Set | | Monoid

X - X∗ hX∗, b, i

sing_X

hM, ;, ei M

H

HH

HHHj f

? ?

f^# f^#

(18)

Examples

Set | | Monoid

X - X∗ hX∗, b, i

sing_X

hM, ;, ei M

H

HH

HHHj f

? ?

f^# f^#

(19)

Examples

Set | | Monoid

X - X∗ hX∗, b, i

sing_X

hM, ;, ei M

H

HH

HHHj f

? ?

f^# f^#

(20)

Examples

• For any graph G ∈ |Graph|, the category of its paths, Path(G) ∈ |Cat|, is free over G w.r.t. the graph functor G : Cat → Graph.

(21)

Examples

G

Graph Cat

G - G(Path(G)) Path(G)

G(K) K HH

HH

HH H j h

? ?

h^# h^#

(22)

Examples

G

Graph Cat

G(K) K HH

HH

HH H j h

? ?

h^# h^#

(23)

Examples

G

Graph Cat

G(K) K HH

HH

HH H j h

? ?

h^# h^#

(24)

Examples

G

Graph Cat

G(K) K HH

HH

HH H j h

? ?

h^# h^#

(25)

Examples

• Discrete topologies, completion of metric spaces, free groups, ideal completion of partial orders, ideal completion of free partial algebras, . . .

Makes precise these and other similar examples Indicate unit morphisms!

(26)

Examples

• Discrete topologies, completion of metric spaces, free groups, ideal completion of partial orders, ideal completion of free partial algebras, . . .

Makes precise these and other similar examples Indicate unit morphisms!

(27)

Free equational models

• Recall: for any algebraic signature Σ = hS, Ωi, term algebra T_Σ(X) is free over X ∈ |Set^S| w.r.t. the carrier functor | | : Alg(Σ) → Set^S.

(28)

Free equational models

(29)

Free equational models

| |

Set^S Alg(Σ)

X - |T_Σ(X)| T_Σ(X)

id_{X ,→|T}_Σ_{(X )|}

|B| B H

HH

HHj f

? ?

f^# f^#

(30)

Free equational models

• For any set of Σ-equations Φ, for any set X ∈ |Set^S|, there exist a model F^Φ(X) ∈ Mod (Φ) that is free over X w.r.t. the carrier functor

| | : Mod(hΣ, Φi) → Set^S, where Mod(hΣ, Φi) is the full subcategory of Alg(Σ) given by the models of Φ.

(31)

Free equational models

| | : Mod(hΣ, Φi) → Set^S, where Mod(hΣ, Φi) is the full subcategory of

Alg(Σ) given by the models of Φ. Recall: F^Φ(X) is T_Σ(X)/≡, where ≡ is the congruence on T_Σ(X) such that t₁ ≡ t₂ iff Φ |= ∀X.t₁ = t₂.

| |

Set^S Mod(hΣ, Φi)

X - |F^Φ(X)| F^Φ(X)

[ ]_≡

|B| B H

HH

HHj f

? ?

f^# f^#

(32)

Free equational models

| | : Mod(hΣ, Φi) → Set^S, where Mod(hΣ, Φi) is the full subcategory of

Alg(Σ) given by the models of Φ. Recall: F^Φ(X) is T_Σ(X)/≡, where ≡ is the congruence on T_Σ(X) such that t₁ ≡ t₂ iff Φ |= ∀X.t₁ = t₂.

| |

Set^S Mod(hΣ, Φi)

X - |F^Φ(X)| F^Φ(X)

[ ]_≡

|B| B H

HH

HHj f

? ?

f^# f^#

(33)

Free equational models

• For any algebraic signature morphism σ : Σ → Σ⁰, for any Σ-algebra

A ∈ |Alg(Σ)|, there exist a Σ⁰-algebra F_σ(A) ∈ |Alg(Σ⁰)| that is free over A w.r.t. the reduct functor _σ : Alg(Σ⁰) → Alg(Σ).

• For any equational specification morphism σ : hΣ, Φi → hΣ⁰, Φ⁰i, for any model A ∈ Mod (Φ), there exist a model F^Φ_σ⁰(A) ∈ Mod (Φ⁰) that is free over A w.r.t.

the reduct functor _σ : Mod(hΣ⁰, Φ⁰i) → Mod(hΣ, Φi).

Prove the above.

(34)

Fact: For any algebraic signature inclusion σ : Σ ,→ Σ , for any Σ-algebra A ∈ |Alg(Σ)|, there exist a Σ⁰-algebra F_σ(A) ∈ |Alg(Σ⁰)| that is free over A w.r.t. the reduct functor _σ : Alg(Σ⁰) → Alg(Σ).

Proof (idea): Define F_σ(A) to be T_Σ⁰(|A|)/≡ with unit [ ]_≡: A → (T_Σ⁰(|A|)/≡) _σ, where ≡ is the least congruence on T_Σ⁰(|A|) such that for f : s₁ × . . . ×_n → s in Σ and a₁ ∈ |A|_s₁,. . . ,a_n ∈ |A|_s₁, f_A(a₁, . . . , a_n) ≡ f (a₁, . . . , a_n)

Alg(Σ) σ Alg(Σ⁰)

A T_Σ⁰(|A|)

[ ]_≡ T_Σ⁰(|A|)/≡

(T_Σ⁰(|A|)/≡) _σ -

[ ]_≡

( )_B⁰[h]

B⁰ B⁰ _σ

H

HH

HHj h

? ?

h^# h^# _σ

(35)

A T_Σ⁰(|A|)

[ ]_≡ T_Σ⁰(|A|)/≡

(T_Σ⁰(|A|)/≡) _σ -

[ ]_≡

( )_B⁰[h]

B⁰ B⁰ _σ

H

HH

HHj h

? ?

h^# h^# _σ

(36)

A T_Σ⁰(|A|)

[ ]_≡ T_Σ⁰(|A|)/≡

(T_Σ⁰(|A|)/≡) _σ -

[ ]_≡

( )_B⁰[h]

B⁰ B⁰ _σ

H

HH

HHj h

? ?

h^# h^# _σ

(37)

• [ ]_≡: A → (T_Σ⁰(|A|)/≡) _σ is indeed a Σ-homomorphism, since [f_A(a₁, . . . , a_n)]_≡ = [f (a₁, . . . , a_n)]_≡ = f_T

Σ0(|A|)/≡([a₁]_≡, . . . , [a_n]_≡)

A T_Σ⁰(|A|)

[ ]_≡ T_Σ⁰(|A|)/≡

(T_Σ⁰(|A|)/≡) _σ -

[ ]_≡

( )_B⁰[h]

B⁰ B⁰ _σ

H

HH

HHj h

? ?

h^# h^# _σ

(38)

• for B⁰ ∈ |Alg(Σ⁰)| and h : A → B⁰ _σ, consider ( )_B⁰[h] : T_Σ⁰(|A|) → B⁰. Then ≡ ⊆ K(( )_B⁰[h]),

A T_Σ⁰(|A|)

[ ]_≡ T_Σ⁰(|A|)/≡

(T_Σ⁰(|A|)/≡) _σ -

[ ]_≡

( )_B⁰[h]

B⁰ B⁰ _σ

H

HH

HHj h

? ?

h^# h^# _σ

(39)

A T_Σ⁰(|A|)

[ ]_≡ T_Σ⁰(|A|)/≡

(T_Σ⁰(|A|)/≡) _σ -

[ ]_≡

( )_B⁰[h]

B⁰ B⁰ _σ

H

HH

HHj h

? ?

h^# h^# _σ

(40)

A T_Σ⁰(|A|)

[ ]_≡ T_Σ⁰(|A|)/≡

(T_Σ⁰(|A|)/≡) _σ -

[ ]_≡

( )_B⁰[h]

B⁰ B⁰ _σ

H

HH

HHj h

? ?

h^# h^# _σ

(41)

• for B⁰ ∈ |Alg(Σ⁰)| and h : A → B⁰ _σ, consider ( )_B⁰[h] : T_Σ⁰(|A|) → B⁰. Then ≡ ⊆ K(( )_B⁰[h]), since:

h_s(f_A(a₁, . . . , a_n)) = f_B⁰(h_s₁(a₁), . . . , h_s_n(a_n)) = (f (a₁, . . . , a_n))_B⁰[h]

A T_Σ⁰(|A|)

[ ]_≡ T_Σ⁰(|A|)/≡

(T_Σ⁰(|A|)/≡) _σ -

[ ]_≡

( )_B⁰[h]

B⁰ B⁰ _σ

H

HH

HHj h

? ?

h^# h^# _σ

(42)

• for B⁰ ∈ |Alg(Σ⁰)| and h : A → B⁰ _σ, consider ( )_B⁰[h] : T_Σ⁰(|A|) → B⁰. Then ≡ ⊆ K(( )_B⁰[h]), and so there is unique Σ⁰-homomorphism

h^#: (T_Σ⁰(|A|)/≡) → B⁰ such that [ ]_≡;h^# = ( )_B⁰[h].

A T_Σ⁰(|A|)

[ ]_≡ T_Σ⁰(|A|)/≡

(T_Σ⁰(|A|)/≡) _σ -

[ ]_≡

( )_B⁰[h]

B⁰ B⁰ _σ

H

HH

HHj h

? ?

h^# h^# _σ

(43)

Free equational models

• For any algebraic signature morphism σ : Σ → Σ⁰, for any Σ-algebra

A ∈ |Alg(Σ)|, there exist a Σ⁰-algebra F_σ(A) ∈ |Alg(Σ⁰)| that is free over A w.r.t. the reduct functor _σ : Alg(Σ⁰) → Alg(Σ).

• For any equational specification morphism σ : hΣ, Φi → hΣ⁰, Φ⁰i, for any model A ∈ Mod (Φ), there exist a model F^Φ_σ⁰(A) ∈ Mod (Φ⁰) that is free over A w.r.t.

the reduct functor _σ : Mod(hΣ⁰, Φ⁰i) → Mod(hΣ, Φi).

Prove the above.

(44)

Fact: For any algebraic signature morphism σ : Σ → Σ and set Φ of Σ -equations, for any Σ-algebra A ∈ |Alg(Σ)|, there exist a Σ⁰-algebra F^Φ_σ⁰(A) ∈ Mod (Φ⁰) that is free over A w.r.t. the reduct functor _σ : Mod(hΣ⁰, Φ⁰i) → Alg(Σ).

Proof (idea): Define F^Φ_σ⁰(A) to be T_Σ⁰(X⁰)/≡ with unit [ ]_≡: A → (T_Σ⁰(X⁰)/≡) _σ, where X_s⁰0 = U

σ(s)=s⁰ |A|_s and ≡ is the least congruence on T_Σ⁰(X⁰) such that t₁ ≡ t₂ when Φ⁰ |= ∀X⁰.t₁ = t₂ as well as for f : s₁ × . . . ×_n → s in Σ and

a₁ ∈ |A|_s₁,. . . ,a_n ∈ |A|_s₁, f_A(a₁, . . . , a_n) ≡ σ(f )(a₁, . . . , a_n)

Alg(Σ) σ Mod(hΣ⁰, Φ⁰i) ⊆ Alg(Σ⁰)

A T_Σ⁰(X⁰)

[ ]≡

T_Σ⁰(X⁰)/≡

(T_Σ⁰(X⁰)/≡) _σ -

[ ]≡

( )_B⁰[h⁰] B⁰

B⁰ _σ HH

HH

HH H j h

? ?

h^# h^# _σ

(45)

A T_Σ⁰(X⁰)

[ ]≡

T_Σ⁰(X⁰)/≡

(T_Σ⁰(X⁰)/≡) _σ -

[ ]≡

( )_B⁰[h⁰] B⁰

B⁰ _σ HH

HH

HH H j h

? ?

h^# h^# _σ

(46)

A T_Σ⁰(X⁰)

[ ]≡

T_Σ⁰(X⁰)/≡

(T_Σ⁰(X⁰)/≡) _σ -

[ ]≡

( )_B⁰[h⁰] B⁰

B⁰ _σ HH

HH

HH H j h

? ?

h^# h^# _σ

(47)

A T_Σ⁰(X⁰)

[ ]≡

T_Σ⁰(X⁰)/≡

(T_Σ⁰(X⁰)/≡) _σ -

[ ]≡

( )_B⁰[h⁰] B⁰

B⁰ _σ HH

HH

HH H j h

? ?

h^# h^# _σ

(48)

A T_Σ⁰(X⁰)

[ ]≡

T_Σ⁰(X⁰)/≡

(T_Σ⁰(X⁰)/≡) _σ -

[ ]≡

( )_B⁰[h⁰] B⁰

B⁰ _σ HH

HH

HH H j h

? ?

h^# h^# _σ

(49)

• T_Σ⁰(|A|)/≡ |= Φ⁰, i.e. indeed T_Σ⁰(|A|)/≡ ∈ Mod (Φ⁰)

A T_Σ⁰(X⁰)

[ ]≡

T_Σ⁰(X⁰)/≡

(T_Σ⁰(X⁰)/≡) _σ -

[ ]≡

( )_B⁰[h⁰] B⁰

B⁰ _σ HH

HH

HH H j h

? ?

h^# h^# _σ

(50)

• [ ]_≡: A → (T_Σ⁰(|A|)/≡) _σ is indeed a Σ-homomorphism, since [f_A(a₁, . . . , a_n)]_≡ = [σ(f )(a₁, . . . , a_n)]_≡ = f_(T

Σ0(X⁰)/≡) _σ([a₁]_≡, . . . , [a_n]_≡)

A T_Σ⁰(X⁰)

[ ]_≡ T_Σ⁰(X⁰)/≡

(T_Σ⁰(X⁰)/≡) _σ -

[ ]_≡

( )_B⁰[h⁰] B⁰

B⁰ _σ H

HH

HHj h

? ?

h^# h^# _σ

(51)

• for B⁰ ∈ |Mod(hΣ⁰, Φ⁰i)| and h : A → B⁰ _σ, ≡ ⊆ K(( )_B⁰[h⁰]) (h⁰: X⁰ → |B⁰| is as h),

A T_Σ⁰(X⁰)

[ ]_≡ T_Σ⁰(X⁰)/≡

(T_Σ⁰(X⁰)/≡) _σ -

[ ]_≡

( )_B⁰[h⁰] B⁰

B⁰ _σ HH

HH

HH H j h

? ?

h^# h^# _σ