instPreservesLimitsObjects — Mathlib

English

The functor Cat.objects preserves all small limits: the limit of a diagram of categories corresponds to the limit of the underlying structures.

Русский

Функтор Cat.objects сохраняет все малые пределы: предел диаграммы категорий соответствует пределу их подлежащих структур.

LaTeX

$$$$\\operatorname{PreservesLimits}(\\mathrm{Cat.objects}).$$$$

Lean4

instance : PreservesLimits Cat.objects.{v, v} where
  preservesLimitsOfShape :=
    {
      preservesLimit := fun {F} =>
        preservesLimit_of_preserves_limit_cone (HasLimits.limitConeIsLimit F)
          (Limits.IsLimit.ofIsoLimit (limit.isLimit (F ⋙ Cat.objects)) (Cones.ext (by rfl) (by cat_disch))) }

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