isSheaf_iff_isSheaf_comp — Mathlib

English

A presheaf is a sheaf iff its composition with a forgetful functor is a sheaf.

Русский

Прешейф является шейфом тогда и только тогда, когда композиция с забывающим функтором тоже является шейфом.

LaTeX

$$$\\text{IsSheaf } F \\iff \\text{IsSheaf } (F \\circ G)$$$

Lean4

theorem isSheaf_iff_isSheaf_comp {C : Type u₁} [Category.{v} C] {D : Type u₂} [Category.{v} D] (G : C ⥤ D)
    [G.ReflectsIsomorphisms] [HasLimits C] [PreservesLimits G] {X : TopCat.{v}} (F : Presheaf C X) :
    Presheaf.IsSheaf F ↔ Presheaf.IsSheaf (F ⋙ G) :=
  isSheaf_iff_isSheaf_comp' G F

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