English
If two presheaves P1 and P2 are naturally equivalent via e, and P1 is a sheaf for R, then P2 is a sheaf for R.
Русский
Если P1 и P2 естественно эквивалентны через e, и P1 является sheaf для R, то P2 также является sheaf для R.
LaTeX
$$isSheafFor_of_nat_equiv {P1} {P2} (e) (he) {X} {R} (hP1) : IsSheafFor P2 R$$
Lean4
/-- C2.1.3 in [Elephant] -/
theorem isSheafFor_iff_generate (R : Presieve X) : IsSheafFor P R ↔ IsSheafFor P (generate R : Presieve X) :=
by
rw [← isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor]
rw [← isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor]
rw [← isSeparatedFor_iff_generate]
apply and_congr (Iff.refl _)
constructor
· intro q x hx
apply Exists.imp _ (q _ (hx.restrict (le_generate R)))
intro t ht
simpa [hx] using isAmalgamation_sieveExtend _ _ ht
· intro q x hx
apply Exists.imp _ (q _ hx.sieveExtend)
intro t ht
simpa [hx] using isAmalgamation_restrict (le_generate R) _ _ ht
