yoneda

Mathlib.CategoryTheory.Sites.Canonical

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GrothendieckTopology.yoneda

Lean4

/-- If `J` is subcanonical, we obtain a "Yoneda" functor from the defining site
into the sheaf category.
-/
@[simps]
def yoneda [J.Subcanonical] : C ⥤ Sheaf J (Type v)
    where
  obj
    X :=
    ⟨CategoryTheory.yoneda.obj X, by
      rw [isSheaf_iff_isSheaf_of_type]
      apply Subcanonical.isSheaf_of_isRepresentable⟩
  map f := ⟨CategoryTheory.yoneda.map f⟩

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

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

Разделы

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

Аффилиация

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