epi_of_target_iso_zero

Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.epi_of_target_iso_zero

← MathLib Explorer

English

If f: X → Y and Y is isomorphic to the zero object, then f is epic.

Русский

Если f: X → Y и Y изоморфен нулевому объекту, то f эпиморфизм.

LaTeX

$$$\forall X,Y:\, C,\ \forall f:X\to Y,\forall i:Y\cong 0,\ Epi\ f$$$

Lean4

theorem epi_of_target_iso_zero {X Y : C} (f : X ⟶ Y) (i : Y ≅ 0) : Epi f :=
  ⟨fun {Z} g h _ => by rw [zero_of_source_iso_zero g i, zero_of_source_iso_zero h i]⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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