singularChainComplexFunctor — Mathlib

English

If X is totally disconnected, the singular chain complex of X with coefficients in C is isomorphic to the alternating-const chain complex on the coproduct indexed by X, i.e., R[X] ⟵0- R[X] ⟵Id- R[X] ⟵0- R[X] …

Русский

Пусть X totally disconnected; цепной комплекс сингулярного гомолога X с коэффициентами в C изоморфен чередованию константного цепного комплекса на coproduct по X: R[X] ⟵0- R[X] ⟵Id- R[X] ⟵0- …

LaTeX

$$$((\text{singularChainComplexFunctor } C).\mathrm{obj} R).\mathrm{obj} X \cong (\text{ChainComplex.alternatingConst}.\mathrm{obj}(\bigoplus_{x\in X} R))$$$

Lean4

/-- The singular chain complex functor with coefficients in `C`. -/
def singularChainComplexFunctor : C ⥤ TopCat.{w} ⥤ ChainComplex C ℕ :=
  SSet.singularChainComplexFunctor.{w} C ⋙ (Functor.whiskeringLeft _ _ _).obj TopCat.toSSet.{w}

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