isColimit₂ — Mathlib

English

There is a LocallySmall structure on the full subcategory of Ind-objects.

Русский

Существует структура локально малой размерности на полной подкатегории Ind-объектов.

LaTeX

$$$\mathrm{LocallySmall}\big(\mathrm{ObjectProperty.FullSubcategory}(\mathrm{IsIndObject}(C))\big)$$$

Lean4

/-- Implementation; see `nonempty_indParallelPairPresentation`. -/
noncomputable abbrev isColimit₂ : IsColimit (Cocone.mk B (ι₂ f g P₁ P₂)) :=
  (Functor.Final.isColimitWhiskerEquiv _ _).symm P₂.isColimit

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