instHasHomology — Mathlib

English

If K has homology at each degree, then K extend e also has homology at the corresponding degrees j'.

Русский

Если у K есть гомология на каждом уровне, то у K, расширенного вдоль e, она есть на соответствующих степенях j'.

LaTeX

$$HasHomology (K.extend e) j'$$

Lean4

instance [∀ j, K.HasHomology j] (j' : ι') : (K.extend e).HasHomology j' :=
  by
  by_cases h : ∃ j, e.f j = j'
  · obtain ⟨j, rfl⟩ := h
    infer_instance
  · have hj := isZero_extend_X K e j' (by tauto)
    exact ShortComplex.HasHomology.mk' (ShortComplex.HomologyData.ofZeros _ (hj.eq_of_tgt _ _) (hj.eq_of_src _ _))

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