Naturality in relative simplicial homology

For a pair of simplicial sets P, given by a monomorphism X ⟶ Y, Mathlib constructs the short exact sequence of chain complexes 0 ⟶ C(X) ⟶ C(Y) ⟶ C(Y, X) ⟶ 0 and the connecting morphism Hₙ(Y, X) ⟶ Hₘ(X) for m + 1 = n. This file shows that a morphism of pairs induces a morphism of these short exact sequences, and deduces that the connecting morphism is natural, so that it forms a natural transformation SSetPair.homologyδNatTrans.

It also records that the quotient maps from ambient to relative chains and homology are natural in the pair: they commute with morphisms of simplicial-set pairs. The short exact sequence of chain complexes of a pair is split in each degree, because the map C(X) ⟶ C(Y) is induced by the injection of the n-simplices of X into those of Y; so the relative chains are a retract of the ambient chains (SSetPair.chainComplexXRetract), and are projective when those are (SSetPair.projective_chainComplex_X). A morphism of pairs which is a quasi-isomorphism on subcomplexes and ambient simplicial sets is a quasi-isomorphism on relative chains (SSetPair.quasiIso_chainComplexMap), hence induces isomorphisms on relative homology.

The source is Eilenberg--Steenrod, Foundations of Algebraic Topology, Chapters I--III.

noncomputable def SSetPair.chainComplexShortComplexMap {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {P P' : SSetPair} (f : P ⟶ P') (R : C) : P.chainComplexShortComplex R ⟶ P'.chainComplexShortComplex R

The morphism of chain complex sequences C(X) ⟶ C(Y) ⟶ C(Y, X) induced by a morphism of pairs of simplicial sets.

@[simp]

theorem SSetPair.chainComplexShortComplexMap_τ₁ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {P P' : SSetPair} (f : P ⟶ P') (R : C) : (chainComplexShortComplexMap f R).τ₁ = SSet.chainComplexMap f.left R

@[simp]

theorem SSetPair.chainComplexShortComplexMap_τ₂ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {P P' : SSetPair} (f : P ⟶ P') (R : C) : (chainComplexShortComplexMap f R).τ₂ = SSet.chainComplexMap f.right R

@[simp]

theorem SSetPair.chainComplexShortComplexMap_τ₃ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {P P' : SSetPair} (f : P ⟶ P') (R : C) : (chainComplexShortComplexMap f R).τ₃ = chainComplexMap f R

theorem SSetPair.chainComplexMap_left_comp_chainComplexMap_hom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) {P P' : SSetPair} (f : P ⟶ P') : CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap f.left R) (SSet.chainComplexMap P'.hom R) = CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap P.hom R) (SSet.chainComplexMap f.right R)

The chain maps induced by a morphism of pairs on the chains of the subobjects and of the ambient simplicial sets commute with the inclusions of subobject chains into ambient chains.

theorem SSetPair.chainComplexMap_left_comp_chainComplexMap_hom_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) {P P' : SSetPair} (f : P ⟶ P') {Z : ChainComplex C ℕ} (h : P'.right.chainComplex R ⟶ Z) : CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap f.left R) (CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap P'.hom R) h) = CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap P.hom R) (CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap f.right R) h)

The chain maps induced by a morphism of pairs on the chains of the subobjects and of the ambient simplicial sets commute with the inclusions of subobject chains into ambient chains.

theorem SSetPair.chainComplexπ_naturality {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) {P P' : SSetPair} (f : P ⟶ P') : CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap f.right R) (P'.chainComplexπ R) = CategoryTheory.CategoryStruct.comp (P.chainComplexπ R) (chainComplexMap f R)

The quotient maps from ambient to relative chains commute with the chain maps induced by a morphism of pairs.

theorem SSetPair.chainComplexπ_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) {P P' : SSetPair} (f : P ⟶ P') {Z : ChainComplex C ℕ} (h : P'.chainComplex R ⟶ Z) : CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap f.right R) (CategoryTheory.CategoryStruct.comp (P'.chainComplexπ R) h) = CategoryTheory.CategoryStruct.comp (P.chainComplexπ R) (CategoryTheory.CategoryStruct.comp (chainComplexMap f R) h)

The quotient maps from ambient to relative chains commute with the chain maps induced by a morphism of pairs.

instance SSetPair.instIsSplitMonoFNatChainComplexMapHomSSet_tauCeti {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) (P : SSetPair) (n : ℕ) : CategoryTheory.IsSplitMono ((SSet.chainComplexMap P.hom R).f n)

In each degree, the map from the chains of the subobject of a pair of simplicial sets to the chains of the ambient simplicial set is a split monomorphism.

noncomputable def SSetPair.chainComplexXRetract {A : Type u_2} [CategoryTheory.Category.{v_2, u_2} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (P : SSetPair) (n : ℕ) : CategoryTheory.Retract ((P.chainComplex R).X n) ((P.right.chainComplex R).X n)

The relative chains Cₙ(Y, X; R) of a pair X ⟶ Y of simplicial sets are a retract of the ambient chains Cₙ(Y; R): the degree-n sequence 0 ⟶ Cₙ(X) ⟶ Cₙ(Y) ⟶ Cₙ(Y, X) ⟶ 0 is short exact with split first map, so the quotient map to the relative chains has a section.

instance SSetPair.projective_chainComplex_X {A : Type u_2} [CategoryTheory.Category.{v_2, u_2} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (P : SSetPair) (n : ℕ) [CategoryTheory.Projective ((P.right.chainComplex R).X n)] : CategoryTheory.Projective ((P.chainComplex R).X n)

The relative chains Cₙ(Y, X; R) of a pair of simplicial sets are projective whenever the ambient chains Cₙ(Y; R) are, for instance for chains with coefficients in a projective module.

theorem SSetPair.homologyδ_naturality {A : Type u_2} [CategoryTheory.Category.{v_2, u_2} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] {P P' : SSetPair} (f : P ⟶ P') (R : A) (n m : ℕ) (h : m + 1 = n := by lia) : CategoryTheory.CategoryStruct.comp (P.homologyδ R n m h) (SSet.homologyMap f.left R m) = CategoryTheory.CategoryStruct.comp (SSetPair.homologyMap f R n) (P'.homologyδ R n m h)

The connecting morphism of the long exact sequence of a pair of simplicial sets is natural: for a morphism of pairs f : P ⟶ P', the square formed by the connecting morphisms Hₙ(P) ⟶ Hₘ(P.left) and Hₙ(P') ⟶ Hₘ(P'.left) and the maps induced by f commutes.

theorem SSetPair.homologyδ_naturality_assoc {A : Type u_2} [CategoryTheory.Category.{v_2, u_2} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] {P P' : SSetPair} (f : P ⟶ P') (R : A) (n m : ℕ) (h : m + 1 = n := by lia) {Z : A} (h✝ : P'.left.homology R m ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.homologyδ R n m h) (CategoryTheory.CategoryStruct.comp (SSet.homologyMap f.left R m) h✝) = CategoryTheory.CategoryStruct.comp (SSetPair.homologyMap f R n) (CategoryTheory.CategoryStruct.comp (P'.homologyδ R n m h) h✝)

The connecting morphism of the long exact sequence of a pair of simplicial sets is natural: for a morphism of pairs f : P ⟶ P', the square formed by the connecting morphisms Hₙ(P) ⟶ Hₘ(P.left) and Hₙ(P') ⟶ Hₘ(P'.left) and the maps induced by f commutes.

noncomputable def SSetPair.homologyδNatTrans {A : Type u_2} [CategoryTheory.Category.{v_2, u_2} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n m : ℕ) (h : m + 1 = n := by lia) : homologyFunctor R n ⟶ (forget.comp CategoryTheory.Arrow.leftFunc).comp (SSet.homologyFunctor R m)

The connecting morphism Hₙ(Y, X) ⟶ Hₘ(X) of the long exact sequence of a pair of simplicial sets X ⟶ Y, for m + 1 = n, as a natural transformation from relative homology to the homology of the subobject.

@[simp]

theorem SSetPair.homologyδNatTrans_app {A : Type u_2} [CategoryTheory.Category.{v_2, u_2} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n m : ℕ) (h : m + 1 = n) (P : SSetPair) : (homologyδNatTrans R n m h).app P = P.homologyδ R n m h

theorem SSetPair.quasiIso_chainComplexMap {A : Type u_2} [CategoryTheory.Category.{v_2, u_2} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] {P P' : SSetPair} (f : P ⟶ P') (R : A) [QuasiIso (SSet.chainComplexMap f.left R)] [QuasiIso (SSet.chainComplexMap f.right R)] : QuasiIso (chainComplexMap f R)

A morphism of pairs of simplicial sets which is a quasi-isomorphism on the subcomplexes and on the ambient simplicial sets is a quasi-isomorphism on relative chains.

theorem SSetPair.isIso_homologyMap_of_quasiIso {A : Type u_2} [CategoryTheory.Category.{v_2, u_2} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] {P P' : SSetPair} (f : P ⟶ P') (R : A) [QuasiIso (SSet.chainComplexMap f.left R)] [QuasiIso (SSet.chainComplexMap f.right R)] (n : ℕ) : CategoryTheory.IsIso (SSetPair.homologyMap f R n)

A morphism of pairs of simplicial sets which is a quasi-isomorphism on the subcomplexes and on the ambient simplicial sets induces isomorphisms on relative homology.

@[simp]

theorem SSetPair.homologyπ_naturality {D : Type u_3} [CategoryTheory.Category.{v_3, u_3} D] [CategoryTheory.Limits.HasCoproducts D] [CategoryTheory.Preadditive D] [CategoryTheory.CategoryWithHomology D] {P P' : SSetPair} (f : P ⟶ P') (R : D) (n : ℕ) : CategoryTheory.CategoryStruct.comp (SSet.homologyMap f.right R n) (P'.homologyπ R n) = CategoryTheory.CategoryStruct.comp (P.homologyπ R n) (SSetPair.homologyMap f R n)

The quotient maps from ambient to relative simplicial homology are natural in the pair.

@[simp]

theorem SSetPair.homologyπ_naturality_assoc {D : Type u_3} [CategoryTheory.Category.{v_3, u_3} D] [CategoryTheory.Limits.HasCoproducts D] [CategoryTheory.Preadditive D] [CategoryTheory.CategoryWithHomology D] {P P' : SSetPair} (f : P ⟶ P') (R : D) (n : ℕ) {Z : D} (h : P'.homology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (SSet.homologyMap f.right R n) (CategoryTheory.CategoryStruct.comp (P'.homologyπ R n) h) = CategoryTheory.CategoryStruct.comp (P.homologyπ R n) (CategoryTheory.CategoryStruct.comp (SSetPair.homologyMap f R n) h)

The quotient maps from ambient to relative simplicial homology are natural in the pair.