preservesLimitsOfShape_sheafification

English

For any category D with finite limits, the sheafification functor preserves finite limits when it is built from plus-plus constructions and forgetful functors reflect isomorphisms.

Русский

Для любой категории D с конечными пределами функция sheafification сохраняет конечные пределы, если она строится из конструкций плюс-плюс и забывающие функторы отражают изоморфизмы.

LaTeX

$$$ \\text{PreservesFiniteLimits (J.sheafification D)} $$$

Lean4

instance preservesLimitsOfShape_sheafification (K : Type t) [SmallCategory K] [FinCategory K] [HasLimitsOfShape K D]
    [PreservesLimitsOfShape K (forget D)] [ReflectsLimitsOfShape K (forget D)] :
    PreservesLimitsOfShape K (J.sheafification D) :=
  Limits.comp_preservesLimitsOfShape _ _

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