preservesLimitsOfShape_diagramFunctor

English

Assuming the index category has multiequalizers for all covers, the diagram functor preserves limits of shape K.

Русский

При этом для каждого покрытия имеется мультиравнитель, диаграммный функтор сохраняет пределы формы K.

LaTeX

$$$ \\text{PreservesLimitsOfShape } K \\,(J. diagramFunctor D X) $$$

Lean4

instance preservesLimitsOfShape_diagramFunctor (X : C) (K : Type s) [SmallCategory K] [HasLimitsOfShape K D] :
    PreservesLimitsOfShape K (J.diagramFunctor D X) :=
  ⟨by apply preservesLimit_diagramFunctor.{s, t, w, v, u}⟩

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