Definition. Presheaf [local-0]
Definition. Presheaf [local-0]
Let be a category. A presheaf over is a functor of the form
For each object , we will denote by
the evaluation of at . The set will sometimes be called the fibre of the presheaf at , and the elements of thus deserve the name of sections of over .
For morphism , the induced map from denotes .
The category of presheaves over denotes .
Definition. Yoneda embedding [local-1]
Definition. Yoneda embedding [local-1]
Lemma. Yoneda [local-3]
Lemma. Yoneda [local-3]
For any presheaf over , there is a natural bijection of the form
Proof. [local-2]
Proof. [local-2]
We first define inverse map , given a section of over , i.e. , we have
for each morphism . This indeed defines a morphism in .
Now check and indeed are inverse of each other. First: given , we have
Another direction: given , we have
for each . Naturality is obvious, hence they form a natural bijection.