yonedaArrow

Mathlib.CategoryTheory.Comma.Presheaf.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.OverPresheafAux.OverArrows.yonedaArrow

Lean4

/-- Construct an element of `OverArrows η s` with `F = yoneda.obj Y` from a suitable morphism
`f : X ⟶ Y`. -/
def yonedaArrow {Y : C} {η : yoneda.obj Y ⟶ A} {X : C} {s : yoneda.obj X ⟶ A} (f : X ⟶ Y) (hf : yoneda.map f ≫ η = s) :
    OverArrows η s :=
  ⟨f, .of_yoneda_arrow hf⟩

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

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

Разделы

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

Аффилиация

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