Naturality of the cellular–singular homology comparison

The cellular–singular comparison for finite-dimensional relative CW complexes intertwines the homology map of a cellular chain map with the relative singular homology map of the original continuous map. Thus it compares the functorial homology theories, including their maps, rather than only their objects in each degree.

The underlying identification of cellular cycles with the homology of a skeleton relative to the base is natural without a dimension bound. Both squares use the restrictions of the original map to pairs, and require neither finite cell sets nor chosen singular representatives. Coefficients are any object of an abelian category with coproducts exact for the cell sets of both complexes.

The source is A. Hatcher, Algebraic Topology, Section 2.2, Theorem 2.35 and the discussion of cellular maps following it. The comparison maps and their formulas on cycles are those of TauCeti.cellularCyclesIso and TauCeti.cellularSingularHomologyIso.

theorem TauCeti.cellularCyclesIso_hom_naturality {X Y : Type w} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] {D : Set X} {E : Set Y} (C : Set X) [Topology.RelCWComplex C D] (C' : Set Y) [Topology.RelCWComplex C' E] {f : ↧↑C ⟶ ↧↑C'} (hf : IsCellular C C' f) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C' m)) A] (n : ℕ) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap (cellularChainComplexMap C C' hf R) n) (cellularCyclesIso C' R n).hom = CategoryTheory.CategoryStruct.comp (cellularCyclesIso C R n).hom (TopPair.singularHomologyMap (skeletonBasePairMap C C' hf n) R n)

The identification of cellular cycles with the homology of the skeleton relative to the base is natural under cellular maps, without a dimension bound.

theorem TauCeti.cellularCyclesIso_hom_naturality_assoc {X Y : Type w} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] {D : Set X} {E : Set Y} (C : Set X) [Topology.RelCWComplex C D] (C' : Set Y) [Topology.RelCWComplex C' E] {f : ↧↑C ⟶ ↧↑C'} (hf : IsCellular C C' f) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C' m)) A] (n : ℕ) {Z : A} (h : (skeletonBasePair C' n).singularHomology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap (cellularChainComplexMap C C' hf R) n) (CategoryTheory.CategoryStruct.comp (cellularCyclesIso C' R n).hom h) = CategoryTheory.CategoryStruct.comp (cellularCyclesIso C R n).hom (CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (skeletonBasePairMap C C' hf n) R n) h)

The identification of cellular cycles with the homology of the skeleton relative to the base is natural under cellular maps, without a dimension bound.

theorem TauCeti.cellularCyclesIso_inv_naturality {X Y : Type w} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] {D : Set X} {E : Set Y} (C : Set X) [Topology.RelCWComplex C D] (C' : Set Y) [Topology.RelCWComplex C' E] {f : ↧↑C ⟶ ↧↑C'} (hf : IsCellular C C' f) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C' m)) A] (n : ℕ) : CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (skeletonBasePairMap C C' hf n) R n) (cellularCyclesIso C' R n).inv = CategoryTheory.CategoryStruct.comp (cellularCyclesIso C R n).inv (HomologicalComplex.cyclesMap (cellularChainComplexMap C C' hf R) n)

The inverse identification from relative skeletal homology to cellular cycles is natural under cellular maps, without a dimension bound.

theorem TauCeti.cellularCyclesIso_inv_naturality_assoc {X Y : Type w} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] {D : Set X} {E : Set Y} (C : Set X) [Topology.RelCWComplex C D] (C' : Set Y) [Topology.RelCWComplex C' E] {f : ↧↑C ⟶ ↧↑C'} (hf : IsCellular C C' f) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C' m)) A] (n : ℕ) {Z : A} (h : HomologicalComplex.cycles (cellularChainComplex C' R) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (skeletonBasePairMap C C' hf n) R n) (CategoryTheory.CategoryStruct.comp (cellularCyclesIso C' R n).inv h) = CategoryTheory.CategoryStruct.comp (cellularCyclesIso C R n).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap (cellularChainComplexMap C C' hf R) n) h)

The inverse identification from relative skeletal homology to cellular cycles is natural under cellular maps, without a dimension bound.

theorem TauCeti.cellularSingularHomologyIso_hom_naturality {X Y : Type w} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] {D : Set X} {E : Set Y} (C : Set X) [Topology.RelCWComplex C D] (C' : Set Y) [Topology.RelCWComplex C' E] {f : ↧↑C ⟶ ↧↑C'} (hf : IsCellular C C' f) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C' m)) A] [Topology.RelCWComplex.FiniteDimensional C] [Topology.RelCWComplex.FiniteDimensional C'] (n : ℕ) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (cellularChainComplexMap C C' hf R) n) (cellularSingularHomologyIso C' R n).hom = CategoryTheory.CategoryStruct.comp (cellularSingularHomologyIso C R n).hom (TopPair.singularHomologyMap (complexBasePairMap C C' hf) R n)

The cellular–singular comparison is natural under cellular maps of finite-dimensional relative CW complexes. The singular map is induced by the original map of the whole pairs.

theorem TauCeti.cellularSingularHomologyIso_hom_naturality_assoc {X Y : Type w} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] {D : Set X} {E : Set Y} (C : Set X) [Topology.RelCWComplex C D] (C' : Set Y) [Topology.RelCWComplex C' E] {f : ↧↑C ⟶ ↧↑C'} (hf : IsCellular C C' f) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C' m)) A] [Topology.RelCWComplex.FiniteDimensional C] [Topology.RelCWComplex.FiniteDimensional C'] (n : ℕ) {Z : A} (h : (complexBasePair C').singularHomology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (cellularChainComplexMap C C' hf R) n) (CategoryTheory.CategoryStruct.comp (cellularSingularHomologyIso C' R n).hom h) = CategoryTheory.CategoryStruct.comp (cellularSingularHomologyIso C R n).hom (CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (complexBasePairMap C C' hf) R n) h)

The cellular–singular comparison is natural under cellular maps of finite-dimensional relative CW complexes. The singular map is induced by the original map of the whole pairs.

theorem TauCeti.cellularSingularHomologyIso_inv_naturality {X Y : Type w} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] {D : Set X} {E : Set Y} (C : Set X) [Topology.RelCWComplex C D] (C' : Set Y) [Topology.RelCWComplex C' E] {f : ↧↑C ⟶ ↧↑C'} (hf : IsCellular C C' f) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C' m)) A] [Topology.RelCWComplex.FiniteDimensional C] [Topology.RelCWComplex.FiniteDimensional C'] (n : ℕ) : CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (complexBasePairMap C C' hf) R n) (cellularSingularHomologyIso C' R n).inv = CategoryTheory.CategoryStruct.comp (cellularSingularHomologyIso C R n).inv (HomologicalComplex.homologyMap (cellularChainComplexMap C C' hf R) n)

The inverse cellular–singular comparison is natural under cellular maps of finite-dimensional relative CW complexes.

theorem TauCeti.cellularSingularHomologyIso_inv_naturality_assoc {X Y : Type w} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] {D : Set X} {E : Set Y} (C : Set X) [Topology.RelCWComplex C D] (C' : Set Y) [Topology.RelCWComplex C' E] {f : ↧↑C ⟶ ↧↑C'} (hf : IsCellular C C' f) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C' m)) A] [Topology.RelCWComplex.FiniteDimensional C] [Topology.RelCWComplex.FiniteDimensional C'] (n : ℕ) {Z : A} (h : HomologicalComplex.homology (cellularChainComplex C' R) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (complexBasePairMap C C' hf) R n) (CategoryTheory.CategoryStruct.comp (cellularSingularHomologyIso C' R n).inv h) = CategoryTheory.CategoryStruct.comp (cellularSingularHomologyIso C R n).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (cellularChainComplexMap C C' hf R) n) h)

The inverse cellular–singular comparison is natural under cellular maps of finite-dimensional relative CW complexes.