米田の補題 - pogi-log

米田の補題

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

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

局所的に小さい圏$ C

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

def yoneda : C ⥤ Cᵒᵖ ⥤ Type v₁ where

obj X :=

{ obj := fun Y => unop Y ⟶ X

map := fun f g => f.unop ≫ g }

map f :=