isZero_singularHomologyFunctor_of_totallyDisconnectedSpace

English

For n ≠ 0 and totally disconnected X, the nth singular homology vanishes (is zero).

Русский

Для n ≠ 0 и totally disconnected X, n-ая гомология тривиальна (равна 0).

LaTeX

$$$$ n \ne 0 \Rightarrow IsZero( ((\mathrm{singularHomologyFunctor} C n).obj R).obj X) $$$$

Lean4

theorem isZero_singularHomologyFunctor_of_totallyDisconnectedSpace (hn : n ≠ 0) :
    IsZero (((singularHomologyFunctor C n).obj R).obj X) :=
  have := hasCoproducts_shrink.{0, w} (C := C)
  have : HasZeroObject C := ⟨_, initialIsInitial.isZero⟩
  (singularChainComplexFunctor_exactAt_of_totallyDisconnectedSpace C n R X hn).isZero_homology

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