isSheaf_of_nat_equiv — Mathlib

English

Let J be a Grothendieck topology on a category C. If two presheaves P1 and P2 are naturally equivalent objectwise (via an equiv e on each X in C) and the equiv is compatible with all structure maps (he), then whenever P1 is a sheaf for J, P2 is also a sheaf for J.

Русский

Пусть J — топология Гротендика на категорию C. Если два преслежи P1 и P2 эквивалентны на каждом объекте X в C через естественное эквивалентное отображение e, и эта эквивалентность совместима со отображениями P1 и P2, то если P1 является sheaf для J, то и P2 является sheaf для J.

LaTeX

$$$\mathrm{IsSheaf}(J,P_1) \Rightarrow \mathrm{IsSheaf}(J,P_2)$$$

Lean4

theorem isSheaf_of_nat_equiv (hP₁ : Presieve.IsSheaf J P₁) : Presieve.IsSheaf J P₂ := fun _ R hR ↦
  isSheafFor_of_nat_equiv e he (hP₁ R hR)

Похожие утверждения