English
Let R and S be sieves on X. If P is a sheaf for R, P is separated for pullbacks along arrows in S, and P is a sheaf for the pullbacks of S along arrows in R, then P is a sheaf for S.
Русский
Пусть R и S — сивы на X. Если P — шейф для R, P разделяется по pullback-умножениям вдоль стрелок в S, и P является шейфом для вытягиваний pullback S вдоль стрелок в R, тогда P является шейфом для S.
LaTeX
$$$\Presieve.IsSheafFor P (S : Presieve X)$$$
Lean4
/-- Given two sieves `R` and `S`, to show that `P` is a sheaf for `S`, we can show:
* `P` is a sheaf for `R`
* `P` is a sheaf for the pullback of `S` along any arrow in `R`
* `P` is separated for the pullback of `R` along any arrow in `S`.
This is mostly an auxiliary lemma to construct `finestTopology`.
Adapted from [Elephant], Lemma C2.1.7(ii) with suggestions as mentioned in
https://math.stackexchange.com/a/358709
-/
theorem isSheafFor_trans (P : Cᵒᵖ ⥤ Type v) (R S : Sieve X) (hR : Presieve.IsSheafFor P (R : Presieve X))
(hR' : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (_ : S f), Presieve.IsSeparatedFor P (R.pullback f : Presieve Y))
(hS : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (_ : R f), Presieve.IsSheafFor P (S.pullback f : Presieve Y)) :
Presieve.IsSheafFor P (S : Presieve X) :=
by
have : (bind R fun Y f _ => S.pullback f : Presieve X) ≤ S :=
by
rintro Z f ⟨W, f, g, hg, hf : S _, rfl⟩
apply hf
apply Presieve.isSheafFor_subsieve_aux P this
· apply isSheafFor_bind _ _ _ hR hS
intro Y f hf Z g
rw [← pullback_comp]
apply (hS (R.downward_closed hf _)).isSeparatedFor
· intro Y f hf
have : Sieve.pullback f (bind R fun T (k : T ⟶ X) (_ : R k) => pullback k S) = R.pullback f :=
by
ext Z g
constructor
· rintro ⟨W, k, l, hl, _, comm⟩
rw [pullback_apply, ← comm]
simp [hl]
· intro a
refine ⟨Z, 𝟙 Z, _, a, ?_⟩
simp [hf]
rw [this]
apply hR' hf
