English
If a presheaf P is a sheaf for every pullback of a sieve S and S is contained in a presieve R, then P is a sheaf for R.
Русский
Если наива P является sheaf для каждого вытянутого обратно шару-Spullback-образа, и если из S ⊆ R, то P является sheaf для R.
LaTeX
$$$ ( \forall f, \ IsSheafFor P (S \!\! \pullback f)) \land (S \le R) \Rightarrow \mathrm{IsSheafFor}(P,R) $$$
Lean4
/-- If `P` is a sheaf for every pullback of the sieve `S`, then `P` is a sheaf for any presieve which
contains `S`.
This is closely related to [Elephant] C2.1.6.
-/
theorem isSheafFor_subsieve (P : Cᵒᵖ ⥤ Type w) {S : Sieve X} {R : Presieve X} (h : (S : Presieve X) ≤ R)
(trans : ∀ ⦃Y⦄ (f : Y ⟶ X), IsSheafFor P (S.pullback f : Presieve Y)) : IsSheafFor P R :=
isSheafFor_subsieve_aux P h (by simpa using trans (𝟙 _)) fun _ f _ => (trans f).isSeparatedFor
