Category Theory Background - and Introduction to Coalgebra

Category Theory Background and Introduction to Coalgebra MATHLOGAPS 2008: Coalgebra and Circularity

August 2008

MATHLOGAPS 2008: Coalgebra and Circularity

Category Theory Background

My goals for this part of the course

At this point, we have seen examples of circularly-defined sets such as the set of streams the set of infinite trees One of the main goals of the course is to present a theory of how these “solution spaces” work. The theory is based on the concept of a coalgebra for a functor and on similar notions from category theory. This part of the course is a quick introduction to a few of the concepts which we’ll need. It is not a systematic presentation of the subject.



Categories A category C consists of 1

objects c, d, . . .

2

morphisms f , g , . . .. Each morphism has a domain and codomain. f : c → d means that c is the domain of f , and d is the codomain.

3

identity morphisms id a for all objects.

4

a composition operation: if f : a → b and g : b → c, then g · f : a → c.

subject to the requirements that Composition is associative. If f : a → b, then id b · f = f = f · id a .



Examples of Categories

We continue with several examples of categories including the category Set of sets. the category CMS of complete metric spaces. Of course, we’ll see constructions of “new categories from old” at several places as well.



The category Set

The objects of Set are the sets, and the morphisms are triples hx, y , f i where f : x → y . The domain of hx, y , f i is x, and the codomain is y . The identity morphism id a for a set a is ha, a, f i, where f is the identity function on a. The composition operation of morphisms is given by: hy , z, g i · hx, y , f i = hx, z, g · f i



The category Set

The objects of Set are the sets, and the morphisms are triples hx, y , f i where f : x → y . The domain of hx, y , f i is x, and the codomain is y . The identity morphism id a for a set a is ha, a, f i, where f is the identity function on a. The composition operation of morphisms is given by: hy , z, g i · hx, y , f i = hx, z, g · f i An alternative presentation of the category of sets would take as morphism the pairs hy , f i with y ⊇ {a : (∃b)hb, ai ∈ f }.



The category CMS

This is the category of complete metric spaces, with distances measured in [0, 1], and with non-expanding functions as morphisms: d(x, y ) ≥ d(fx, fy ). One reason for the use of [0, 1] is that this way the homsets CMS(X , Y )

=

{f : f is a continuous function from X to Y }

are again objects in the category, with d(f , g )

=

sup dY (f (x), g (x)). x∈X



Functors

Let C and D be categories. A functor from C to D consists of An object mapping a 7→ Fa, taking objects of C to objects of D. A morphism mapping f 7→ Ff , taking morphisms of C to morphisms of D. such that If f : a → b, then Ff : Fa → Fb. F id a = id Fa . F (f · g ) = Ff · Fg . A functor from C to itself is an endofunctor.



The easiest examples

Let d be an object of D. We get F : C → D, the constant functor d by: Fc = d, Ff = id d .

The composition of functors is again a functor.



Endofunctors on Set related to our examples of systems Let A be a fixed set. Then we get a functor Fy = A × y by using the cartesian product for the object part, and if f : y → z, then Ff : A × y → A × z is given by Ff (ha, xi)

=

ha, fxi.

Another way to say this: Ff (w )

=

hfst(w ), f (snd(w )i.

I’ll omit the verification that this actually is a functor.



Stream systems and their solutions Let FX = N × X . Stream systems are coalgebras of F , maps of the form e : X → FX . Even more, the solution e † : X → N ∞ would be a coalgebra morphism: X e†

e

N∞

/ FX

id

Fe †

/ FN ∞

The point is that for x ∈ X , Fe † (e(x)) = Fe † hfst(e(x)), snd(e(x))i = hfst(e(x)), e † (snd(e(x)))i We have seen this formulation before.



The power set endofunctor P

For any set X , PX is the set of subsets of X . P extends to an endofunctor, taking f :X →Y to Pf : PX → PY given by direct images: for a ⊆ X , Pf (a) = f [a] = {f (x) : x ∈ a}. We similarly have functors such as the finite power set functor Pfin .



Set systems and their solutions Let FX = PX . Set systems are coalgebras of F , maps of the form e : X → PX . Even more, the solution e † : X → V is practically a coalgebra morphism: e

X e†

V

/ PX

id

Pe †

/ PV

The point is that for x ∈ X , Pe † (e(x)) = e † [e(x)] = {e † (a) : a ∈ e(x)} So e † satisfies the equation we saw before.



Signature Functors

A signature is set Σ of function symbols with arities. Each Σ gives us HΣ : Set → Set by HΣ (X ) for g : X → Y HΣ g (hf , x1 , . . . , xn i)

=

{hf , x1 , . . . , xn i : arity (f ) = n; x ∈ X }

=

hf , g (x1 ), . . . , g (xn )i

So HΣ (X ) is like the one-level trees, allowing elements of X to appear on the leaves.



Signature Functors

A signature is set Σ of function symbols with arities. Each Σ gives us HΣ : Set → Set by HΣ (X ) for g : X → Y HΣ g (hf , x1 , . . . , xn i)

=


=

hf , g (x1 ), . . . , g (xn )i

Example: Σ has a binary symbol ◦ and a 0-ary e. HΣ ({x, y }) = {hei, h◦, x, xi, h◦, x, y i, h◦, y , xi, h◦, y , y i}.



Signature Functors A signature is set Σ of function symbols with arities. Each Σ gives us HΣ : Set → Set by HΣ (X ) for g : X → Y HΣ g (hf , x1 , . . . , xn i)

=


=

hf , g (x1 ), . . . , g (xn )i

The point is that now tree systems and solutions are represented: X e†

e

Tr Σ

/ HΣ X

id


HΣ e †

/ H Σ (Tr Σ )


The discrete measure functor D

A discrete measure on a set A is a function µ : A → [0, 1] such that 1 2

µ has finite support: {a ∈ A | µ(a) > 0} is finite. P a∈A µ(a) = 1.

D(A) is the set of discrete measures on A. We make D into a functor by setting, for f : P A → B, Df (µ)(b) = µ(f −1 (b)); this is {µ(a) : f (a) = b}. (This extends discrete measures on A to functions on P(A) by summing.)



Functions from a fixed set

Let A be a set, and write X A for the functions from A to X . Let F be defined by FX = X A , and for f : X → Y , Ff : X A → Y A is ?? .



Coproducts Let C be a category. A coproduct of objects x and y , is an object x + y with morphisms inl : x → x + y and inr : y → x + y meeting the following condition: if f : x → z and g : y → z, then there is a unique [f , g ] : x + y → z such that [f , g ] · inl = f and [f , g ] · inr = g . x inl

f

[f ,g ] $ x +O y _ _ _ _ _ _ _ _ _ _ _:/ z inr

y


g


Coproducts Let C be a category. A coproduct of objects x and y , is an object x + y with morphisms inl : x → x + y and inr : y → x + y meeting the following condition: if f : x → z and g : y → z, then there is a unique [f , g ] : x + y → z such that [f , g ] · inl = f and [f , g ] · inr = g . Technically, the coproduct of x and y is the triple (x + y , inl, inr). Usually there’s no need to add the names of the objects to the coproduct maps inl and inr. But if we would need to, we could write inla,a+b : a → a + b, and similarly for inrb,a+b .



Using coproducts If f : a → b and g : c → d, then we have f +g :a+c →b+d given by f + g = [inl · f , inr · g ]. In pictures, a

f

a+b

b

g

/c N NNN NNinl NNN NNN ' [inl·f ,inr·g ] /c +d 8 ppp p p ppp ppp inr p /d



Categories with coproducts

C has coproducts if every two objects have a coproduct. A category with coproducts is a tuple (C , +), where C is a category and + is a coproduct operation on C , giving for each x and y the triple (x + y , inlx,x+y , inry ,x+y ). E.g., (Set, +), where x +y

=

(x × {0}) ∪ (y × {1}),

also, inl(a) = (a, 0) for a ∈ x, and inr(b) = (b, 1) for b ∈ y .



Coproducts of functors

Let C be a category and (D, +) be a category with coproducts. If F : C → D and G : C → D, we define F +G :C →D by (F + G )a = Fa + Ga, and if f : a → b, then (F + G )f : Fa + Ga → Fb + Gb is given by (F + G )f


=

Ff + Gf


Initial and Final Objects

In a category C , an object c is called initial if for every object a, there is a unique ! : c → a.




In a category C , an object c is called initial if for every object a, there is a unique ! : c → a. In Set, ∅ is initial. For every a, the empty function is the unique function from ∅ to a.




In a category C , an object c is called initial if for every object a, there is a unique ! : c → a.

c is terminal, or final if for every object a, there is a unique ! : a → c. In Set, the final objects are exactly the singletons.



Algebras for a Functor

Let F : C → C be a functor. An algebra for F is a pair (A, a), where a : FA → A in C . The leading example is when F is a signature functor, say FΣ . Then an F -algebra is a set A together with interpretations of the symbols in Σ.



Algebras for a Functor Let F : C → C be a functor. An algebra for F is a pair (A, a), where a : FA → A in C . The leading example is when F is a signature functor, say FΣ . Then an F -algebra is a set A together with interpretations of the symbols in Σ. Example: Σ has a binary symbol ◦ and a 0-ary symbol e. An algebra as usually presented might have universe {x, y }; interpret e by y , and interpret ◦ by ◦ x y

x x y

y x x

We would trade all this in for a : HΣ ({x, y }) → {x, y }: a(hei) = y a(h◦, x, xi) = x a(h◦, x, y i) = x MATHLOGAPS 2008: Coalgebra and Circularity

a(h◦, y , xi) = y a(h◦, y , y i) = x Category Theory Background

Algebras for a Functor

Let F : C → C be a functor. An algebra for F is a pair (A, a), where a : FA → A in C . The leading example is when F is a signature functor, say FΣ . A morphism from (A, a) to (B, b) is h : A → B such that FA Fh

/A

a

FB

h

/B

b

commutes. This gives a category of F -algebras.



Initial algebras Let’s return to Σ with ◦ and e, and its associated H : Set → Set. Let T0Σ be the set of finite trees (=terms) on the signature. So T0Σ contains e, ◦(e, e), ◦(◦(e, e), e), etc. We have i

#

H(T0Σ ) c

T0Σ

j

For example, i(h◦, ◦(e, e), ei) = ◦(◦(e, e), e). Then (T0Σ , i) is an initial algebra of H. For any (A, a), the unique H-algebra morphism from the term algebra (T0Σ , i) to (A, a) is evaluation of terms : T0Σ → A.



an initial algebra of another functor Consider now Pfin on Set. Then Vω = Pfin Vω is the set of hereditarily finite sets. (Vω , id) is an initial algebra of Pfin . That is, given (A, a : Pfin A → A), we need a unique h : Vω → A such that id / Pfin Vω Vω Pfin h

Pfin A

a

h

/A

We get h by -recursion, and the formula is h(x) =


??


an initial algebra of another functor Consider now Pfin on Set. Then Vω = Pfin Vω is the set of hereditarily finite sets. (Vω , id) is an initial algebra of Pfin . That is, given (A, a : Pfin A → A), we need a unique h : Vω → A such that id / Pfin Vω Vω Pfin h

Pfin A

a

h

/A

We get h by -recursion, and the formula is h(x)

=

a(Pfin h(x))


=

a({h(y ) : y ∈ x}).


Coalgebras for a Functor

Let F : C → C be a functor. A coalgebra for F is a pair (A, a), where a : A → FA in C . We’ll shortly see many examples. A morphism from (A, a) to (B, b) is h : A → B such that A h

a

B

/ FA

b

Fh

/ FB

commutes.



Why are we studying coalgebras?

stream systems are coalgebras for FX = N × X tree systems are coalgebras for FX = HΣ X , where Σ is x, y , •, ∗ set systems (= graphs) are coalgebra for FX = PX Solutions are coalgebra morphisms into final coalgebras. Next time we’ll see a result that gives us final coalgebras in all cases except PX (but it works for Pfin X ).



Why are we studying coalgebras? stream systems are coalgebras for FX = N × X tree systems are coalgebras for FX = HΣ X , where Σ is x, y , •, ∗ set systems (= graphs) are coalgebra for FX = PX Solutions are coalgebra morphisms into final coalgebras. Next time we’ll see a result that gives us final coalgebras in all cases except PX (but it works for Pfin X ). belief spaces are coalgebras for FX = ∆([0, 1] × X ) on Meas



Automata and languages Let A = {a, b, c} be a set which we think of as alphabet symbols, and consider the functor FX = X A × 2, where 2 = {0, 1}. A coalgebra for this F is a re-packaged version of a deterministic automaton. a,b

c

a,c

9y

xM m b

b,c

ze

a

Here S = {x, y , z}, and e : S → FS is e(x) e(y ) e(z)

= = =

h{ha, xi, hb, xi, hc, y i}, 0i h{ha, y i, hb, xi, hc, y i}, 1i y is accepting h{ha, zi, hb, xi, hc, xi}, 0i



Automata and languages a,b

c

9y

xM m

b,c

b

ze a Let A∗ be the set of finite words on A, including the empty word . We define δ : X × A∗ → X by recursion: a,c

δ(s, ) δ(s, wi)

= =

s fst(e(δ(s, w )))(i)

For example δ(x, bacabc) = y . Also, let L be the set P(A∗ ) of languages on A. We define acc : X → L, the language acceptance function by acc(s)

= =

{w ∈ A∗ : δ(a, w ) is an accepting state} {w ∈ A∗ : snd(δ(a, w )) = 1}



L carries a coalgebra structure Let l : L → F L be given by l(L)

=

hi 7→ {w : wi ∈ L}, 1 iff ∈ Li.

This is the language automaton (L, l). For example, if L

=

{, ab, abab, ababab, abababab, . . .}

then l(L)

=

h(a 7→ ∅, b 7→ {a, aba, ababa, . . .}, c 7→ ∅), 1i



L carries a coalgebra structure

Let l : L → F L be given by l(L)

=

hi 7→ {w : wi ∈ L}, 1 iff ∈ Li.

This is the language automaton (L, l). For all languages L and words w ∈ A∗ , δ(L,l) (L, w ) = {v : vw ∈ L}.



L carries a coalgebra structure

Let l : L → F L be given by l(L)

=

hi 7→ {w : wi ∈ L}, 1 iff ∈ Li.

This is the language automaton (L, l). In it, acc(L,l) (L)

= = = =

{w : δ(L, w ) is an accepting state} {w : {v : vw ∈ L} contains } {w : w ∈ L} L



The language automaton is a final coalgebra

One first checks that acc is a coalgebra morphism: S acc

e

L

/ FS

l

F acc

/ FL

Second, every coalgebra morphism preserves language acceptance.



The language automaton is a final coalgebra One first checks that acc is a coalgebra morphism: e

S acc

/ FS

L

l

F acc

/ FL

Second, every coalgebra morphism preserves language acceptance. To prove the uniqueness of acc, let ϕ : S → L be a coalgebra morphism. Then for all states s of S, acc(S,e) (s)

=

acc(L,l) (ϕ(s))

=

ϕ(s).

And this just says that ϕ = acc. MATHLOGAPS 2008: Coalgebra and Circularity


The big picture

algebra initial algebra least fixed point congruence relation Foundation Axiom iterative conception equational logic recursion: map out of an initial algebra useful in syntax construct bottom-up

coalgebra final coalgebra greatest fixed point bisimulation equivalence relation Anti-Foundation Axiom coiterative conception modal logic corecursion: map into a final coalgebra useful in semantics observe top-down



Lambek’s Lemma

Lemma (Lambek’s Lemma) Let C be a category, let F : C → C be a functor, and let (a, f ) be an initial algebra for F . Then f is an isomorphism: there is a morphism g : Fa → a such that g · f = id a and f · g = id Fa . The same statement holds for final coalgebras of F .



Proof of Lambek’s Lemma Note first that (Fa, Ff ) is an algebra for F . The square below commutes: Ff / FFa Fa Ff

Fa

f

f

/a

By initiality, there is a morphism g : a → Fa so that the square on the top commutes: Fa Fg

FFa Ff

f

Ff

Fa

/a g

/ Fa

f

f

/a

The bottom is obvious, the outside of the figure thus commutes. MATHLOGAPS 2008: Coalgebra and Circularity


Proof of Lambek’s Lemma, continued By initiality, there is a morphism g : a → Fa so that the square on the top commutes: Fa Fg F (f ·g )

FFa Ff

/a

f

Ff

g

/ Fa

f ·g

f

Fa

/a}

f

By initiality, we see that f · g = id a . And then from that top square again, g · f = Ff · Fg = F (f · g ) = F id a = id Fa . This completes the proof. MATHLOGAPS 2008: Coalgebra and Circularity


There are no initial algebras or final coalgebras of P An isomorphism in Set is a bijection. And there are no maps from any set onto its power set (Cantor’s Theorem). Together with Lambek’s Lemma, we see that P on Set has no initial algebra and no final coalgebra. To get around this, one either 1 2

moves from Set to the category Class. moves from P to Pκ , the functor giving the subsets of a set of size < κ.

We’ll generally go the second route, and in particular consider Pfin . It turns out that (Hκ , id) is an initial algebra of Pκ . We’ll see the final coalgebra later.



Natural transformations Let F : C → D be a functor between two categories, and let G : C → D also be a functor between the same two. Then a natural transformation from F to G is a family η of morphisms of D indexed by objects of C , in particular each ηx is a morphism in D from Fx to Gx. The requirement on η is that for each morphism in C of the form f : x → y , the square below commutes: x

Fx f

y

Ff

ηx

Fy

/ Gx

ηy

Gf

/ Gy

In symbols, Gf · ηx = ηy · Ff . One writes η : F → G . For each object x of C , ηx is called the component of η at x. MATHLOGAPS 2008: Coalgebra and Circularity


Constructions on natural transformations Suppose first that η : F → G , and let H : B → C be another functor. Then F · H : B → D and G · H : B → D. We get a natural transformation called ηH from F · H to G · H by ηH b

=

ηHb .

Now let H : D → E . So now H · F and H · G are functors from C to E . We get a natural transformation from H · F to H · G , this time called Hη, by (Hη)x = Hηx . That is, we apply the functor H to the morphism ηx . The verification of naturality is a little different: we apply H throughout. MATHLOGAPS 2008: Coalgebra and Circularity


Constructions on natural transformations Suppose first that η : F → G , and let H : B → C be another functor. Then F · H : B → D and G · H : B → D. We get a natural transformation called ηH from F · H to G · H by ηH b

=

ηHb .

To check that this is indeed natural, let f : x → y be a morphism in B. Then for each x in B (ηH)x : (F · H)x → G · H)x. And we have the diagram (F · H)x (F ·H)f

(ηH)x

(F · H)y

/ (G · H)x

(ηH)y

(G ·H)f

/ (G · H)y

This is literally the same as F (Hx) MATHLOGAPS 2008: Coalgebra and Circularity

ηHx

/ G (Hx) Category Theory Background

Constructions on natural transformations If η : F → G and µ : F → H, then we get a natural transformation µ · η : F → H by (µ · η)x = µx · ηx . The verification of naturality is easy. Finally, suppose that F , G : D → E and H, K : C → D, and let η : F → G and µ : H → K . We get a natural transformation µ ∗ η : F · H → K · G by Fµ

F · HII II

ηH

G ·H

/F ·K

µ∗ηII Gµ

ηK

II$ /G ·K

That is, we claim that the outside of the figure commutes, and then we define µ ∗ η to be the composite in either direction; this will be a natural transformation by the three constructions which we have already seen. But for each object x of C the square above is a naturality square for η, applied to the morphsim µ x : Hx → Kx. MATHLOGAPS 2008: Coalgebra and Circularity Category Theory Background

Functors preserving (weak) pullbacks

Definition A functor F : C → D preserves pullbacks if the image of every pullback square is a pullback square. Lemma Concerning preservation of pullbacks: 1

Constant functors preserve pullbacks.

2

If F and G preserve pullbacks, so do F + G , F × G , and F · G .

3

P, Pfin , and D do not preserve pullbacks.



Set-functors and surjective maps Lemma Every functor F on Set preserves all surjective maps. Proof. Suppose g : X → Y is surjective. Let h : Y → X be such that g · h = id Y . Then Fg · Fh = id FY , and so Fg must be surjective. Proposition If FX = ∅ for some X 6= ∅, then F is the constant functor ∅. Proof. Let Y be any set. Then there is f : Y → X ; f could be a constant, for example. And now Ff : FY → ∅. So FY must be empty also, since there are no maps from a non-empty set to ∅. MATHLOGAPS 2008: Coalgebra and Circularity
