Lean4
/-- If a presieve `R` on `X` has a subsieve `S` such that:
* `P` is a sheaf for `S`.
* For every `f` in `R`, `P` is separated for the pullback of `S` along `f`,
then `P` is a sheaf for `R`.
This is closely related to [Elephant] C2.1.6(i).
-/
theorem isSheafFor_subsieve_aux (P : Cᵒᵖ ⥤ Type w) {S : Sieve X} {R : Presieve X} (h : (S : Presieve X) ≤ R)
(hS : IsSheafFor P (S : Presieve X))
(trans : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (S.pullback f : Presieve Y)) : IsSheafFor P R :=
by
rw [← isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor]
constructor
· intro x t₁ t₂ ht₁ ht₂
exact hS.isSeparatedFor _ _ _ (isAmalgamation_restrict h x t₁ ht₁) (isAmalgamation_restrict h x t₂ ht₂)
· intro x hx
use hS.amalgamate _ (hx.restrict h)
intro W j hj
apply (trans hj).ext
intro Y f hf
rw [← FunctorToTypes.map_comp_apply, ← op_comp, hS.valid_glue (hx.restrict h) _ hf, FamilyOfElements.restrict, ←
hx (𝟙 _) f (h _ hf) _ (id_comp _)]
simp
