wellPowered_moduleCat

Mathlib.Algebra.Category.ModuleCat.Subobject

URI: https://scilib.ai/kg/mathlib#ModuleCat.wellPowered_moduleCat

English

ModuleCat R is well-powered; subobjects form a set for each object.

Русский

Категория ModuleCat R хорошо порождается; подобъекты образуют множество для каждого объекта.

LaTeX

$$$\text{WellPowered}(\mathrm{ModuleCat}\;R)$$$

Lean4

instance wellPowered_moduleCat : WellPowered.{v} (ModuleCat.{v} R) :=
  ⟨fun M => ⟨⟨_, ⟨(subobjectModule M).toEquiv⟩⟩⟩⟩

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

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

Разделы

Аффилиация

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