toCoverage

Mathlib.CategoryTheory.Sites.Coverage

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

Lean4

/-- Associate a coverage to any Grothendieck topology.
If `J` is a Grothendieck topology, and `K` is the associated coverage, then a presieve
`S` is a covering presieve for `K` if and only if the sieve that it generates is a
covering sieve for `J`.
-/
def toCoverage (J : GrothendieckTopology C) : Coverage C
    where
  coverings X := {S | Sieve.generate S ∈ J X}
  pullback := by
    intro X Y f S (hS : Sieve.generate S ∈ J X)
    refine ⟨(Sieve.generate S).pullback f, ?_, fun Z g h => h⟩
    dsimp
    rw [Sieve.generate_sieve]
    exact J.pullback_stable _ hS

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

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

Разделы

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

Аффилиация

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