forget_preservesMonomorphisms — Mathlib

English

The forgetful functor Mod_R → Type preserves monomorphisms: mono f implies the underlying map is injective.

Русский

Забывающий сохранение мономорфизмов: если f моно в ModuleCat, то отображение инъективно.

LaTeX

$$$\\text{forget}(f)$ mono in Type ⟺ $f$ mono in ModuleCat; hence underlying map is injective.$$

Lean4

instance forget_preservesMonomorphisms : (forget (ModuleCat.{v} R)).PreservesMonomorphisms where
  preserves f
    hf := by
    rw [CategoryTheory.mono_iff_injective, ConcreteCategory.forget_map_eq_coe, ← mono_iff_injective]
    exact hf

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