米田の補題

圏Cから(Sets)への関手Fがあるとする。
Cの対象Aを取る。

米田の補題
θ:Nat(H^A, F) -> F(A) がbijection
θ(η) := ηA(1_A)

証明:

主張1: θがinjection

ηは自然変換なので、f:A->Bとして

F(f).ηA = ηB.H^A(f)

が成り立つ。

H^A(f): hom(A,A)->hom(A,B)
ηB: hom(A,B) -> F(B)

なので、
ηB(f) = ηB(H^A(f)(1_A)) = ηB.H^A(f) (1_A) = F(f).ηA (1_A)

ηはηA(1_A)で完全に決まる

主張2:θがsurjective

任意のa ∈ F(A)に対して
aB*(f) := F(f)(a)とする。

g:B->Cとして

aC*(g.f) := F(g.f)(a)

F(g)(aB*(f)) = F(g)(F(f)(a)) = F(g.f)(a) = aC*(g.f) = aC*(H^A(g)(f))
よって
F(g).aB* = aC*.H^A(g)

よって、a*は自然変換 H^A -> F

ここで、θ(a*) = aA(1_A) = a
より、θはsurjecve

本当か。。