id_nonzero

Mathlib.CategoryTheory.Simple

URI: https://scilib.ai/kg/mathlib#CategoryTheory.id_nonzero

English

In a simple object X, the identity morphism 𝟙_X is nonzero.

Русский

Для простого объекта X тождественный морфизм 𝟙_X не равен нулю.

LaTeX

$$$ 𝟙_X \neq 0. $$$

Lean4

theorem id_nonzero (X : C) [Simple.{v} X] : 𝟙 X ≠ 0 :=
  (Simple.mono_isIso_iff_nonzero (𝟙 X)).mp (by infer_instance)

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

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

Разделы

Аффилиация

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