mono_of_source_iso_zero

Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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