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.
noncomputable def
SSet.chainComplexFunctor
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Preadditive 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 X := ℤ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[deprecated SSet.chainComplexFunctor (since := "2026-04-05")]
def
AlgebraicTopology.SSet.singularChainComplexFunctor
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Preadditive C]
:
Alias of SSet.chainComplexFunctor.
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 X := ℤ.
Instances For
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.
Instances For
@[deprecated SSet.chainComplexFunctorAdjunction (since := "2026-04-05")]
def
SSet.singularChainComplexFunctorAdjunction
(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 })
Alias of SSet.chainComplexFunctorAdjunction.
The adjunction Hom(Cⁿ(-, X), F) ≃ Hom(X, F(Δ[n])) for R : C and F : SSet ⥤ C.
Instances For
@[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)
:
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
Instances For
@[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)
:
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
Instances For
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 }))
:
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
Instances For
@[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.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
(∑ i : Fin (n + 2), (-1) ^ ↑i • X.ιChainComplex (CategoryTheory.SimplicialObject.δ X i 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 (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 (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
Instances For
noncomputable def
SSet.isColimitChainComplexXCofan
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Preadditive C]
(X : SSet)
(R : C)
(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
Instances For
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)
:
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
@[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
Instances For
@[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 : ℕ)
:
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
Instances For
@[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 : ℕ)
:
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✝)
:
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 : ℕ)
:
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 := ⋯ }
Instances For
@[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)
:
@[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✝)
: