mono_of_mono_map — Mathlib

English

If F reflects monomorphisms, a mono in the target implies a mono in the domain.

Русский

Если F отражает моно, монообраз в образе F отражается обратно – это моно в исходном объекте.

LaTeX

$$[F.ReflectsMonomorphisms] ⇒ [Mono (F.map f) ⇒ Mono f]$$

Lean4

theorem mono_of_mono_map (F : C ⥤ D) [ReflectsMonomorphisms F] {X Y : C} {f : X ⟶ Y} (h : Mono (F.map f)) : Mono f :=
  ReflectsMonomorphisms.reflects f h

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