English
There is a canonical successor structure on the functor Arrow C ⥤ Arrow C, obtained by iterating a natural transformation ε: 𝟭(Arrow C) ⟶ SmallObject.functor I.homFamily. This provides a systematic way to build successive stages of objects and morphisms in Arrow C.
Русский
Существует каноническая структура-последовательность на функторе Arrow C ⥤ Arrow C, получаемая путём итерации естественного преобразования ε: 𝟭(Arrow C) ⟶ SmallObject.functor I.homFamily. Это обеспечивает опорядоченный конструктор последовательных стадий объектов и морфизмов в Arrow C.
LaTeX
$$$\\text{succStruct}(I,\\kappa):\\mathrm{SuccStruct}(\\mathrm{Functor}(\\mathrm{Arrow}(C),\\mathrm{Arrow}(C)))$$$
Lean4
/-- The successor structure on `Arrow C ⥤ Arrow C` corresponding
to the iterations of the natural transformation
`ε : 𝟭 (Arrow C) ⟶ SmallObject.functor I.homFamily`
(see the file `SmallObject.Construction`). -/
noncomputable def succStruct : SuccStruct (Arrow C ⥤ Arrow C) :=
haveI := hasColimitsOfShape_discrete I κ
haveI := hasPushouts I κ
SuccStruct.ofNatTrans (ε I.homFamily)
