English
The Yoneda lemma asserts a natural isomorphism between the Yoneda pairing and the Yoneda evaluation: yonedaPairing C ≅ yonedaEvaluation C, natural in both arguments.
Русский
Лемма Ёнеда утверждает естественную изomорфизм между парингом Ёнеда и оценкой Ёнеда: yonedaPairing C ≅ yonedaEvaluation C, естественный по обоим аргументам.
LaTeX
$$$\ yonedaLemma : yonedaPairing C \cong yonedaEvaluation C$$$
Lean4
/-- The Yoneda lemma asserts that the Yoneda pairing
`(X : Cᵒᵖ, F : Cᵒᵖ ⥤ Type) ↦ (yoneda.obj (unop X) ⟶ F)`
is naturally isomorphic to the evaluation `(X, F) ↦ F.obj X`. -/
@[stacks 001P]
def yonedaLemma : yonedaPairing C ≅ yonedaEvaluation C :=
NatIso.ofComponents (fun _ ↦ Equiv.toIso (yonedaEquiv.trans Equiv.ulift.symm))
(by
intro (X, F) (Y, G) f
ext (a : yoneda.obj X.unop ⟶ F)
apply ULift.ext
dsimp [yonedaEvaluation, yonedaEquiv]
simp [← FunctorToTypes.naturality])
