English
The Grothendieck topology associated to a coverage K is the infimum of all Grothendieck topologies whose associated coverage contains K.
Русский
Топология Гротендика, связанная с покрытием K, является инфимумом всех топологий Гротендика, чьи покрывающие структуры содержат K.
LaTeX
$$$$ \mathrm{toGrothendieck}(K) = \inf\{ J \mid K \le J.toCoverage \} $$$$
Lean4
/-- An alternative characterization of the Grothendieck topology associated to a coverage `K`:
it is the infimum of all Grothendieck topologies whose associated coverage contains `K`.
-/
theorem toGrothendieck_eq_sInf (K : Coverage C) : toGrothendieck K = sInf {J | K ≤ J.toCoverage} :=
by
apply le_antisymm
· apply le_sInf
intro J hJ X S hS
induction hS with
| of X S hS => apply hJ; assumption
| top => apply J.top_mem
| transitive X R S _ _ H1 H2 => exact J.transitive H1 _ H2
· apply sInf_le
intro X S hS
apply Saturate.of _ _ hS
