Saturate

Mathlib.CategoryTheory.Sites.Coverage

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Coverage.Saturate

Lean4

/-- An auxiliary definition used to define the Grothendieck topology associated to a
coverage. See `Coverage.toGrothendieck`.
-/
inductive Saturate (K : Coverage C) : (X : C) → Sieve X → Prop where
  | of (X : C) (S : Presieve X) (hS : S ∈ K X) : Saturate K X (Sieve.generate S)
  | top (X : C) : Saturate K X ⊤
  |
  transitive (X : C) (R S : Sieve X) :
    Saturate K X R → (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → Saturate K Y (S.pullback f)) → Saturate K X S

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

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

Разделы

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

Аффилиация

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