preservesZeroMorphisms_comp

Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero

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

← MathLib Explorer

English

If F1 ≅ F2 are isomorphic functors, then F2 preserves zero morphisms.

Русский

Если F1 и F2 изоморфны как функторы, то F2 сохраняет нулевые морфизмы.

LaTeX

$$$F_1 \cong F_2 \Rightarrow \PreservesZeroMorphisms F_2$$$

Lean4

instance preservesZeroMorphisms_comp (F : C ⥤ D) (G : D ⥤ E) [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] :
    (F ⋙ G).PreservesZeroMorphisms :=
  ⟨by simp⟩

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

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

Разделы

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

Аффилиация

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