instUniqueHomLeftExtensionOppositeOpObjFunctorTypeYonedaMkYonedaMap

Mathlib.CategoryTheory.Limits.Presheaf

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Presheaf.instUniqueHomLeftExtensionOppositeOpObjFunctorTypeYonedaMkYonedaMap

← MathLib Explorer

Lean4

instance (X : C) (Y : F.op.LeftExtension (yoneda.obj X)) : Unique (Functor.LeftExtension.mk _ (yonedaMap F X) ⟶ Y)
    where
  default :=
    StructuredArrow.homMk (yonedaEquiv.symm (yonedaEquiv (F := F.op.comp Y.right) Y.hom))
      (by
        ext Z f
        simpa using congr_fun (Y.hom.naturality f.op).symm (𝟙 _))
  uniq
    φ := by
    ext1
    apply yonedaEquiv.injective
    simp [← StructuredArrow.w φ, yonedaEquiv]

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

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

Разделы

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

Аффилиация

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