instPreservesColimitEval — Mathlib

English

For every i, evaluation at i preserves colimits of diagrams F: J ⥤ HomologicalComplex C c.

Русский

Для каждого i функция оценки сохраняет колимиты диаграмм F: J ⥤ HomologicalComplex C c.

LaTeX

$$$ \forall n, \mathrm{PreservesColimit}(F, \mathrm{eval}_{n}). $$$

Lean4

noncomputable instance (n : ι) : PreservesColimit F (eval C c n) :=
  preservesColimit_of_preserves_colimit_cocone (isColimitCoconeOfHasColimitEval F) (colimit.isColimit _)

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