instMonoι — Mathlib

English

For any morphism f: G → H in ModuleCat R, the inclusion map image f → H is a monomorphism.

Русский

Для любой стрелки f: G → H в категории модулей над кольцом R, включение изображения image f → H является мономорфизмом.

LaTeX

$$$\\operatorname{Mono}(\\mathrm{image.ι}_f)$$$

Lean4

instance : Mono (image.ι f) :=
  ConcreteCategory.mono_of_injective (image.ι f) Subtype.val_injective

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