The Yoneda Lemma

Representable Functor F of C ( a, -):

\boxed {(-)^{a} = \text {F} \iff a = \text {log F}}

Video 4.2 Yoneda Lemma

Prove : 

Yoneda Lemma :
\text {F :: C} \to \text {Set}

\boxed {\alpha \text { :: [C, Set] (C (a, -),F) } \simeq \text {F a}}

\alpha : \text {Natural Transformation}
\simeq : \text {(Natural) Isomorphism, "naturally" } \forall ( a, F )

Proof: By “Diagram chasing” below, shows that

: \alpha \text { :: [C, Set] (C (a, -),F) } is indeed a (co-variant) Functor. (Higher-order Function)

Right-side: Functor “F a“. (Data Structure)

\boxed {\forall x, (a \to x) \to \text { F } x \simeq \text { F } a }

Note: When talking about the natural transformations, always mention their component “x”: \alpha_{x}, \beta_{x}

Video 5.1 Yoneda Embedding

Example 1: F = List functor [x]

\boxed {\alpha \text { :: } (a \to x) \to [x] \simeq [a] }

Example 2: F = C (b, -)

\boxed {\alpha \text { :: [C, Set] (C (a, -), C (b, -) ) } \simeq \text {C (b, a)}}

Note: check a , b is in co-variant or contra-variant position.

Example 3: F = Id

\boxed {\alpha \text { :: } (a \to x) \to x \simeq a }

Right-hand-side: a (data structure)

Left-hand-side : “(a -> x) “is a function called “handler” (or “continuation“) which takes the argument “a” to provide it as output : “(a -> x ) -> x“.

eg. handler to database query, over internet…(technique used in Compiler)

Co-Yoneda Lemma : (Contra-variant a , F)

\boxed {\alpha \text { :: [C, Set] (C(-, a),F) } \simeq \text {F a}}

Yoneda Embedding: Full and Faithful
\alpha \text { :: [C, Set] (C (a, -), C (b, -) ) } \simeq \text {C (b, a)}

Note: Instead of proving a , b are isomorphic, sometimes it is easier to prove the functors C(a, -) & C(b, -) are isomorphic.[Proof Trivial: functors preserve composition and identity]

ApplicationCo-Yoneda Lemma : (Contra-variant a , F)
\boxed {\text {[C, Set] (C(- , a), C(- , b) } \simeq \text {C(a ,b)}}

Pre-order Category \boxed {a \leq b}

\forall x, \text {C(x , a)} \to \text {C(x , b)} \simeq \text {C(a , b)}

C(x , a) = x \leq a = \{\varnothing, 1 \}
C(x , b) = x \leq b =\{\varnothing, 1 \}

3 possibilities: (“1” = singleton)
id_{\varnothing} :: \varnothing \to \varnothing
absurd :: \varnothing \to 1
id_{1} :: 1 \to 1
Note: 1 \to \varnothing impossible (function must have an image)


Right-Hand Side: a \leq b

Left-Hand Side: \forall x,( x \leq a \implies x \leq b) \implies a \leq b

Yoneda Embedding (Lagatta)


One thought on “The Yoneda Lemma

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s