instHasSeparatorModuleCatOfSmall

Mathlib.Algebra.Category.ModuleCat.AB

URI: https://scilib.ai/kg/mathlib#instHasSeparatorModuleCatOfSmall

English

If R is small, ModuleCat R has a separator (as a consequence of smallness).

Русский

Если R мал, у ModuleCat R существует разделитель.

LaTeX

$$$\operatorname{Small}(R) \Rightarrow \operatorname{HasSeparator}(\mathrm{ModuleCat}(R))$$$

Lean4

instance [Small.{v} R] : HasSeparator (ModuleCat.{v} R) where
  hasSeparator := ⟨ModuleCat.of R (Shrink.{v} R), ModuleCat.isSeparator R⟩

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

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

Разделы

Аффилиация

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