unop_epi_iff

Mathlib.CategoryTheory.EpiMono

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

English

Analogous statement: Epi(f.unop) iff Mono(f).

Русский

Аналогично: Epi(f.unop) тогда и только тогда, когда Mono(f).

LaTeX

$$$ Epi(f.unop) \\iff Mono(f) $$$

Lean4

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

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

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

Разделы

Аффилиация

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