hasHomology_sc'_of_not_mem_boundary

English

If j is not in the boundaryGE, then the short complex component (K.truncGE' e).sc' i j k has homology.

Русский

Если j не принадлежит границе BoundaryGE, то компонент sc' i j k в K.truncGE' e имеет гомологию.

LaTeX

$$$\bigl((K.\mathrm{truncGE}' e).\mathrm{sc}' i j k\bigr).\mathrm{HasHomology}$$$

Lean4

theorem hasHomology_sc'_of_not_mem_boundary (hj : ¬e.BoundaryGE j) : ((K.truncGE' e).sc' i j k).HasHomology :=
  by
  have : (K.restriction e).HasHomology j :=
    restriction.hasHomology K e i j k hi hk rfl rfl rfl (e.prev_f_of_not_boundaryGE hi hj) (e.next_f hk)
  have := ShortComplex.hasHomology_of_iso ((K.restriction e).isoSc' i j k hi hk)
  let φ := (shortComplexFunctor' C c i j k).map (K.restrictionToTruncGE' e)
  have : Epi φ.τ₁ := by dsimp [φ]; infer_instance
  have : IsIso φ.τ₂ := K.isIso_restrictionToTruncGE' e j hj
  have : IsIso φ.τ₃ := K.isIso_restrictionToTruncGE' e k (e.not_boundaryGE_next' hj hk)
  exact ShortComplex.hasHomology_of_epi_of_isIso_of_mono φ

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