plusPlusFunctorIsoSheafification — Mathlib

English

Under suitable hypotheses, the plus-plus construction preserves finite limits.

Русский

При разумных предположениях конструкция плюс-плюс сохраняет конечные пределы.

LaTeX

$$$ \\text{PreservesFiniteLimits (CategoryTheory.plusPlusSheaf J D)} $$$

Lean4

/-- `plusPlusFunctor` is isomorphic to `sheafification`. -/
def plusPlusFunctorIsoSheafification : J.sheafification D ≅ sheafification J D :=
  Functor.isoWhiskerRight (plusPlusSheafIsoPresheafToSheaf J D) (sheafToPresheaf J D)

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