curriedCoyonedaLemma

Mathlib.CategoryTheory.Yoneda

URI: https://scilib.ai/kg/mathlib#CategoryTheory.curriedCoyonedaLemma

Lean4

/-- The curried version of coyoneda lemma when `C` is small. -/
def curriedCoyonedaLemma {C : Type u₁} [SmallCategory C] : coyoneda.rightOp ⋙ coyoneda ≅ evaluation C (Type u₁) :=
  NatIso.ofComponents (fun X ↦ NatIso.ofComponents (fun _ ↦ Equiv.toIso coyonedaEquiv))
    (by
      intro X Y f
      ext a b
      simp [coyonedaEquiv, ← FunctorToTypes.naturality])

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru