English
The Grothendieck topology derived from a pre-coverage by taking its coverage equals the original Grothendieck topology.
Русский
Топология Гротендика, полученная из пред coverage через покрытие, равна исходной топологии Гротендика.
LaTeX
$$$$ J.toCoverage.toGrothendieck = J.toGrothendieck $$$$
Lean4
theorem toGrothendieck_toCoverage [HasPullbacks C] (J : Pretopology C) :
J.toCoverage.toGrothendieck = J.toGrothendieck := by
ext T S
rw [mem_toGrothendieck, Coverage.mem_toGrothendieck]
refine ⟨fun h ↦ ?_, fun ⟨R, hR, hle⟩ ↦ ?_⟩
·
induction h with
| of X S hS => use S, hS, Sieve.le_generate S
| top X => use Presieve.singleton (𝟙 X), J.has_isos (𝟙 X), le_top
| transitive X R S hR hRS hle hfS =>
obtain ⟨R', hR', hle⟩ := hle
choose S' hS' hS'le using hfS
refine ⟨Presieve.bind R' (fun Y f hf ↦ S' (hle _ hf)), ?_, fun Z u hu ↦ ?_⟩
· exact J.transitive R' (fun Y f hf ↦ S' (hle Y hf)) hR' fun Y f H ↦ hS' (hle Y H)
· obtain ⟨W, g, w, hw, hg, rfl⟩ := hu
exact hS'le _ _ hg
· refine Coverage.saturate_of_superset _ ?_ (.of _ _ hR)
rwa [Sieve.generate_le_iff]
