unop_mono_iff

Mathlib.CategoryTheory.EpiMono

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

English

For objects in the opposite category, Mono(f.unop) iff Epi(f).

Русский

Для объектов в противоположной категории: Mono(f.unop) равносильно Epi(f).

LaTeX

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

Lean4

@[simp]
theorem unop_mono_iff {X Y : Cᵒᵖ} (f : X ⟶ Y) : Mono f.unop ↔ Epi f :=
  ⟨fun _ ↦ op_epi_of_mono f.unop, fun _ ↦ inferInstance⟩

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

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

Разделы

Аффилиация

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