English
If the presheaf of J1-closed sieves is a J2-sheaf, then J1 is less than or equal to J2.
Русский
Если предпредсет замкнутых сит по J1 является шейфом по J2, то J1 ⊆ J2.
LaTeX
$$$(\mathrm{Presieve.IsSheaf}(J_1, \mathrm{Functor.closedSieves}(J_2))) \Rightarrow J_1 \le J_2$$$
Lean4
/-- If presheaf of `J₁`-closed sieves is a `J₂`-sheaf then `J₁ ≤ J₂`. Note the converse is true by
`classifier_isSheaf` and `isSheaf_of_le`.
-/
theorem le_topology_of_closedSieves_isSheaf {J₁ J₂ : GrothendieckTopology C}
(h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)) : J₁ ≤ J₂ :=
by
intro X S hS
rw [← J₂.close_eq_top_iff_mem]
have : J₂.IsClosed (⊤ : Sieve X) := by
intro Y f _
trivial
suffices (⟨J₂.close S, J₂.close_isClosed S⟩ : Subtype _) = ⟨⊤, this⟩
by
rw [Subtype.ext_iff] at this
exact this
apply (h S hS).isSeparatedFor.ext
intro Y f hf
simp only [Functor.closedSieves_obj]
ext1
dsimp
rw [Sieve.pullback_top, ← J₂.pullback_close, S.pullback_eq_top_of_mem hf, J₂.close_eq_top_iff_mem]
apply J₂.top_mem
