map_zero

Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.map_zero

English

If F is a left adjoint, then F preserves zero morphisms.

Русский

Если F имеет левого сопряженного, то F сохраняет нулевые morphisms.

LaTeX

$$$(\text{IsLeftAdjoint } F) \Rightarrow \PreservesZeroMorphisms F$$$

Lean4

@[simp]
protected theorem map_zero (F : C ⥤ D) [PreservesZeroMorphisms F] (X Y : C) : F.map (0 : X ⟶ Y) = 0 :=
  PreservesZeroMorphisms.map_zero _ _

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

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

Разделы

Аффилиация

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