mono_iff_injective_of_preservesPullback

English

Under preservation of limits of shape WalkingCospan by the forgetful functor, a morphism f is a monomorphism if and only if its underlying map is injective.

Русский

При сохранении забывающим функтором пределов формы WalkingCospan морфизм f является мономорфизмом тогда и только тогда, когда его базовая функция инъективна.

LaTeX

$$$\\operatorname{Mono}(f) \\iff \\operatorname{Injective}((\\mathrm{forget}\\,C).map\\ f)$$$

Lean4

theorem mono_iff_injective_of_preservesPullback {X Y : C} (f : X ⟶ Y)
    [PreservesLimitsOfShape WalkingCospan (forget C)] : Mono f ↔ Function.Injective f :=
  ((forget C).mono_map_iff_mono _).symm.trans (mono_iff_injective _)

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