English
The presheaf that assigns to each X the set of J-closed sieves on X is a J-sheaf.
Русский
Предварительный слепок, который сопоставляет каждому X множество J-закрытых сит над X, является J-шейфом.
LaTeX
$$$\mathrm{Presieve.IsSheaf}(J_1, \mathrm{Functor.closedSieves}(J_1))$$$
Lean4
/-- The presheaf of `J`-closed sieves is a `J`-sheaf.
The proof of this is adapted from [MM92], Chapter III, Section 7, Lemma 1.
-/
theorem classifier_isSheaf : Presieve.IsSheaf J₁ (Functor.closedSieves J₁) :=
by
intro X S hS
rw [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor]
refine ⟨?_, ?_⟩
· rintro x ⟨M, hM⟩ ⟨N, hN⟩ hM₂ hN₂
simp only [Functor.closedSieves_obj]
ext Y f
dsimp only [Subtype.coe_mk]
rw [← J₁.covers_iff_mem_of_isClosed hM, ← J₁.covers_iff_mem_of_isClosed hN]
have q : ∀ ⦃Z : C⦄ (g : Z ⟶ X) (_ : S g), M.pullback g = N.pullback g := fun Z g hg =>
congr_arg Subtype.val ((hM₂ g hg).trans (hN₂ g hg).symm)
have MSNS : M ⊓ S = N ⊓ S := by
ext Z g
rw [Sieve.inter_apply, Sieve.inter_apply]
simp only [and_comm]
apply and_congr_right
intro hg
rw [Sieve.mem_iff_pullback_eq_top, Sieve.mem_iff_pullback_eq_top, q g hg]
constructor
· intro hf
rw [J₁.covers_iff]
apply J₁.superset_covering (Sieve.pullback_monotone f inf_le_left)
rw [← MSNS]
apply J₁.arrow_intersect f M S hf (J₁.pullback_stable _ hS)
· intro hf
rw [J₁.covers_iff]
apply J₁.superset_covering (Sieve.pullback_monotone f inf_le_left)
rw [MSNS]
apply J₁.arrow_intersect f N S hf (J₁.pullback_stable _ hS)
· intro x hx
rw [Presieve.compatible_iff_sieveCompatible] at hx
let M := Sieve.bind S fun Y f hf => (x f hf).1
have : ∀ ⦃Y⦄ (f : Y ⟶ X) (hf : S f), M.pullback f = (x f hf).1 :=
by
intro Y f hf
apply le_antisymm
· rintro Z u ⟨W, g, f', hf', hg : (x f' hf').1 _, c⟩
rw [Sieve.mem_iff_pullback_eq_top, ←
show (x (u ≫ f) _).1 = (x f hf).1.pullback u from congr_arg Subtype.val (hx f u hf)]
conv_lhs => congr; congr;
rw [← c] -- Porting note: Originally `simp_rw [← c]`
rw [show (x (g ≫ f') _).1 = _ from congr_arg Subtype.val (hx f' g hf')]
apply Sieve.pullback_eq_top_of_mem _ hg
· apply Sieve.le_pullback_bind S fun Y f hf => (x f hf).1
refine ⟨⟨_, J₁.close_isClosed M⟩, ?_⟩
intro Y f hf
simp only [Functor.closedSieves_obj]
ext1
dsimp
rw [← J₁.pullback_close, this _ hf]
apply le_antisymm (J₁.le_close_of_isClosed le_rfl (x f hf).2) (J₁.le_close _)
