可表函子
在局部小範疇 C 中固定一個物件 A。指派 h^A = Hom(A, −) : C → Set 是一個函子(它把 f : X → Y 送到後複合 f∘− : Hom(A, X) → Hom(A, Y))。函子 F : C → Set 稱為[[representable-functor|可表]],若它自然同構於某個 Hom(A, −);稱物件 A 表示 F。可表性是偽裝的泛性質:A 表示 F 恰當 F 帶有一個泛元素。
米田引理
這就是整條軌道所指向的定理。對任意函子 F : C → Set 與任意物件 A,[[yoneda-lemma|米田引理]]給出一個對 A 與 F 都自然的雙射:Nat( Hom(A, −), F ) ≅ F(A)。從可表函子 Hom(A, −) 出發的自然變換,與 F(A) 中的單個元素是同一份資料。一旦問對了問題,證明只是一行計算。
Yoneda lemma: Nat( Hom(A,-), F ) ~= F(A).
Proof (both directions explicit):
-> Given a natural transformation eta : Hom(A,-) => F,
look at its component at A:
eta_A : Hom(A,A) -> F(A).
Feed it the identity: u := eta_A(id_A) in F(A).
Send eta |-> u.
<- Given u in F(A), DEFINE eta by, for f : A -> X,
eta_X(f) := F(f)(u) in F(X).
Naturality of eta is forced by functoriality of F.
These are mutually inverse:
start from eta, get u = eta_A(id_A), rebuild eta'_X(f)=F(f)(u);
naturality square of eta at f : A -> X says
eta_X( f o id_A ) = F(f)( eta_A(id_A) ),
i.e. eta_X(f) = F(f)(u) = eta'_X(f). So eta' = eta. QED.
Corollary (Yoneda embedding). Take F = Hom(B,-):
Nat( Hom(A,-), Hom(B,-) ) ~= Hom(B,A).
So natural transformations between representables are exactly
the morphisms B -> A. The functor A |-> Hom(A,-) is
FULLY FAITHFUL (contravariantly). An object is determined,
up to unique iso, by the functor it represents.米田嵌入推論是其哲學落點。映射 A ↦ Hom(−, A) 把 C 全忠實地嵌入函子範疇 Cᵒᵖ → Set。全忠實意味著:兩個物件若(自然地)有相同的映入它們的映射,則它們同構;且物件的同構恰對應於其可表函子的自然同構。認識一個物件,就是認識映入它的一切映射。這正是泛性質奏效的原因——它們釘死了可表函子,而米田說這就釘死了物件。