instSmallHomFunctorOppositeTypeColimitCompYoneda

Mathlib.CategoryTheory.Limits.Indization.LocallySmall

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

English

There is a smallness instance for the Hom-objects from the colimit of F ⋙ yoneda to G.

Русский

Существует экземпляр малого объекта для гом-функтора: Colimit(F ⋙ yoneda) ⟶ G.

LaTeX

$$$\mathrm{Small}(\mathrm{Functor\_Hom}\big(\mathrm{colimit}(F\cdot\mathrm{yoneda}), G\big))$$$

Lean4

instance : Small.{v} (colimit (F ⋙ yoneda) ⟶ G) where equiv_small := ⟨_, ⟨colimitYonedaHomEquiv F G⟩⟩

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

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

Разделы

Аффилиация

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