instIsStrictlySupportedOfNat — Mathlib

English

If there exists a zero object in the category, then the zero complex is strictly supported with respect to any embedding e.

Русский

Если существует нулевой объект в категории, то нулевой комплекс строго поддержан относительно любого вложения e.

LaTeX

$$IsStrictlySupported(0,e)$$

Lean4

instance [HasZeroObject C] : (0 : HomologicalComplex C c').IsStrictlySupported e where
  isZero i _ := (eval _ _ i).map_isZero (Limits.isZero_zero _)

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