op_epi_iff

Mathlib.CategoryTheory.EpiMono

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

English

Symmetric statement to the previous one: Epi(f^{op}) iff Mono(f).

Русский

Симметричное тождество к предыдущему: Epi(f^{op}) тогда и только тогда, когда Mono(f).

LaTeX

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

Lean4

@[simp]
theorem op_epi_iff {X Y : C} (f : X ⟶ Y) : Epi f.op ↔ Mono f :=
  ⟨fun _ ↦ unop_mono_of_epi f.op, fun _ ↦ inferInstance⟩

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

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

Разделы

Аффилиация

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