exact₀ — Mathlib

English

For an injective resolution I of Z, the induced three-term complex built from I is exact at the leftmost position.

Русский

Для разрешения инъективного I объекта Z получаемая трёхчленная комплексная структура точна в левой позиции.

LaTeX

$$$\text{Exact}_0\left( I \right)$$$

Lean4

theorem exact₀ {Z : C} (I : InjectiveResolution Z) : (ShortComplex.mk _ _ I.ι_f_zero_comp_complex_d).Exact :=
  ShortComplex.exact_of_f_is_kernel _ I.isLimitKernelFork

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