op_epi_of_mono

Mathlib.CategoryTheory.EpiMono

URI: https://scilib.ai/kg/mathlib#CategoryTheory.op_epi_of_mono

English

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

Русский

Если f моно в C, то f^{op} — эпиморфизм в C^{op}. Обратное: эпиморфизм f^{op} даёт моно f.

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru