close_eq_top_iff_mem — Mathlib

English

Let J1 be a Grothendieck topology on a category. For any object X and sieve S on X, the closure of S with respect to J1 is the top sieve if and only if S belongs to J1 X.

Русский

Пусть J1 — топология Гротендикса на категорию. Для любого объекта X и любого сита S над X замыкание S относительно J1 равно верхнему ситу тогда и только тогда, когда S принадлежит J1 X.

LaTeX

$$$J_1\mathrm{.close} S = \top \iff S \in J_1 X$$$

Lean4

/-- The sieve `S` is in the topology iff its closure is the maximal sieve. This shows that the closure
operator determines the topology.
-/
theorem close_eq_top_iff_mem {X : C} (S : Sieve X) : J₁.close S = ⊤ ↔ S ∈ J₁ X :=
  by
  constructor
  · intro h
    apply J₁.transitive (J₁.top_mem X)
    intro Y f hf
    change J₁.close S f
    rwa [h]
  · intro hS
    rw [eq_top_iff]
    intro Y f _
    apply J₁.pullback_stable _ hS

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