isColimit₁ — Mathlib

English

If the CostructuredArrow yoneda A is filtered and finally small, then A is an Ind-object.

Русский

Если CostructuredArrow yoneda A фильтрован и finally small, то A является Ind-объектом.

LaTeX

$$$\mathrm{IsFiltered}(\mathrm{CostructuredArrow}(\mathrm{yoneda},A)) \land \mathrm{FinallySmall}(\mathrm{CostructuredArrow}(\mathrm{yoneda},A)) \Rightarrow \mathrm{IsIndObject}(A)$$$

Lean4

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

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