isSheaf_iff_isSheafUniqueGluing — Mathlib

English

Under a forgetful functor that reflects isomorphisms and preserves limits, the pair IsSheaf and IsSheafUniqueGluing are equivalent.

Русский

При любом забывающем функторе, сохраняющем предельные объекты и отражающем изоморфизмы, IsSheaf и IsSheafUniqueGluing эквивалентны.

LaTeX

$$$$\text{IsSheaf } F \iff \text{IsSheafUniqueGluing } F,$$$$

Lean4

/-- For presheaves valued in a concrete category, whose forgetful functor reflects isomorphisms and
preserves limits, the sheaf condition in terms of unique gluings is equivalent to the usual one.
-/
theorem isSheaf_iff_isSheafUniqueGluing : F.IsSheaf ↔ F.IsSheafUniqueGluing :=
  Iff.trans (isSheaf_iff_isSheaf_comp' (forget C) F) (isSheaf_iff_isSheafUniqueGluing_types (F ⋙ forget C))

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