preserveFiniteLimits_plusFunctor — Mathlib

English

The plus-functor preserves finite limits under suitable hypotheses on forgetful functors and smallness of covers.

Русский

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

LaTeX

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

Lean4

instance preserveFiniteLimits_plusFunctor [HasFiniteLimits D] [PreservesFiniteLimits (forget D)]
    [(forget D).ReflectsIsomorphisms] : PreservesFiniteLimits (J.plusFunctor D) :=
  by
  apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{t}
  intro K _ _
  have : ReflectsLimitsOfShape K (forget D) := reflectsLimitsOfShape_of_reflectsIsomorphisms
  apply preservesLimitsOfShape_plusFunctor

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