closedSieves

Mathlib.CategoryTheory.Sites.Closed

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.closedSieves

Lean4

/-- The presheaf sending each object to the set of `J`-closed sieves on it. This presheaf is a `J`-sheaf
(and will turn out to be a subobject classifier for the category of `J`-sheaves).
-/
@[simps]
def closedSieves : Cᵒᵖ ⥤ Type max v u
    where
  obj X := { S : Sieve X.unop // J₁.IsClosed S }
  map f S := ⟨S.1.pullback f.unop, J₁.isClosed_pullback f.unop _ S.2⟩

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

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

Разделы

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

Аффилиация

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