English
Let P be a presheaf on C. Let U be a sieve on X and B a family that assigns to every Y and arrow f: Y → X a sieve on Y, such that P is a sheaf for U, P is a sheaf for each B hf, and P is separated for pullbacks of any B h along any g. Then P is a sheaf for the bind U with B, i.e., P is a sheaf for the combined sieve obtained by binding U with B.
Русский
Пусть P — преподмешка на C. Пусть U — сив на X, и B — семейство, которое каждому Y и стрелке f: Y → X ставит на Y сив, причем P является шейфом по U, по каждому B hf и разделяется по вытягиваниям pullback любых B h вдоль любых g. Тогда P является шейфом для объединённого sievе, полученного при связывании U с B.
LaTeX
$$$\Presieve.IsSheafFor P \bigl( \mathrm{Sieve.bind} (U : Presieve X) B \bigr)\,$$
Lean4
/-- To show `P` is a sheaf for the binding of `U` with `B`, it suffices to show that `P` is a sheaf for
`U`, that `P` is a sheaf for each sieve in `B`, and that it is separated for any pullback of any
sieve in `B`.
This is mostly an auxiliary lemma to show `isSheafFor_trans`.
Adapted from [Elephant], Lemma C2.1.7(i) with suggestions as mentioned in
https://math.stackexchange.com/a/358709/
-/
theorem isSheafFor_bind (P : Cᵒᵖ ⥤ Type v) (U : Sieve X) (B : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄, U f → Sieve Y)
(hU : Presieve.IsSheafFor P (U : Presieve X))
(hB : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (hf : U f), Presieve.IsSheafFor P (B hf : Presieve Y))
(hB' : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (h : U f) ⦃Z⦄ (g : Z ⟶ Y), Presieve.IsSeparatedFor P (((B h).pullback g) : Presieve Z)) :
Presieve.IsSheafFor P (Sieve.bind (U : Presieve X) B : Presieve X) :=
by
intro s hs
let y : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (hf : U f), Presieve.FamilyOfElements P (B hf : Presieve Y) := fun Y f hf Z g hg =>
s _ (Presieve.bind_comp _ _ hg)
have hy : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (hf : U f), (y hf).Compatible :=
by
intro Y f H Y₁ Y₂ Z g₁ g₂ f₁ f₂ hf₁ hf₂ comm
apply hs
apply reassoc_of% comm
let t : Presieve.FamilyOfElements P (U : Presieve X) := fun Y f hf => (hB hf).amalgamate (y hf) (hy hf)
have ht : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (hf : U f), (y hf).IsAmalgamation (t f hf) := fun Y f hf => (hB hf).isAmalgamation _
have hT : t.Compatible := by
rw [Presieve.compatible_iff_sieveCompatible]
intro Z W f h hf
apply (hB (U.downward_closed hf h)).isSeparatedFor.ext
intro Y l hl
apply (hB' hf (l ≫ h)).ext
intro M m hm
have : bind U B (m ≫ l ≫ h ≫ f) := by simpa using (Presieve.bind_comp f hf hm : bind U B _)
trans s (m ≫ l ≫ h ≫ f) this
· have := ht (U.downward_closed hf h) _ ((B _).downward_closed hl m)
rw [op_comp, FunctorToTypes.map_comp_apply] at this
grind
· have h : s _ _ = _ := (ht hf _ hm).symm
conv_lhs at h => congr; rw [assoc, assoc]
rw [h]
simp only [op_comp, assoc, FunctorToTypes.map_comp_apply]
refine ⟨hU.amalgamate t hT, ?_, ?_⟩
· rintro Z _ ⟨Y, f, g, hg, hf, rfl⟩
rw [op_comp, FunctorToTypes.map_comp_apply, Presieve.IsSheafFor.valid_glue _ _ _ hg]
apply ht hg _ hf
· intro y hy
apply hU.isSeparatedFor.ext
intro Y f hf
apply (hB hf).isSeparatedFor.ext
intro Z g hg
rw [← FunctorToTypes.map_comp_apply, ← op_comp, hy _ (Presieve.bind_comp _ _ hg), hU.valid_glue _ _ hf, ht hf _ hg]
