instFunctor

Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

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

← MathLib Explorer

English

If C has a zero object, then for any B the functor category B ⥤ C has a zero object.

Русский

Если в C есть нулевой объект, то категория функций B ⥤ C имеет нулевой объект.

LaTeX

$$HasZeroObject C \Rightarrow HasZeroObject (B ⥤ C)$$

Lean4

instance {B : Type*} [Category B] : HasZeroObject (B ⥤ C) :=
  (((CategoryTheory.Functor.const B).obj (0 : C)).isZero fun _ => isZero_zero _).hasZeroObject

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

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

Разделы

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

Аффилиация

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