evaluation_preservesFiniteColimits

English

For any X, the evaluation functor at X preserves finite colimits: evaluating a finite colimit diagram yields the finite colimit of evaluated diagrams.

Русский

Для любого X функтор вычисления по X сохраняет конечные колимиты: вычисление конечного колимитного диаграммы даёт конечный колимит вычисленных диаграмм.

LaTeX

$$$\\text{evaluation\\_preservesFiniteColimits}(X):\\; \\mathrm{PreservesFiniteColimits}(\\text{evaluation}(R,X))$$$

Lean4

noncomputable instance evaluation_preservesFiniteColimits (X : Cᵒᵖ) : PreservesFiniteColimits (evaluation.{v} R X) where

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