Classes of 1-simplices with equal faces

A 1-simplex of a simplicial set whose two faces agree is a 1-cycle of its chain complex, and so has a class SSet.ιHomology₁ in first simplicial homology with coefficients in R. This is the analogue in degree one of the vertex classes SSet.ιHomology₀ in degree zero.

noncomputable def SSet.ιHomology₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) (X : SSet) (s : X.obj (Opposite.op { len := 1 })) (h : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) s = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 1)) s) : R ⟶ X.homology R 1

The homology class of a 1-simplex whose two faces agree, a 1-cycle.

theorem SSet.ιHomology₁_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) (X : SSet) (s : X.obj (Opposite.op { len := 1 })) (h : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) s = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 1)) s) : ιHomology₁ R X s h = CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles (X.chainComplex R) (X.ιChainComplex s) 0 ιHomology₁_def._proof_1 ⋯) (HomologicalComplex.homologyπ (X.chainComplex R) 1)

The class of a 1-simplex with equal faces is the homology class of the cycle it defines.