zero_of_source_iso_zero'

Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

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

English

If a morphism f: X → Y has Y isomorphic to the zero object, then f is the zero morphism.

Русский

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

LaTeX

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

Lean4

theorem zero_of_source_iso_zero' {X Y : C} (f : X ⟶ Y) (i : IsIsomorphic X 0) : f = 0 :=
  zero_of_source_iso_zero f (Nonempty.some i)

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

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

Разделы

Аффилиация

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