instPresheafIsFiniteObjFunctorOppositeTypeYoneda

Mathlib.CategoryTheory.Subpresheaf.Finite

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instPresheafIsFiniteObjFunctorOppositeTypeYoneda

English

For any object X, the Yoneda presheaf y_X is generated by the identity morphism at X.

Русский

Для каждого объекта X универсальный префешев: y_X порожден идентити-морфизмом на X.

LaTeX

$$PresheafIsGeneratedBy (yoneda.obj X) (\lambda _ => 𝟙 X)$$

Lean4

instance (X : C) : PresheafIsFinite (yoneda.obj X) :=
  (yoneda_obj_isGeneratedBy X).isFinite

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru