Yoneda embedding

The Yoneda embedding $よ : 𝖢 ↪ 𝖯 𝖲 𝗁 (𝖢)$ is an embedding of a locally small category $𝖢$ into the Category of presheaves, that

maps an object $𝑋 \in 𝖢$ to the presheaf $よ 𝑋 = 𝖢 (-, 𝑋)$
maps a morphism $𝑓 : 𝑋 \to 𝑌$ to the natural transformation $よ 𝑓 = 𝑓 ⋆$ , whose components are the pushforwards of $𝑓$

Proof of embedding

Let $𝑋, 𝑌 \in 𝖢$ . By the Yoneda lemma we have

H 𝑋, よ 𝑌 : 𝖲 𝖾 𝗍 𝖢 𝐨 𝐩 (よ 𝑋, よ 𝑌) ≅ (よ 𝑌) 𝑋 = 𝖢 (𝑋, 𝑌)

where using the notation of the proof of the Yoneda lemma given $𝑥 \in (よ 𝑌) 𝑋 = 𝖢 (𝑋, 𝑌)$ and $𝑓 \in 𝖢 (𝑋', 𝑋)$

(𝜗 𝑥) 𝑋' 𝑓 = ((よ 𝑌) 𝑓) 𝑥 = 𝖢 (𝑓, 𝑌) 𝑥 = 𝑥 𝑓 = 𝖢 (𝑋', 𝑥) 𝑓 = (よ 𝑥) 𝑋' 𝑓

so $𝜗 𝑥 = よ 𝑥$ , implying

H - 1 𝑋, よ 𝑌 = よ ↾ 𝖢 (𝑋, 𝑌)

so in particular, $よ$ is fully faithful. $よ$ is also clearly injective on objects, since if $よ 𝑋 = よ 𝑌$ then

1 𝑋 \in 𝖢 (𝑋, 𝑋) = (よ 𝑋) 𝑋 = (よ 𝑌) 𝑋 = 𝖢 (𝑋, 𝑌)

so $𝑋 = 𝑌$ .

#state/tidy | #lang/en | #SemBr