hasColimitsOfShape_thinSkeleton — Mathlib

English

If a category C has all colimits of shape J, then its thin skeleton also has all colimits of shape J; the colimits in the thin skeleton are obtained by transporting along the inclusion from ThinSkeleton C.

Русский

Если категория C имеет все колимиты по форме J, то и тонкая скелетная категория ThinSkeleton(C) имеет такие же колимиты; колимиты в тонкой скелетной сохраняются через включение из ThinSkeleton C.

LaTeX

$$$\mathrm{HasColimitsOfShape}(J,C) \Rightarrow \mathrm{HasColimitsOfShape}(J,\mathrm{ThinSkeleton}(C))$$$

Lean4

instance hasColimitsOfShape_thinSkeleton [HasColimitsOfShape J C] : HasColimitsOfShape J (ThinSkeleton C) :=
  hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape (fromThinSkeleton C)

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