OverArrows

Mathlib.CategoryTheory.Comma.Presheaf.Basic

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

Lean4

/-- This is equivalent to the type `Over.mk s ⟶ Over.mk η`, but that lives in the wrong universe.
However, if `F = yoneda.obj Y` for some `Y`, then (using that the Yoneda embedding is fully
faithful) we get a good statement, see `OverArrow.costructuredArrowIso`. -/
def OverArrows {F : Cᵒᵖ ⥤ Type v} (η : F ⟶ A) {X : C} (s : yoneda.obj X ⟶ A) : Type v :=
  Subtype (MakesOverArrow η s)

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

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

Разделы

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

Аффилиация

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