instFinitaryExtensiveSheafOfHasPullbacksOfHasSheafify

English

If forgetful functors preserve and reflect limits, then sheafification preserves finite limits.

Русский

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

LaTeX

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

Lean4

instance [FinitaryExtensive D] [HasPullbacks D] [HasSheafify J D] : FinitaryExtensive (Sheaf J D) :=
  finitaryExtensive_of_reflective (sheafificationAdjunction _ _)

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