isSheaf_yoneda'

Mathlib.CategoryTheory.Sites.Types

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

← MathLib Explorer

English

The Yoneda presheaf is a sheaf for the topology on Type

Русский

Предшефенка Yoneda является шарфом для топологии над Type

LaTeX

$$$ Presheaf.IsSheaf typesGrothendieckTopology (yoneda.obj α) $$$

Lean4

/-- The sheaf condition for `yoneda'`. -/
theorem isSheaf_yoneda' {α : Type u} : Presheaf.IsSheaf typesGrothendieckTopology (yoneda.obj α) :=
  by
  rw [isSheaf_iff_isSheaf_of_type]
  exact Presieve.isSheaf_yoneda'

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

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

Разделы

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

Аффилиация

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