Lean4
/-- A closure (increasing, inflationary and idempotent) operation on sieves that commutes with pullback
induces a Grothendieck topology.
In fact, such operations are in bijection with Grothendieck topologies.
-/
@[simps]
def topologyOfClosureOperator (c : ∀ X : C, ClosureOperator (Sieve X))
(hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), c _ (S.pullback f) = (c _ S).pullback f) : GrothendieckTopology C
where
sieves X := {S | c X S = ⊤}
top_mem' X := top_unique ((c X).le_closure _)
pullback_stable' X Y S f
hS := by
rw [Set.mem_setOf_eq] at hS
rw [Set.mem_setOf_eq, hc, hS, Sieve.pullback_top]
transitive' X S hS R
hR := by
rw [Set.mem_setOf_eq] at hS
rw [Set.mem_setOf_eq, ← (c X).idempotent, eq_top_iff, ← hS]
apply (c X).monotone fun Y f hf => _
intro Y f hf
rw [Sieve.mem_iff_pullback_eq_top, ← hc]
apply hR hf
