Homology of simplicial sets in degree 0

The main definition in this file is SSet.homology₀Iso which is an isomorphism X.homology R 0 ≅ ∐ (fun (_ : π₀ X) ↦ R) for any simplicial set X.

noncomputable def SSet.π₀.fromChainComplexXZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) : (X.chainComplex R).X 0 ⟶ ∐ fun (x : X.π₀) => R

Given a simplicial set X, this is the morphism from 0-chains with coefficients in R to coproduct of copies of R indexed by π₀ X.

Equations

• SSet.π₀.fromChainComplexXZero X R = (CategoryTheory.Limits.sigmaConst.obj R).map (TypeCat.ofHom SSet.π₀.mk)

@[simp]

theorem SSet.π₀.comp_fromChainComplexXZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) (x : X.obj (Opposite.op { len := 0 })) : CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) (fromChainComplexXZero X R) = CategoryTheory.Limits.Sigma.ι (fun (x : X.π₀) => R) (mk x)

@[simp]

theorem SSet.π₀.comp_fromChainComplexXZero_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) (x : X.obj (Opposite.op { len := 0 })) {Z : C} (h : (∐ fun (x : X.π₀) => R) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) (CategoryTheory.CategoryStruct.comp (fromChainComplexXZero X R) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : X.π₀) => R) (mk x)) h

@[simp]

theorem SSet.π₀.d_fromChainComplexXZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) (n : ℕ) : CategoryTheory.CategoryStruct.comp ((X.chainComplex R).d n 0) (fromChainComplexXZero X R) = 0

@[simp]

theorem SSet.π₀.d_fromChainComplexXZero_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) (n : ℕ) {Z : C} (h : (∐ fun (x : X.π₀) => R) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((X.chainComplex R).d n 0) (CategoryTheory.CategoryStruct.comp (fromChainComplexXZero X R) h) = CategoryTheory.CategoryStruct.comp 0 h

noncomputable def SSet.isColimitCokernelCoforkChainComplexDOneZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (π₀.fromChainComplexXZero X R) ⋯)

Given a simplicial set X, the cokernel of the differential d 1 0 of the chain complex of X with coefficients in R identifies to the coproduct of copies of R indexed by π₀ X.

Equations

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

noncomputable def SSet.homologyData₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) : (HomologicalComplex.sc' (X.chainComplex R) 1 0 0).HomologyData

A homology data saying that the singular homology in degree 0 of a simplicial set with coefficients in R identify to a coproduct of copies of X indexed by π₀ X.

Equations

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

@[simp]

theorem SSet.homologyData₀_left_K {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) : (X.homologyData₀ R).left.K = (X.chainComplex R).X 0

@[simp]

theorem SSet.homologyData₀_right_H {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) : (X.homologyData₀ R).right.H = ∐ fun (x : X.π₀) => R

@[simp]

theorem SSet.homologyData₀_right_Q {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) : (X.homologyData₀ R).right.Q = ∐ fun (x : X.π₀) => R

@[simp]

theorem SSet.homologyData₀_left_H {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) : (X.homologyData₀ R).left.H = ∐ fun (x : X.π₀) => R

@[simp]

theorem SSet.homologyData₀_left_π {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) : (X.homologyData₀ R).left.π = π₀.fromChainComplexXZero X R

@[simp]

theorem SSet.homologyData₀_left_i {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) : (X.homologyData₀ R).left.i = CategoryTheory.CategoryStruct.id ((X.chainComplex R).X 0)

@[simp]

theorem SSet.homologyData₀_left_liftK {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) {T : C} (f : T ⟶ (X.chainComplex R).X 0) : (X.homologyData₀ R).left.liftK f ⋯ = f

noncomputable def SSet.homology₀Iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) [CategoryTheory.CategoryWithHomology C] : X.homology R 0 ≅ ∐ fun (x : X.π₀) => R

The homology of a simplicial set in degree 0 with coefficients in R identifies to a coproduct of copies of R indexed by π₀ X.

Equations

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

@[simp]

theorem SSet.liftCycles_ιChainComplex_homologyπ_homology₀Iso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) [CategoryTheory.CategoryWithHomology C] (x : X.obj (Opposite.op { len := 0 })) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles (X.chainComplex R) (X.ιChainComplex x) 0 liftCycles_ιChainComplex_homologyπ_homology₀Iso_hom._proof_1 ⋯) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ (X.chainComplex R) 0) (X.homology₀Iso R).hom) = CategoryTheory.Limits.Sigma.ι (fun (x : X.π₀) => R) (π₀.mk x)

@[simp]

theorem SSet.liftCycles_ιChainComplex_homologyπ_homology₀Iso_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) [CategoryTheory.CategoryWithHomology C] (x : X.obj (Opposite.op { len := 0 })) {Z : C} (h : (∐ fun (x : X.π₀) => R) ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles (X.chainComplex R) (X.ιChainComplex x) 0 liftCycles_ιChainComplex_homologyπ_homology₀Iso_hom._proof_1 ⋯) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ (X.chainComplex R) 0) (CategoryTheory.CategoryStruct.comp (X.homology₀Iso R).hom h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : X.π₀) => R) (π₀.mk x)) h

noncomputable def SSet.homology₀ε {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) [CategoryTheory.CategoryWithHomology C] : X.homology R 0 ⟶ R

The augmentation map X.homology R 0 ⟶ R.

Equations

• X.homology₀ε R = CategoryTheory.CategoryStruct.comp (X.homology₀Iso R).hom (CategoryTheory.Limits.Sigma.desc fun (x : X.π₀) => CategoryTheory.CategoryStruct.id R)

@[simp]

theorem SSet.liftCycles_ιChainComplex_homologyπ_homology₀ε {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) [CategoryTheory.CategoryWithHomology C] (x : X.obj (Opposite.op { len := 0 })) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles (X.chainComplex R) (X.ιChainComplex x) 0 liftCycles_ιChainComplex_homologyπ_homology₀Iso_hom._proof_1 ⋯) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ (X.chainComplex R) 0) (X.homology₀ε R)) = CategoryTheory.CategoryStruct.id R

@[simp]

theorem SSet.liftCycles_ιChainComplex_homologyπ_homology₀ε_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) [CategoryTheory.CategoryWithHomology C] (x : X.obj (Opposite.op { len := 0 })) {Z : C} (h : R ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles (X.chainComplex R) (X.ιChainComplex x) 0 liftCycles_ιChainComplex_homologyπ_homology₀Iso_hom._proof_1 ⋯) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ (X.chainComplex R) 0) (CategoryTheory.CategoryStruct.comp (X.homology₀ε R) h)) = h

instance SSet.instIsIsoHomology₀εOfIsConnected {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) [CategoryTheory.CategoryWithHomology C] [X.IsConnected] : CategoryTheory.IsIso (X.homology₀ε R)