instHasHomologyNatObjAlternatingConst

English

Even-case iso at level j between alternatingConst and ShortComplex with ψ, φ.

Русский

Чётный случай на уровне j между alternatingConst и гомологией короткого комплекса ψ, φ.

LaTeX

$$$\text{AltConstHomologyIsoEven}(A, hOdd, hEven, hc).homology\, j \cong \mathrm{ShortComplex.mk}\; ψ\; φ\; hEven$.homology$$

Lean4

instance (X : C) (n : ℕ) : (alternatingConst.obj X).HasHomology n :=
  by
  rcases n.even_or_odd with h | h
  · rcases n with - | n
    · exact ⟨⟨alternatingConstHomologyDataZero X _ rfl⟩⟩
    · exact ⟨⟨alternatingConstHomologyDataEvenNEZero X _ h (by simp)⟩⟩
  · exact ⟨⟨alternatingConstHomologyDataOdd X _ h⟩⟩

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