preservesColimitsOfSize_subsingleton

English

For any functor F, the property PreservesColimitsOfSize F is a subsingleton: at most one witness that F preserves colimits of all shapes up to a given size.

Русский

Для любого функторa PreservesColimitsOfSize F является пододном: не более одного свидетельства сохранения колимит всех форм вплоть до заданного размера.

LaTeX

$$$$\operatorname{Subsingleton}(\mathrm{PreservesColimitsOfSize} F).$$$$

Lean4

instance preservesColimitsOfSize_subsingleton (F : C ⥤ D) : Subsingleton (PreservesColimitsOfSize.{w', w} F) := by
  constructor; rintro ⟨a⟩ ⟨b⟩; congr!

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