ι₂ — Mathlib

English

Ind-objects are equivalent to having filtered plus FinallySmall costructured arrows via Yoneda.

Русский

Ind-объекты эквивалентны условию: существует фильтрованность и FinallySmall для CostructuredArrow через Yoneda.

LaTeX

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

Lean4

/-- Implementation; see `nonempty_indParallelPairPresentation`. -/
abbrev ι₂ : F₂ f g P₁ P₂ ⋙ yoneda ⟶ (Functor.const (K f g P₁ P₂)).obj B :=
  whiskerLeft (Comma.snd _ _) P₂.ι

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