Lean4
/-- The Grothendieck topology associated to a coverage `K`.
It is defined *inductively* as follows:
1. If `S` is a covering presieve for `K`, then the sieve generated by `S` is a covering
sieve for the associated Grothendieck topology.
2. The top sieves are in the associated Grothendieck topology.
3. Add all sieves required by the *local character* axiom of a Grothendieck topology.
The pullback compatibility condition for a coverage ensures that the
associated Grothendieck topology is pullback stable, and so an additional constructor
in the inductive construction is not needed.
-/
def toGrothendieck (K : Coverage C) : GrothendieckTopology C
where
sieves := Saturate K
top_mem' := .top
pullback_stable' := by
intro X Y S f hS
induction hS generalizing Y with
| of X S hS =>
obtain ⟨R, hR1, hR2⟩ := K.pullback f S hS
suffices Sieve.generate R ≤ (Sieve.generate S).pullback f from saturate_of_superset _ this (Saturate.of _ _ hR1)
rintro Z g ⟨W, i, e, h1, h2⟩
obtain ⟨WW, ii, ee, hh1, hh2⟩ := hR2 h1
refine ⟨WW, i ≫ ii, ee, hh1, ?_⟩
simp only [hh2, reassoc_of% h2, Category.assoc]
| top X => apply Saturate.top
| transitive X R S _ hS H1 _ =>
apply Saturate.transitive
· apply H1 f
intro Z g hg
rw [← Sieve.pullback_comp]
exact hS hg
transitive' _ _ hS _ hR := .transitive _ _ _ hS hR
