unop_epi_of_mono — Mathlib

English

If f is epi in C, then its opposite f^{op} is mono in C^{op}. Conversely, epi of f^{op} corresponds to mono of f.

Русский

Если f является эпиморфизмом в C, то его противоположность f^{op} является мономорфизмом в C^{op}. Обратное верно: эпиморфизм f^{op} соответствует мономорфизму f.

LaTeX

$$$ Epi(f) \\implies Mono(f^{op}) \\quad\\text{and}\\quad Mono(f) \\implies Epi(f^{op}). $$$

Lean4

instance unop_epi_of_mono {A B : Cᵒᵖ} (f : A ⟶ B) [Mono f] : Epi f.unop :=
  ⟨fun _ _ eq => Quiver.Hom.op_inj ((cancel_mono f).1 (Quiver.Hom.unop_inj eq))⟩

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