isIndObject_yoneda — Mathlib

English

Representable presheaves are ind-objects. For every object X in C, the presheaf yoneda.obj X is an Ind-object.

Русский

Представимые прешепафеты являются индуктивными объектами. Пусть X — объект в C; presheaf yoneda.obj X является Ind-объектом.

LaTeX

$$$\forall X\in \mathrm{Obj}(C),\ \mathrm{IsIndObject}(\mathrm{yoneda.obj} X)$$$

Lean4

/-- Representable presheaves are (trivially) ind-objects. -/
theorem isIndObject_yoneda (X : C) : IsIndObject (yoneda.obj X) :=
  .mk <| IndObjectPresentation.yoneda X

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