injective_eq_monomorphisms — Mathlib

English

Let C be a concrete category whose forgetful functor preserves monomorphisms. Then a morphism f in C is injective on the underlying sets if and only if f is a monomorphism in C.

Русский

Пусть C — конкретная категория, для которой забывательный функтор сохраняет мономорфизмы. Тогда морфизм f в C инъективен по основанным множествам тогда и только тогда, когда он является мономорфизмом в C.

LaTeX

$$$\\operatorname{MorphismProperty.injective}(C) = \\operatorname{monomorphisms}(C).$$$

Lean4

theorem injective_eq_monomorphisms [(forget C).PreservesMonomorphisms] :
    MorphismProperty.injective C = monomorphisms C :=
  by
  rw [injective_eq_monomorphisms_iff]
  infer_instance

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