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 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. 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.

Equations

• SSetPair.chainComplexShortComplexMap f R = { τ₁ := SSet.chainComplexMap f.left R, τ₂ := SSet.chainComplexMap f.right R, τ₃ := SSetPair.chainComplexMap f R, comm₁₂ := ⋯, comm₂₃ := ⋯ }

@[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

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.

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.

Equations

• SSetPair.homologyδNatTrans R n m h = { app := fun (P : SSetPair) => P.homologyδ R n m h, naturality := ⋯ }

@[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.