Computing homology using nondegenerate simplices

In this file, we introduce the normalized chain complex X.normalizedChainComplex R of a simplicial set X with coefficients in R (where R is an object of a preadditive category C with coproducts). The n-chains of this complex identify to the coproduct of copies of R indexed by the nondegenerate n-simplices of X. In particular, we deduce that the homology is zero in degree ≥ d when X has dimension < d.

noncomputable def SSet.normalizedChainComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) : ChainComplex C ℕ

The normalized chain complex of a simplicial set X with coefficients in R. In degree n, it consists of a coproduct of copies of R indexed by the nondegenerate n-simplices of X.

Equations

• X.normalizedChainComplex R = (X.splitting.map (CategoryTheory.Limits.sigmaConst.obj R)).nondegComplex

noncomputable def SSet.toNormalizedChainComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) : X.chainComplex R ⟶ X.normalizedChainComplex R

The split epi X.chainComplex R ⟶ X.normalizedChainComplex R.

Equations

• X.toNormalizedChainComplex R = (X.splitting.map (CategoryTheory.Limits.sigmaConst.obj R)).toNondegComplex

noncomputable def SSet.fromNormalizedChainComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) : X.normalizedChainComplex R ⟶ X.chainComplex R

The split mono X.normalizedChainComplex R ⟶ X.chainComplex R.

Equations

• X.fromNormalizedChainComplex R = (X.splitting.map (CategoryTheory.Limits.sigmaConst.obj R)).fromNondegComplex

@[simp]

theorem SSet.PInfty_toNormalizedChainComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) : CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty (X.toNormalizedChainComplex R) = X.toNormalizedChainComplex R

@[simp]

theorem SSet.PInfty_toNormalizedChainComplex_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) {Z : ChainComplex C ℕ} (h : X.normalizedChainComplex R ⟶ Z) : CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty (CategoryTheory.CategoryStruct.comp (X.toNormalizedChainComplex R) h) = CategoryTheory.CategoryStruct.comp (X.toNormalizedChainComplex R) h

instance SSet.instIsSplitEpiChainComplexNatToNormalizedChainComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) : CategoryTheory.IsSplitEpi (X.toNormalizedChainComplex R)

instance SSet.instIsSplitMonoChainComplexNatFromNormalizedChainComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) : CategoryTheory.IsSplitMono (X.fromNormalizedChainComplex R)

@[simp]

theorem SSet.fromNormalizedChainComplex_toNormalizedChainComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) : CategoryTheory.CategoryStruct.comp (X.fromNormalizedChainComplex R) (X.toNormalizedChainComplex R) = CategoryTheory.CategoryStruct.id (X.normalizedChainComplex R)

@[simp]

theorem SSet.fromNormalizedChainComplex_toNormalizedChainComplex_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) {Z : ChainComplex C ℕ} (h : X.normalizedChainComplex R ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.fromNormalizedChainComplex R) (CategoryTheory.CategoryStruct.comp (X.toNormalizedChainComplex R) h) = h

@[simp]

theorem SSet.fromNormalizedChainComplex_f_toNormalizedChainComplex_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) (n : ℕ) : CategoryTheory.CategoryStruct.comp ((X.fromNormalizedChainComplex R).f n) ((X.toNormalizedChainComplex R).f n) = CategoryTheory.CategoryStruct.id ((X.normalizedChainComplex R).X n)

@[simp]

theorem SSet.fromNormalizedChainComplex_f_toNormalizedChainComplex_f_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) (n : ℕ) {Z : C} (h : (X.normalizedChainComplex R).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp ((X.fromNormalizedChainComplex R).f n) (CategoryTheory.CategoryStruct.comp ((X.toNormalizedChainComplex R).f n) h) = h

@[simp]

theorem SSet.toNormalizedChainComplex_fromNormalizedChainComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) : CategoryTheory.CategoryStruct.comp (X.toNormalizedChainComplex R) (X.fromNormalizedChainComplex R) = AlgebraicTopology.DoldKan.PInfty

@[simp]

theorem SSet.toNormalizedChainComplex_fromNormalizedChainComplex_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) {Z : ChainComplex C ℕ} (h : X.chainComplex R ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.toNormalizedChainComplex R) (CategoryTheory.CategoryStruct.comp (X.fromNormalizedChainComplex R) h) = CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty h

@[simp]

theorem SSet.toNormalizedChainComplex_f_fromNormalizedChainComplex_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) (n : ℕ) : CategoryTheory.CategoryStruct.comp ((X.toNormalizedChainComplex R).f n) ((X.fromNormalizedChainComplex R).f n) = AlgebraicTopology.DoldKan.PInfty.f n

@[simp]

theorem SSet.toNormalizedChainComplex_f_fromNormalizedChainComplex_f_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) (n : ℕ) {Z : C} (h : (X.chainComplex R).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp ((X.toNormalizedChainComplex R).f n) (CategoryTheory.CategoryStruct.comp ((X.fromNormalizedChainComplex R).f n) h) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) h

noncomputable def SSet.homotopyEquivNormalizedChainComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) : HomotopyEquiv (X.chainComplex R) (X.normalizedChainComplex R)

The homotopy equivalence from X.chainComplex R to X.normalizedChainComplex R.

Equations

• X.homotopyEquivNormalizedChainComplex R = (X.splitting.map (CategoryTheory.Limits.sigmaConst.obj R)).homotopyEquivNondegComplex

@[simp]

theorem SSet.homotopyEquivNormalizedChainComplex_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) : (X.homotopyEquivNormalizedChainComplex R).hom = X.toNormalizedChainComplex R

@[simp]

theorem SSet.homotopyEquivNormalizedChainComplex_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) : (X.homotopyEquivNormalizedChainComplex R).inv = X.fromNormalizedChainComplex R

noncomputable def SSet.ιNormalizedChainComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) {R : C} {n : ℕ} (x : X.obj (Opposite.op { len := n })) : R ⟶ (X.normalizedChainComplex R).X n

The map R ⟶ (X.normalizedChainComplex R).X n for any x : X _⦋n⦌. Note that this is zero if x is a degenerate simplex, see ιNormalizedChainComplex_eq_zero.

Equations

• X.ιNormalizedChainComplex x = CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) ((X.toNormalizedChainComplex R).f n)

@[simp]

theorem SSet.ιChainComplex_toNormalizedChainComplex_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) {R : C} {n : ℕ} (x : X.obj (Opposite.op { len := n })) : CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) ((X.toNormalizedChainComplex R).f n) = X.ιNormalizedChainComplex x

@[simp]

theorem SSet.ιChainComplex_toNormalizedChainComplex_f_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) {R : C} {n : ℕ} (x : X.obj (Opposite.op { len := n })) {Z : C} (h : (X.normalizedChainComplex R).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) (CategoryTheory.CategoryStruct.comp ((X.toNormalizedChainComplex R).f n) h) = CategoryTheory.CategoryStruct.comp (X.ιNormalizedChainComplex x) h

@[simp]

theorem SSet.ιNormalizedChainComplex_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) {R : C} {n : ℕ} (x : X.obj (Opposite.op { len := n + 1 })) : CategoryTheory.CategoryStruct.comp (X.ιNormalizedChainComplex x) ((X.normalizedChainComplex R).d (n + 1) n) = ∑ i : Fin (n + 2), (-1) ^ ↑i • X.ιNormalizedChainComplex ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X i)) x)

@[simp]

theorem SSet.ιNormalizedChainComplex_d_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) {R : C} {n : ℕ} (x : X.obj (Opposite.op { len := n + 1 })) {Z : C} (h : (X.normalizedChainComplex R).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.ιNormalizedChainComplex x) (CategoryTheory.CategoryStruct.comp ((X.normalizedChainComplex R).d (n + 1) n) h) = CategoryTheory.CategoryStruct.comp (∑ x_1 : Fin (n + 2), (-1) ^ ↑x_1 • X.ιNormalizedChainComplex ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X x_1)) x)) h

theorem SSet.ιNormalizedChainComplex_fromNormalizedChainComplex_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) {R : C} {n : ℕ} (x : X.obj (Opposite.op { len := n })) : CategoryTheory.CategoryStruct.comp (X.ιNormalizedChainComplex x) ((X.fromNormalizedChainComplex R).f n) = CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) (AlgebraicTopology.DoldKan.PInfty.f n)

theorem SSet.ιNormalizedChainComplex_fromNormalizedChainComplex_f_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) {R : C} {n : ℕ} (x : X.obj (Opposite.op { len := n })) {Z : C} (h : (X.chainComplex R).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.ιNormalizedChainComplex x) (CategoryTheory.CategoryStruct.comp ((X.fromNormalizedChainComplex R).f n) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) (AlgebraicTopology.DoldKan.PInfty.f n)) h

theorem SSet.ιNormalizedChainComplex_eq_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) {R : C} {n : ℕ} (x : X.obj (Opposite.op { len := n })) (hx : x ∈ X.degenerate n) : X.ιNormalizedChainComplex x = 0

@[reducible, inline]

noncomputable abbrev SSet.cofanNormalizedChainComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) (n : ℕ) : CategoryTheory.Limits.Cofan fun (x : ↑(X.nonDegenerate n)) => R

The cofan given by the inclusions X.ιNormalizedChainComplex x : R ⟶ (X.normalizedChainComplex R).X n for all nondegenerate n-simplices x of a simplicial set X.

Equations

• X.cofanNormalizedChainComplex R n = CategoryTheory.Limits.Cofan.mk ((X.normalizedChainComplex R).X n) fun (x : ↑(X.nonDegenerate n)) => X.ιNormalizedChainComplex ↑x

noncomputable def SSet.isColimitCofanNormalizedChainComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) (n : ℕ) : CategoryTheory.Limits.IsColimit (X.cofanNormalizedChainComplex R n)

(X.normalizedChainComplex R).X n identifies to the coproduct of copies of R indexed by the nondegenerate n-simplices of the simplicial set X.

Equations

• One or more equations did not get rendered due to their size.

theorem SSet.normalizedChainComplex_hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) {R : C} {n : ℕ} {T : C} {f g : (X.normalizedChainComplex R).X n ⟶ T} (h : ∀ x ∈ X.nonDegenerate n, CategoryTheory.CategoryStruct.comp (X.ιNormalizedChainComplex x) f = CategoryTheory.CategoryStruct.comp (X.ιNormalizedChainComplex x) g) : f = g

theorem SSet.normalizedChainComplex_hom_ext_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {X : SSet} {R : C} {n : ℕ} {T : C} {f g : (X.normalizedChainComplex R).X n ⟶ T} : f = g ↔ ∀ x ∈ X.nonDegenerate n, CategoryTheory.CategoryStruct.comp (X.ιNormalizedChainComplex x) f = CategoryTheory.CategoryStruct.comp (X.ιNormalizedChainComplex x) g

theorem SSet.isZero_normalizedChainComplex_X_of_hasDimensionLT {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) (n d : ℕ) [X.HasDimensionLT d] (h : d ≤ n := by lia) : CategoryTheory.Limits.IsZero ((X.normalizedChainComplex R).X n)

theorem SSet.chainComplexMap_PInfty {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {X Y : SSet} (f : X ⟶ Y) (R : C) : CategoryTheory.CategoryStruct.comp (chainComplexMap f R) AlgebraicTopology.DoldKan.PInfty = CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty (chainComplexMap f R)

theorem SSet.chainComplexMap_PInfty_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {X Y : SSet} (f : X ⟶ Y) (R : C) {Z : ChainComplex C ℕ} (h : AlgebraicTopology.AlternatingFaceMapComplex.obj (((CategoryTheory.Limits.sigmaConst.comp (CategoryTheory.SimplicialObject.whiskering (Type w) C)).obj R).obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (chainComplexMap f R) (CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty h) = CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty (CategoryTheory.CategoryStruct.comp (chainComplexMap f R) h)

noncomputable def SSet.normalizedChainComplexMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {X Y : SSet} (f : X ⟶ Y) (R : C) : X.normalizedChainComplex R ⟶ Y.normalizedChainComplex R

The morphism X.normalizedChainComplex R ⟶ Y.normalizedChainComplex R induced by a morphism a simplicial sets X ⟶ Y.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SSet.toNormalizedChainComplex_normalizedChainComplexMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {X Y : SSet} (f : X ⟶ Y) (R : C) : CategoryTheory.CategoryStruct.comp (X.toNormalizedChainComplex R) (normalizedChainComplexMap f R) = CategoryTheory.CategoryStruct.comp (chainComplexMap f R) (Y.toNormalizedChainComplex R)

@[simp]

theorem SSet.toNormalizedChainComplex_normalizedChainComplexMap_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {X Y : SSet} (f : X ⟶ Y) (R : C) {Z : ChainComplex C ℕ} (h : Y.normalizedChainComplex R ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.toNormalizedChainComplex R) (CategoryTheory.CategoryStruct.comp (normalizedChainComplexMap f R) h) = CategoryTheory.CategoryStruct.comp (chainComplexMap f R) (CategoryTheory.CategoryStruct.comp (Y.toNormalizedChainComplex R) h)

@[simp]

theorem SSet.ι_normalizedChainComplexMap_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {X Y : SSet} (f : X ⟶ Y) (R : C) {n : ℕ} (x : X.obj (Opposite.op { len := n })) : CategoryTheory.CategoryStruct.comp (X.ιNormalizedChainComplex x) ((normalizedChainComplexMap f R).f n) = Y.ιNormalizedChainComplex ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n }))) x)

@[simp]

theorem SSet.ι_normalizedChainComplexMap_f_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {X Y : SSet} (f : X ⟶ Y) (R : C) {n : ℕ} (x : X.obj (Opposite.op { len := n })) {Z : C} (h : (Y.normalizedChainComplex R).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.ιNormalizedChainComplex x) (CategoryTheory.CategoryStruct.comp ((normalizedChainComplexMap f R).f n) h) = CategoryTheory.CategoryStruct.comp (Y.ιNormalizedChainComplex ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n }))) x)) h

noncomputable def SSet.normalizedChainComplexFunctorObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) : CategoryTheory.Functor SSet (ChainComplex C ℕ)

Given R : C, this is the functor SSet.{w} ⥤ ChainComplex C ℕ which sends a simplicial set X to X.normalizedChainComplex R.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SSet.normalizedChainComplexFunctorObj_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) {X✝ Y✝ : SSet} (f : X✝ ⟶ Y✝) : (normalizedChainComplexFunctorObj R).map f = normalizedChainComplexMap f R

@[simp]

theorem SSet.normalizedChainComplexFunctorObj_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) (X : SSet) : (normalizedChainComplexFunctorObj R).obj X = X.normalizedChainComplex R

noncomputable def SSet.toNormalizedChainComplexNatTrans {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) : (chainComplexFunctor C).obj R ⟶ normalizedChainComplexFunctorObj R

The morphism X.toNormalizedChainComplex R for any simplicial set X, as a natural transformation.

Equations

• SSet.toNormalizedChainComplexNatTrans R = { app := fun (X : SSet) => X.toNormalizedChainComplex R, naturality := ⋯ }

@[simp]

theorem SSet.toNormalizedChainComplexNatTrans_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) (X : SSet) : (toNormalizedChainComplexNatTrans R).app X = X.toNormalizedChainComplex R

instance SSet.instQuasiIsoNatToNormalizedChainComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) [CategoryTheory.CategoryWithHomology C] : QuasiIso (X.toNormalizedChainComplex R)

instance SSet.instQuasiIsoNatFromNormalizedChainComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) [CategoryTheory.CategoryWithHomology C] : QuasiIso (X.fromNormalizedChainComplex R)

theorem SSet.exactAt_chainComplex_of_hasDimensionLT {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) [CategoryTheory.CategoryWithHomology C] (n d : ℕ) [X.HasDimensionLT d] (h : d ≤ n := by lia) : HomologicalComplex.ExactAt (X.chainComplex R) n

theorem SSet.isZero_homology_of_hasDimensionLT {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) [CategoryTheory.CategoryWithHomology C] (n d : ℕ) [X.HasDimensionLT d] (h : d ≤ n := by lia) : CategoryTheory.Limits.IsZero (X.homology R n)