English
For a precoverage K with suitable pullbacks and base-change stability, the Grothendieck topology on Over X obtained by localizing K is equal to the comap of K along the forgetful functor Over forget X to C.
Русский
При заданной пре-покрывающей системе K со свойствами основания и устойчивости к базовому изменению, топология Гротендика на Over X равна композиции/супер-покрытию через forget X.
LaTeX
$$$K.toGrothendieck.over X = (K.comap(Over.forget X)).toGrothendieck$$$
Lean4
/-- The Grothendieck topology on `Over X`, obtained from localizing the topology generated
by the precoverage `K`, is generated by the preimage of `K`. -/
theorem over_toGrothendieck_eq_toGrothendieck_comap_forget (X : C) :
K.toGrothendieck.over X = (K.comap (Over.forget X)).toGrothendieck :=
by
refine le_antisymm ?_ ?_
· intro ⟨Y, right, (s : Y ⟶ X)⟩ R hR
obtain ⟨(R : Sieve Y), rfl⟩ := (Sieve.overEquiv _).symm.surjective R
simp only [GrothendieckTopology.mem_over_iff, Equiv.apply_symm_apply] at hR
induction hR with
| of Z S hS =>
rw [Sieve.overEquiv_symm_generate]
exact .of _ _ (by simpa)
| top =>
rw [Sieve.overEquiv_symm_top]
simp
| transitive Y R S hR H ih
ih' =>
refine GrothendieckTopology.transitive _ (ih s) _ fun Z g hg ↦ ?_
obtain rfl : right = Z.right := Subsingleton.elim _ _
rw [← Sieve.overEquiv_symm_pullback]
exact ih' hg Z.hom
· rw [Precoverage.toGrothendieck_le_iff_le_toPrecoverage]
intro Y R hR
rw [Precoverage.mem_comap_iff] at hR
rw [GrothendieckTopology.mem_toPrecoverage_iff, GrothendieckTopology.mem_over_iff, Sieve.overEquiv, Equiv.coe_fn_mk,
← Sieve.generate_map_eq_functorPushforward]
exact Coverage.Saturate.of _ _ hR
