IsSheaf'

Mathlib.CategoryTheory.Sites.Sheaf

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

Lean4

/-- An alternative definition of the sheaf condition in terms of equalizers. This is shown to be
equivalent in `CategoryTheory.Presheaf.isSheaf_iff_isSheaf'`.
-/
def IsSheaf' (P : Cᵒᵖ ⥤ A) : Prop :=
  ∀ (U : C) (R : Presieve U) (_ : generate R ∈ J U),
    Nonempty
      (IsLimit (Fork.ofι _ (w R P)))
        -- Again I wonder whether `UnivLE` can somehow be used to allow `s` to take
        -- values in a more general universe.

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

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

Разделы

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

Аффилиация

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