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] :
    yoneda ⋙ (whiskeringLeft C (C ⥤ Type u₁)ᵒᵖ (Type u₁)).obj coyoneda.rightOp ≅ 𝟭 (C ⥤ Type u₁) :=
  NatIso.ofComponents
    (fun F ↦
      NatIso.ofComponents (fun _ ↦ Equiv.toIso coyonedaEquiv)
        (by
          intro X Y f
          ext a
          simp [coyonedaEquiv, ← FunctorToTypes.naturality]))

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

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

Разделы

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

Аффилиация

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