zeroIsoInitial_hom

Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

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

English

For a terminal object X, the morphism from the zero object to X is zero.

Русский

Для терминального объекта X морфизм от нулевого объекта к X равен нулю.

LaTeX

$$HasTerminal X \Rightarrow (zeroIsoTerminal t).hom = 0$$

Lean4

@[simp]
theorem zeroIsoInitial_hom [HasInitial C] : zeroIsoInitial.hom = (0 : 0 ⟶ ⊥_ C) := by ext

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

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

Разделы

Аффилиация

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