English
If n ≠ 0 and space X is totally disconnected, then the nth level of the singular chain complex is exact at n.
Русский
Если n ≠ 0 и пространство X totally disconnected, то цепной комплекс имеет точность на уровне n.
LaTeX
$$$$ n \ne 0 \quad\Rightarrow\quad \text{ExactAt}(((\mathrm{singularChainComplexFunctor} C).obj R).obj X) n $$$$
Lean4
theorem singularChainComplexFunctor_exactAt_of_totallyDisconnectedSpace (hn : n ≠ 0) :
(((singularChainComplexFunctor C).obj R).obj X).ExactAt n :=
have := hasCoproducts_shrink.{0, w} (C := C)
have : HasZeroObject C := ⟨_, initialIsInitial.isZero⟩
.of_iso (ChainComplex.alternatingConst_exactAt _ _ hn)
(singularChainComplexFunctorIsoOfTotallyDisconnectedSpace C R X).symm
