instHasZeroObject — Mathlib

English

The derived category D(C) has a zero object; there is a distinguished zero object that is initial and terminal.

Русский

Производная категория D(C) содержит нулевой объект; существует нулевой объект, который является и началом, и концом.

LaTeX

$$$\mathrm{HasZeroObject}(\mathrm{DerivedCategory}(\mathcal{C}))$$$

Lean4

noncomputable instance : HasZeroObject (DerivedCategory C) :=
  Q.hasZeroObject_of_additive

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