instHasIterationOfShapeFunctor — Mathlib

English

If J has a linear order and C a category, then the functor category Functor(K, C) has iteration of shape J whenever C has iteration of shape J.

Русский

Если J задаёт линейный порядок, а C — категория, то множество категорий функций Functor(K, C) имеет итерацию формы J тогда, когда C имеет итерацию формы J.

LaTeX

$$$\mathrm{HasIterationOfShape}(J, \mathrm{Functor}(K, C))$$$

Lean4

instance : HasIterationOfShape J (K ⥤ C) where
  hasColimitsOfShape_of_isSuccLimit j
    hj := by
    have := hasColimitsOfShape_of_isSuccLimit C j hj
    infer_instance

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