米田の補題 - pogi-log

米田の補題

米田の補題(よねだのほだい、Yoneda lemma)、米田埋め込み (よねだうめこみ、Yoneda embedding)

米田の補題（よねだのほだい、英: Yoneda lemma）とは、小さなhom集合をもつ圏 C について、共変hom関手 hom(A , _) : C → Set から集合値関手 F : C → Set への自然変換と、集合である対象 F(A) の要素との間に一対一対応が存在するという定理である。「米田の補題」という名称は、米田信夫に因んでソーンダース・マックレーンにより名付けられた。

局所的に小さい圏$ C

共変Hom関手$ \mathrm{Hom}(A, -) : C \to \mathbf{Set}

$ A : 対象

$ \mathbf{Set} : 圏Set

$ F : C \to \mathbf{Set}

$ \mathrm{Nat}(\mathrm{Hom}(A, -), F) \simeq F(A)

mathlib4での定義

Mathlib.CategoryTheory.Yoneda

code:lean.hs

/-- The Yoneda embedding, as a functor from C into presheaves on C.

See <https://stacks.math.columbia.edu/tag/001O>.

@simps