mem_homologicalKernel_iff — Mathlib

English

For an appropriate shift structure, F.homologicalKernel X is equivalent to IsZero (F.shift n).obj X for all n.

Русский

При наличии структуры сдвига F.homologicalKernel X эквивалентно IsZero (F.shift n).obj X для всех n.

LaTeX

$$$F.homologicalKernel X \\iff \\forall n, IsZero((F.shift n).obj X)$$$

Lean4

theorem mem_homologicalKernel_iff [F.ShiftSequence ℤ] (X : C) :
    F.homologicalKernel X ↔ ∀ (n : ℤ), IsZero ((F.shift n).obj X) := by
  simp only [← fun (n : ℤ) => Iso.isZero_iff ((F.isoShift n).app X), homologicalKernel, comp_obj]

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