isSheaf_iso_iff — Mathlib

English

If α: F ≅ G is an isomorphism of presheaves and F is a sheaf, then G is a sheaf (transfer of the sheaf property along isomorphisms).

Русский

Если α: F ≅ G — изоморфизм прешрафов и F — она sheaf, тогда G тоже является sheaf (перенос свойства через изоморфизм).

LaTeX

$$$ F.IsSheaf \Rightarrow G.IsSheaf \quad \text{for } \alpha: F \cong G. $$$

Lean4

theorem isSheaf_iso_iff {F G : Presheaf C X} (α : F ≅ G) : F.IsSheaf ↔ G.IsSheaf :=
  Presheaf.isSheaf_of_iso_iff α

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