isSeparator_range_yoneda — Mathlib

English

For any category C, the Ind-object Yoneda embedding yields a separating coproduct: IsSeparator of the coproduct of Ind.yoneda.obj.

Русский

Для любой категории C вложение Yoneda через Ind образует сепараторный копроконкретный объект: IsSeparator у coproduct Ind.yoneda.obj.

LaTeX

$$$\mathrm{IsSeparator}(\bigoplus_{?} \mathrm{Ind.yoneda}.obj)$$$

Lean4

theorem isSeparator_range_yoneda : IsSeparator (∐ (Ind.yoneda : C ⥤ _).obj) :=
  Ind.isSeparating_range_yoneda.isSeparator_coproduct

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