Simplicial homology

In this file, we define the homology of simplicial sets. For any preadditive category C with coproducts of size w and any object R : C, the simplicial chain complex of a simplicial set X is denoted X.chainComplex R, and its homology in degree n : ℕ is X.homology R n.

@[implicit_reducible]

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

The chain complex associated to a simplicial set, with coefficients in R : C. It computes the simplicial homology of a simplicial sets with coefficients in R. One can recover the ordinary simplicial chain complex when C := Ab and R := ℤ.

Equations

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

instance SSet.instAdditiveFunctorChainComplexNatChainComplexFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] : (chainComplexFunctor C).Additive

noncomputable def SSet.chainComplexFunctorAdjunction (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (n : ℕ) : (CategoryTheory.Functor.postcompose₂.obj (HomologicalComplex.eval C (ComplexShape.down ℕ) n)).obj (chainComplexFunctor C) ⊣ (CategoryTheory.evaluation SSet C).obj (stdSimplex.obj { len := n })

The adjunction Hom(Cⁿ(-, X), F) ≃ Hom(X, F(Δ[n])) for R : C and F : SSet ⥤ C.

Equations

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

@[reducible, inline]

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

The (simplicial) chain complex of a simplicial set X with coefficients in R : C. Its homology is the simplicial homology of X.

Equations

• X.chainComplex R = ((SSet.chainComplexFunctor C).obj R).obj X

@[reducible, inline]

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

The morphism of simplicial chain complexes induces by a morphism of simplicial sets.

Equations

• SSet.chainComplexMap f R = ((SSet.chainComplexFunctor C).obj R).map f

noncomputable def SSet.ιChainComplex {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.chainComplex R).X n

The inclusion R ⟶ (X.chainComplex R).X n of the summand corresponding to a n-simplex x : X _⦋n⦌.

Equations

• X.ιChainComplex x = CategoryTheory.Limits.Sigma.ι (fun (x : X.obj (Opposite.op { len := n })) => R) x

@[simp]

theorem SSet.ιChainComplex_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.ιChainComplex x) ((X.chainComplex R).d (n + 1) n) = ∑ i : Fin (n + 2), (-1) ^ ↑i • X.ιChainComplex ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X i)) x)

@[simp]

theorem SSet.ιChainComplex_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.chainComplex R).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) (CategoryTheory.CategoryStruct.comp ((X.chainComplex R).d (n + 1) n) h) = CategoryTheory.CategoryStruct.comp (∑ x_1 : Fin (n + 2), (-1) ^ ↑x_1 • X.ιChainComplex ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X x_1)) x)) h

@[simp]

theorem SSet.ι_chainComplexMap_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.ιChainComplex x) ((chainComplexMap f R).f n) = Y.ιChainComplex ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n }))) x)

@[simp]

theorem SSet.ι_chainComplexMap_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.chainComplex R).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) (CategoryTheory.CategoryStruct.comp ((chainComplexMap f R).f n) h) = CategoryTheory.CategoryStruct.comp (Y.ιChainComplex ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n }))) x)) h

noncomputable def SSet.chainComplexXCofan {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.obj (Opposite.op { len := n })) => R

The colimit cofan which defines the simplicial n-chains (X.chainComplex R).X n.

Equations

• X.chainComplexXCofan R n = CategoryTheory.Limits.Cofan.mk ((X.chainComplex R).X n) X.ιChainComplex

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

Simplicial n-chains (X.chainComplex R).X n of a simplicial set X with coefficients in R identify to a coproduct of copies of R indexed by X _⦋n⦌.

Equations

• X.isColimitChainComplexXCofan R n = CategoryTheory.Limits.coproductIsCoproduct fun (x : X.obj (Opposite.op { len := n })) => R

theorem SSet.chainComplex_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.chainComplex R).X n ⟶ T} (h : ∀ (x : X.obj (Opposite.op { len := n })), CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) f = CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) g) : f = g

theorem SSet.chainComplex_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.chainComplex R).X n ⟶ T} : f = g ↔ ∀ (x : X.obj (Opposite.op { len := n })), CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) f = CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) g

theorem SSet.isZero_chainComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) [X.HasDimensionLT 0] : CategoryTheory.Limits.IsZero (X.chainComplex R)

@[reducible, inline]

noncomputable abbrev SSet.homology {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : C

The simplicial homology with coefficients in R : C in degree n of a simplicial set X.

Equations

• X.homology R n = HomologicalComplex.homology (X.chainComplex R) n

@[reducible, inline]

noncomputable abbrev SSet.homologyMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {X Y : SSet} (f : X ⟶ Y) (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : X.homology R n ⟶ Y.homology R n

The morphism in simplicial homology that is induced by a morphism of simplicial sets.

Equations

• SSet.homologyMap f R n = HomologicalComplex.homologyMap (SSet.chainComplexMap f R) n

@[simp]

theorem SSet.homologyMap_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : SSet.homologyMap (CategoryTheory.CategoryStruct.id X) R n = CategoryTheory.CategoryStruct.id (X.homology R n)

theorem SSet.homologyMap_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X Y Z : SSet) (f : X ⟶ Y) (g : Y ⟶ Z) (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : SSet.homologyMap (CategoryTheory.CategoryStruct.comp f g) R n = CategoryTheory.CategoryStruct.comp (SSet.homologyMap f R n) (SSet.homologyMap g R n)

theorem SSet.homologyMap_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X Y Z : SSet) (f : X ⟶ Y) (g : Y ⟶ Z) (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) {Z✝ : C} (h : Z.homology R n ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (SSet.homologyMap (CategoryTheory.CategoryStruct.comp f g) R n) h = CategoryTheory.CategoryStruct.comp (SSet.homologyMap f R n) (CategoryTheory.CategoryStruct.comp (SSet.homologyMap g R n) h)

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

The simplicial homology functor in degree n with coefficients in R : C.

Equations

• SSet.homologyFunctor R n = { obj := fun (X : SSet) => X.homology R n, map := fun {X Y : SSet} (f : X ⟶ Y) => SSet.homologyMap f R n, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem SSet.homologyFunctor_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) {X✝ Y✝ : SSet} (f : X✝ ⟶ Y✝) : (homologyFunctor R n).map f = SSet.homologyMap f R n

@[simp]

theorem SSet.homologyFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) (X : SSet) : (homologyFunctor R n).obj X = X.homology R n