instSmallHomOfLocallySmall

Mathlib.CategoryTheory.EssentiallySmall

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

English

If C is LocallySmall and F: C → D, then for all X,Y, the morphism set Hom_C(X,Y) is small.

Русский

Если C локально малый и F: C → D, тогда для любых X,Y множество мороморфизмов Hom_C(X,Y) малое.

LaTeX

$$$\forall X,Y,\operatorname{Small}(\mathrm{Hom}_C(X,Y))$$$

Lean4

instance (C : Type u) [Category.{v} C] [LocallySmall.{w} C] (X Y : C) : Small.{w, v} (X ⟶ Y) :=
  LocallySmall.hom_small X Y

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

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

Разделы

Аффилиация

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