mono_as_hom'_subtype

Mathlib.Algebra.Category.ModuleCat.EpiMono

URI: https://scilib.ai/kg/mathlib#ModuleCat.mono_as_hom'_subtype

English

For any submodule U of X, the inclusion map U ↪ X is mono in ModuleCat.

Русский

Для любого подпространства U модуля X вложение U → X является моно в ModuleCat.

LaTeX

$$$\\text{ModuleCat.ofHom}(U.subtype)\\;\\text{is Mono}$$$

Lean4

instance mono_as_hom'_subtype (U : Submodule R X) : Mono (ModuleCat.ofHom U.subtype) :=
  (mono_iff_ker_eq_bot _).mpr (Submodule.ker_subtype U)

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

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

Разделы

Аффилиация

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