hasZeroObject_unop

Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

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

English

If Cᵒᵖ has a zero object, then C has a zero object.

Русский

Если Cᵒᵖ имеет нулевой объект, то и в C есть нулевой объект.

LaTeX

$$$\\\\text{HasZeroObject}(C)\\Leftarrow \\text{HasZeroObject}(C^{op})$$$

Lean4

theorem hasZeroObject_unop [HasZeroObject Cᵒᵖ] : HasZeroObject C :=
  ⟨⟨Opposite.unop 0, IsZero.unop (isZero_zero Cᵒᵖ)⟩⟩

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

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

Разделы

Аффилиация

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