Relative classes of 1-simplices

For a pair of simplicial sets Q (a monomorphism Q.left ⟶ Q.right), a 1-simplex s of Q.right whose two faces lie in Q.left is a relative cycle, and so has a class SSetPair.relClass₁ R Q s v₀ v₁ h₀ h₁ : R ⟶ Q.homology R 1 in relative homology with coefficients in R. This file computes its image under the connecting morphism, the difference [v₁] - [v₀] of the classes of its endpoints (SSetPair.relClass₁_homologyδ); proves that the class is natural in maps of pairs (SSetPair.relClass₁_homologyMap); and identifies it with the image of the absolute class SSet.ιHomology₁ (in SimplicialSet/Homology/One.lean) when the two faces agree (SSetPair.ιHomology₁_homologyπ). The computation of the connecting morphism is ShortComplex.ShortExact.δ_eq for the short exact sequence of chain complexes of the pair.

With coproducts available, the relative cycle needs only preadditive coefficients. Its class and naturality also require a category with homology. The connecting-morphism calculation uses abelian coefficients.

Main definitions and results

• SSetPair.relClass₁: the relative class of a 1-simplex with faces in the subcomplex.
• SSetPair.relClass₁_homologyδ: its image under the connecting morphism.
• SSetPair.relClass₁_homologyMap: naturality in maps of pairs.
• SSetPair.ιHomology₁_homologyπ: the image in relative homology of the absolute class of a 1-simplex with equal faces.

@[simp]

theorem SSetPair.ιChainComplex_hom_app_comp_chainComplexπ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] (R : C) (Q : SSetPair) [CategoryTheory.Preadditive C] (v : Q.left.obj (Opposite.op { len := 0 })) : CategoryTheory.CategoryStruct.comp (Q.right.ιChainComplex ((CategoryTheory.ConcreteCategory.hom (Q.hom.app (Opposite.op { len := 0 }))) v)) ((Q.chainComplexπ R).f 0) = 0

The chain of a vertex in the subcomplex vanishes in relative chains.

@[simp]

theorem SSetPair.ιChainComplex_hom_app_comp_chainComplexπ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] (R : C) (Q : SSetPair) [CategoryTheory.Preadditive C] (v : Q.left.obj (Opposite.op { len := 0 })) {Z : C} (h : (Q.chainComplex R).X 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (Q.right.ιChainComplex ((CategoryTheory.ConcreteCategory.hom (Q.hom.app (Opposite.op { len := 0 }))) v)) (CategoryTheory.CategoryStruct.comp ((Q.chainComplexπ R).f 0) h) = CategoryTheory.CategoryStruct.comp 0 h

The chain of a vertex in the subcomplex vanishes in relative chains.

theorem SSetPair.relClass₁_cycle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] (R : C) (Q : SSetPair) (s : Q.right.obj (Opposite.op { len := 1 })) (v₀ v₁ : Q.left.obj (Opposite.op { len := 0 })) (h₀ : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Q.right 1)) s = (CategoryTheory.ConcreteCategory.hom (Q.hom.app (Opposite.op { len := 0 }))) v₀) (h₁ : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Q.right 0)) s = (CategoryTheory.ConcreteCategory.hom (Q.hom.app (Opposite.op { len := 0 }))) v₁) [CategoryTheory.Preadditive C] : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (Q.right.ιChainComplex s) ((Q.chainComplexπ R).f 1)) ((Q.chainComplex R).d 1 0) = 0

A simplex whose endpoints lie in the subcomplex defines a relative cycle.

noncomputable def SSetPair.relClass₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] (R : C) (Q : SSetPair) (s : Q.right.obj (Opposite.op { len := 1 })) (v₀ v₁ : Q.left.obj (Opposite.op { len := 0 })) (h₀ : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Q.right 1)) s = (CategoryTheory.ConcreteCategory.hom (Q.hom.app (Opposite.op { len := 0 }))) v₀) (h₁ : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Q.right 0)) s = (CategoryTheory.ConcreteCategory.hom (Q.hom.app (Opposite.op { len := 0 }))) v₁) [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] : R ⟶ Q.homology R 1

The relative homology class of a 1-simplex of the ambient simplicial set whose two faces lie in the subcomplex.

theorem SSetPair.relClass₁_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] (R : C) (Q : SSetPair) (s : Q.right.obj (Opposite.op { len := 1 })) (v₀ v₁ : Q.left.obj (Opposite.op { len := 0 })) (h₀ : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Q.right 1)) s = (CategoryTheory.ConcreteCategory.hom (Q.hom.app (Opposite.op { len := 0 }))) v₀) (h₁ : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Q.right 0)) s = (CategoryTheory.ConcreteCategory.hom (Q.hom.app (Opposite.op { len := 0 }))) v₁) [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] : relClass₁ R Q s v₀ v₁ h₀ h₁ = CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles (Q.chainComplex R) (CategoryTheory.CategoryStruct.comp (Q.right.ιChainComplex s) ((Q.chainComplexπ R).f 1)) 0 relClass₁_eq._proof_1 ⋯) (HomologicalComplex.homologyπ (Q.chainComplex R) 1)

The relative class of a 1-simplex is the homology class of the relative cycle it defines.

theorem SSetPair.δ_map_eq {Q : SSetPair} (s : Q.right.obj (Opposite.op { len := 1 })) {Q' : SSetPair} (f : Q ⟶ Q') (i : Fin 2) (v : Q.left.obj (Opposite.op { len := 0 })) (h : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Q.right i)) s = (CategoryTheory.ConcreteCategory.hom (Q.hom.app (Opposite.op { len := 0 }))) v) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Q'.right i)) ((CategoryTheory.ConcreteCategory.hom (f.right.app (Opposite.op { len := 0 + 1 }))) s) = (CategoryTheory.ConcreteCategory.hom (Q'.hom.app (Opposite.op { len := 0 }))) ((CategoryTheory.ConcreteCategory.hom (f.left.app (Opposite.op { len := 0 }))) v)

A map of pairs carries a face of a 1-simplex lying in the subcomplex to a face lying in the subcomplex.

@[simp]

theorem SSetPair.relClass₁_homologyMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] (R : C) {Q : SSetPair} (s : Q.right.obj (Opposite.op { len := 1 })) (v₀ v₁ : Q.left.obj (Opposite.op { len := 0 })) (h₀ : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Q.right 1)) s = (CategoryTheory.ConcreteCategory.hom (Q.hom.app (Opposite.op { len := 0 }))) v₀) (h₁ : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Q.right 0)) s = (CategoryTheory.ConcreteCategory.hom (Q.hom.app (Opposite.op { len := 0 }))) v₁) [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {Q' : SSetPair} (f : Q ⟶ Q') : CategoryTheory.CategoryStruct.comp (relClass₁ R Q s v₀ v₁ h₀ h₁) (SSetPair.homologyMap f R 1) = relClass₁ R Q' ((CategoryTheory.ConcreteCategory.hom (f.right.app (Opposite.op { len := 1 }))) s) ((CategoryTheory.ConcreteCategory.hom (f.left.app (Opposite.op { len := 0 }))) v₀) ((CategoryTheory.ConcreteCategory.hom (f.left.app (Opposite.op { len := 0 }))) v₁) ⋯ ⋯

Naturality of the relative class of a 1-simplex in maps of pairs.

@[simp]

theorem SSetPair.relClass₁_homologyMap_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] (R : C) {Q : SSetPair} (s : Q.right.obj (Opposite.op { len := 1 })) (v₀ v₁ : Q.left.obj (Opposite.op { len := 0 })) (h₀ : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Q.right 1)) s = (CategoryTheory.ConcreteCategory.hom (Q.hom.app (Opposite.op { len := 0 }))) v₀) (h₁ : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Q.right 0)) s = (CategoryTheory.ConcreteCategory.hom (Q.hom.app (Opposite.op { len := 0 }))) v₁) [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {Q' : SSetPair} (f : Q ⟶ Q') {Z : C} (h : Q'.homology R 1 ⟶ Z) : CategoryTheory.CategoryStruct.comp (relClass₁ R Q s v₀ v₁ h₀ h₁) (CategoryTheory.CategoryStruct.comp (SSetPair.homologyMap f R 1) h) = CategoryTheory.CategoryStruct.comp (relClass₁ R Q' ((CategoryTheory.ConcreteCategory.hom (f.right.app (Opposite.op { len := 1 }))) s) ((CategoryTheory.ConcreteCategory.hom (f.left.app (Opposite.op { len := 0 }))) v₀) ((CategoryTheory.ConcreteCategory.hom (f.left.app (Opposite.op { len := 0 }))) v₁) ⋯ ⋯) h

Naturality of the relative class of a 1-simplex in maps of pairs.

theorem SSetPair.ιHomology₁_homologyπ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] (R : C) (Q : SSetPair) (s : Q.right.obj (Opposite.op { len := 1 })) (v₀ v₁ : Q.left.obj (Opposite.op { len := 0 })) (h₀ : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Q.right 1)) s = (CategoryTheory.ConcreteCategory.hom (Q.hom.app (Opposite.op { len := 0 }))) v₀) (h₁ : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Q.right 0)) s = (CategoryTheory.ConcreteCategory.hom (Q.hom.app (Opposite.op { len := 0 }))) v₁) [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (h : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Q.right 0)) s = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Q.right 1)) s) : CategoryTheory.CategoryStruct.comp (SSet.ιHomology₁ R Q.right s h) (Q.homologyπ R 1) = relClass₁ R Q s v₀ v₁ h₀ h₁

The relative class of a 1-simplex whose two faces agree is the image of its absolute class.

@[simp]

theorem SSetPair.relClass₁_homologyδ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] (R : C) (Q : SSetPair) (s : Q.right.obj (Opposite.op { len := 1 })) (v₀ v₁ : Q.left.obj (Opposite.op { len := 0 })) (h₀ : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Q.right 1)) s = (CategoryTheory.ConcreteCategory.hom (Q.hom.app (Opposite.op { len := 0 }))) v₀) (h₁ : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Q.right 0)) s = (CategoryTheory.ConcreteCategory.hom (Q.hom.app (Opposite.op { len := 0 }))) v₁) [CategoryTheory.Abelian C] : CategoryTheory.CategoryStruct.comp (relClass₁ R Q s v₀ v₁ h₀ h₁) (Q.homologyδ R 1 0 relClass₁_homologyδ._proof_2) = SSet.ιHomology₀ R v₁ - SSet.ιHomology₀ R v₀

The connecting morphism on the relative class of a 1-simplex is the difference of the classes of its two vertices in the subcomplex.

@[simp]

theorem SSetPair.relClass₁_homologyδ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] (R : C) (Q : SSetPair) (s : Q.right.obj (Opposite.op { len := 1 })) (v₀ v₁ : Q.left.obj (Opposite.op { len := 0 })) (h₀ : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Q.right 1)) s = (CategoryTheory.ConcreteCategory.hom (Q.hom.app (Opposite.op { len := 0 }))) v₀) (h₁ : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Q.right 0)) s = (CategoryTheory.ConcreteCategory.hom (Q.hom.app (Opposite.op { len := 0 }))) v₁) [CategoryTheory.Abelian C] {Z : C} (h : Q.left.homology R 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (relClass₁ R Q s v₀ v₁ h₀ h₁) (CategoryTheory.CategoryStruct.comp (Q.homologyδ R 1 0 relClass₁_homologyδ._proof_2) h) = CategoryTheory.CategoryStruct.comp (SSet.ιHomology₀ R v₁ - SSet.ιHomology₀ R v₀) h

The connecting morphism on the relative class of a 1-simplex is the difference of the classes of its two vertices in the subcomplex.