Yoneda lemma
Let
where
where naturality in
commutes; and naturality in
commutes.1
Proof
For
we have π β { π’ π¨ π© } ( γ π , πΉ ) . Let π π : π’ ( π , π ) β πΉ π . π₯ π : = π π ( 1 π ) β πΉ π Conversely, given an
, we can define \vartheta_{x} : \yo X \Rightarrow F : \op{\cat C} \to \Set as follows: Given any π₯ β πΉ π , we define the component π β² ( π π₯ ) π β² : π’ ( π β² , π ) β πΉ π β² β β¦ ( πΉ β ) π₯ whose naturality condition is given by the diagram
Now for
we have β β π’ ( π β² , π ) ( π π₯ ) π β³ π’ ( π , π ) β = ( π π₯ ) π β³ β π = πΉ ( β π ) π₯ = ( πΉ π ) ( πΉ β ) π₯ = ( πΉ π ) ( π π₯ ) π β² β so
is indeed natural. π π₯ Now we calculate
for π π₯ π . From the above definitions, for π β { π’ π¨ π© } ( γ π , πΉ ) we have β β π’ ( π β² , π ) ( π π₯ π ) π β² β = ( πΉ β ) π₯ π = ( πΉ β ) π π ( 1 π ) but by naturality of
π ( πΉ β ) π π ( 1 π ) = π π β² π’ ( β , π ) ( 1 π ) = π π β² β wherefore
. π ( π₯ π ) = π Conversely, for
we have π₯ β πΉ π π₯ π π₯ = ( π π₯ ) π ( 1 π ) = πΉ ( 1 π ) π₯ = 1 πΉ π π₯ = π₯ . Therefore
H π , πΉ : { π’ π¨ π© } ( γ π , πΉ ) β πΉ π π β¦ π₯ π defines a bijection for any
. π , πΉ For naturality in
, suppose πΉ Then for any π β { π’ π¨ π© } ( πΉ , πΊ ) we have π β { π’ π¨ π© } ( γ π , πΉ ) H π , πΉ ( π₯ π ) = π π π₯ π = π π π π ( 1 π ) = ( π π ) π ( 1 π ) = π₯ π π = H π , πΊ ( π π ) = H π , πΊ ( π’ ( γ π , π ) π ) so the required diagram commutes.
For naturality in
, suppose π . Then for β β π’ ( π , π ) we have π β { π’ π¨ π© } ( γ π , πΉ ) H π , πΉ { π’ π¨ π© } ( γ β , πΉ ) π = H π , πΉ ( π ( γ β ) ) = ( π ( γ β ) ) π ( 1 π ) = π π ( γ β ) π ( 1 π ) = π π π’ ( π , β ) ( 1 π ) = π π ( β ) = π π π’ ( β , π ) ( 1 π ) = π π ( ( γ π ) β ) ( 1 π ) = ( πΉ β ) π π ( 1 π ) = ( πΉ β ) H π , πΉ π as required. ^proof
Corollaries
-
The βtheoremβ: The Yoneda embedding is an embedding.
Footnotes
-
2010. Category theory, Β§8.3, pp. 189β192 β©