instHasIterationOfShapeArrow — Mathlib

English

If J is a linear order with an iteration of shape J for C, then the Arrow category (category of morphisms in C) also has iteration of shape J.

Русский

Если J задаёт форму итерации для C, то категория стрелок Arrow C также имеет итерацию формы J.

LaTeX

$$$\text{HasIterationOfShape}(J, \mathrm{Arrow}(C))$$$

Lean4

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

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