op_mono_of_epi — Mathlib

English

A dual property: if f is epi in C, then f^{op} is mono in C^{op}. The converse holds as well.

Русский

Двойственное свойство: если f — эпиморфизм в C, то f^{op} — мономорфизм в C^{op}. Обратное также верно.

LaTeX

$$$ Mono(f^{op}) \\iff Epi(f) $$$

Lean4

instance op_mono_of_epi {A B : C} (f : A ⟶ B) [Epi f] : Mono f.op :=
  ⟨fun _ _ eq => Quiver.Hom.unop_inj ((cancel_epi f).1 (Quiver.Hom.op_inj eq))⟩

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