English
There is a natural isomorphism between the Coyoneda pairing and the Coyoneda evaluation: coyonedaPairing C ≅ coyonedaEvaluation C. This states that pairing (X,F) ↦ (coyoneda.obj X ⟶ F) is naturally equivalent to evaluation (X,F) ↦ F.obj X.
Русский
Существует естественное тождественное отношение между связыванием Coyoneda и оценкой Coyoneda: coyonedaPairing C ≅ coyonedaEvaluation C; то есть сопряжение (X,F) ↦ (coyoneda.obj X ⟶ F) эквивалентно отображению (X,F) ↦ F(X).
LaTeX
$$$$ coyoneda\,pairing(C) \cong coyonedaEvaluation(C) $$$$
Lean4
/-- The Coyoneda lemma asserts that the Coyoneda pairing
`(X : C, F : C ⥤ Type) ↦ (coyoneda.obj X ⟶ F)`
is naturally isomorphic to the evaluation `(X, F) ↦ F.obj X`. -/
@[stacks 001P]
def coyonedaLemma : coyonedaPairing C ≅ coyonedaEvaluation C :=
NatIso.ofComponents (fun _ ↦ Equiv.toIso (coyonedaEquiv.trans Equiv.ulift.symm))
(by
intro (X, F) (Y, G) f
ext (a : coyoneda.obj (op X) ⟶ F)
apply ULift.ext
dsimp [coyonedaEquiv, coyonedaEvaluation]
simp [← FunctorToTypes.naturality])
