injective_of_mono_of_preservesPullback

English

If f is a monomorphism in a concrete category C and the forgetful functor preserves pullbacks (limits of shape WalkingCospan), then the underlying function of f is injective.

Русский

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

LaTeX

$$$\\operatorname{Mono}(f) \\Rightarrow \\operatorname{Injective}(\\underline{f})$$$

Lean4

theorem injective_of_mono_of_preservesPullback {X Y : C} (f : X ⟶ Y) [Mono f]
    [PreservesLimitsOfShape WalkingCospan (forget C)] : Function.Injective f :=
  (mono_iff_injective ((forget C).map f)).mp inferInstance

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