alternatingConstHomologyDataEvenNEZero

English

For every object X and every natural number n, the alternatingConst.obj X has a homology object at degree n (i.e., a homology theory exists for all degrees).

Русский

Для каждого объекта X и каждого натурального n существует гамомология объекта в степени n для alternatingConst.obj X.

LaTeX

$$$\forall X\forall n\; (\text{AltConst.obj } X).HasHomology\, n$$$

Lean4

/-- The `n`-th homology of the alternating constant complex is zero for non-zero even `n`. -/
noncomputable def alternatingConstHomologyDataEvenNEZero (X : C) (n : ℕ) (hn : Even n) (h₀ : n ≠ 0) :
    ((alternatingConst.obj X).sc n).HomologyData :=
  .ofIsLimitKernelFork _ (by simp [Nat.even_add_one, hn]) _ (Limits.zeroKernelOfCancelZero _ (by cases n <;> simp_all))

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