preservesLimits_diagramFunctor — Mathlib

English

The diagram functor J.diagramFunctor D X preserves limits of shape K, given the multiequalizers along covers exist.

Русский

Диаграммный функтор J.diagramFunctor D X сохраняет пределы формы K при условии существования мультиравнителей вдоль покрытий.

LaTeX

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

Lean4

instance preservesLimits_diagramFunctor (X : C) [HasLimitsOfSize.{max t u v, max t u v} D] :
    PreservesLimits (J.diagramFunctor D X) := by
  constructor
  intro _ _
  apply preservesLimitsOfShape_diagramFunctor.{max t u v}

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