The relative comparison of cubical and simplicial singular chains

For a topological pair P = (X, A), the relative normalized cubical chain complex P.cubicalChainComplex k is the cokernel of the map of normalized cubical chains induced by the inclusion A → X. This inclusion is injective on normalized chains (NormalizedCubicalChain.map_injective), so the sequence 0 ⟶ N(A) ⟶ N(X) ⟶ N(X, A) ⟶ 0 is short exact (TopPair.shortExact_cubicalChainComplexShortComplex). In each degree it splits, since the push-forward along the inclusion A → X has a left inverse (NormalizedCubicalChain.exists_comp_map_eq_id), so the relative chains are projective modules.

The comparison maps of TauCeti.cubicalSingularHomotopyEquiv are natural, so they carry the chains of A into those of A and induce maps of relative chain complexes in both directions (TopPair.singularToCubicalRel, TopPair.cubicalToSingularRel). By the five lemma, applied to the long exact homology sequences, both are quasi-isomorphisms, so relative cubical homology is relative singular homology (TopPair.singularCubicalHomologyIso), naturally in the pair. Its inverse is induced by TopPair.cubicalToSingularRel, because the natural homotopy between the composite on simplicial chains and the identity descends to relative chains (TopPair.singularToCubicalRelCompHomotopy). The relative homotopy invariance of cubical homology is transported from the simplicial one (TopPair.Homotopy.congr_homologyMap_cubicalChainComplexMap).

Main definitions

• TopPair.cubicalChainComplex k P: the relative normalized cubical chain complex of a pair.
• TopPair.cubicalChainComplexMap k f: the chain map induced by a map of pairs.
• TopPair.IsCubicalRepresentative k c μ: a normalized cubical chain of the ambient space is a relative cycle with relative class μ; every class has one (TopPair.exists_isCubicalRepresentative).
• TopPair.cubicalChainComplexXDesc k g hg: a linear map out of the chains of the ambient space, vanishing on the chains of the subspace, descended to the relative chains.
• TopPair.cubicalChainOfCube k c, TopPair.cubicalCycleOfCube k c hc: a singular cube as a relative chain, and as a relative cycle when it sends the boundary of the cube into the subspace. Linear maps out of the relative chains are determined by their values on these (TopPair.cubicalChainComplexX_linearMap_ext).
• TopPair.cubicalChainComplexMap_f_cubicalChainOfCube, TopPair.cyclesMap_cubicalCycleOfCube: their naturality in maps of pairs, and TopPair.d_cubicalChainOfCube_eq_sum: the relative boundary of a cube is the signed sum of its faces.
• TopPair.cubicalBoundaryChainOfCube k c hc, TopPair.cubicalBoundaryCycleOfCube k c hc: the boundary of a cube sending the boundary of the cube into the subspace, as a chain and as a cycle of the subspace (TopPair.map_cubicalBoundaryChainOfCube).
• TopPair.singularToCubicalRel k P, TopPair.cubicalToSingularRel k P: the relative comparison maps.
• TopPair.singularCubicalHomologyIso k P n: relative cubical homology is relative singular homology.
• TopPair.singularToCubicalRelCompHomotopy k P: the relative comparison maps compose to a map homotopic to the identity on relative simplicial chains.

Main results

• The terms of TopPair.cubicalChainComplex k P are projective k-modules (an instance).
• TopPair.quasiIso_singularToCubicalRel, TopPair.quasiIso_cubicalToSingularRel: the relative comparison maps are quasi-isomorphisms.
• TopPair.Homotopy.congr_homologyMap_cubicalChainComplexMap: homotopic maps of pairs induce the same map on relative cubical homology.

References

• W. S. Massey, Singular Homology Theory, GTM 70, Springer, 1980, Chapter VII.
• S. Eilenberg and N. Steenrod, Foundations of Algebraic Topology, Princeton, 1952, Chapters I–III.

instance TopPair.mono_normalizedCubicalChainComplex_map (k : Type u) [Ring k] (P : TopPair) : CategoryTheory.Mono ((TauCeti.normalizedCubicalChainComplex k).map map)

The inclusion of a subspace induces a monomorphism of normalized cubical chains.

@[reducible, inline]

noncomputable abbrev TopPair.cubicalChainComplex (k : Type u) [Ring k] (P : TopPair) : ChainComplex (ModuleCat k) ℕ

The relative normalized cubical chain complex of a topological pair (X, A): the cokernel of the map of normalized cubical chains induced by the inclusion A → X.

@[simp]

theorem TopPair.cubicalChainComplex_condition_f (k : Type u) [Ring k] (P : TopPair) (n : ℕ) : CategoryTheory.CategoryStruct.comp (((TauCeti.normalizedCubicalChainComplex k).map map).f n) ((CategoryTheory.Limits.cokernel.π ((TauCeti.normalizedCubicalChainComplex k).map map)).f n) = 0

The chains of the subspace vanish degreewise in the relative normalized cubical chains of a pair.

@[simp]

theorem TopPair.cubicalChainComplex_condition_f_assoc (k : Type u) [Ring k] (P : TopPair) (n : ℕ) {Z : ModuleCat k} (h : (CategoryTheory.Limits.cokernel ((TauCeti.normalizedCubicalChainComplex k).map map)).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (((TauCeti.normalizedCubicalChainComplex k).map map).f n) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.cokernel.π ((TauCeti.normalizedCubicalChainComplex k).map map)).f n) h) = CategoryTheory.CategoryStruct.comp 0 h

The chains of the subspace vanish degreewise in the relative normalized cubical chains of a pair.

@[reducible, inline]

noncomputable abbrev TopPair.cubicalChainComplexShortComplex (k : Type u) [Ring k] (P : TopPair) : CategoryTheory.ShortComplex (ChainComplex (ModuleCat k) ℕ)

The sequence N(A) ⟶ N(X) ⟶ N(X, A) of normalized cubical chain complexes of a pair.

theorem TopPair.shortExact_cubicalChainComplexShortComplex (k : Type u) [Ring k] (P : TopPair) : (cubicalChainComplexShortComplex k P).ShortExact

The normalized cubical chain sequence of a pair is short exact.

instance TopPair.instProjectiveCarrierXNatModuleCatCubicalChainComplex (k : Type u) [Ring k] (P : TopPair) (n : ℕ) : Module.Projective k ↑((cubicalChainComplex k P).X n)

The terms of the relative normalized cubical chain complex of a pair are projective: the chains of the subspace split off the chains of the ambient space (TauCeti.NormalizedCubicalChain.exists_comp_map_eq_id), so the relative chains are a direct summand of the projective chains of the ambient space.

def TopPair.IsCubicalRepresentative (k : Type u) [Ring k] (P : TopPair) {n : ℕ} (c : TauCeti.NormalizedCubicalChain (↑fst) k n) (μ : ↑(HomologicalComplex.homology (cubicalChainComplex k P) n)) : Prop

A normalized cubical n-chain c of the ambient space of a pair (X, A) represents the class μ of the relative cubical homology Hₙ(X, A) when its image in the relative chains is a relative cycle whose class is μ.

theorem TopPair.isCubicalRepresentative_iff {k : Type u} [Ring k] {P : TopPair} {n : ℕ} (c : TauCeti.NormalizedCubicalChain (↑fst) k n) (μ : ↑(HomologicalComplex.homology (cubicalChainComplex k P) n)) : IsCubicalRepresentative k P c μ ↔ ∃ (r : ↑(HomologicalComplex.cycles (cubicalChainComplex k P) n)), (ModuleCat.Hom.hom ((CategoryTheory.Limits.cokernel.π ((TauCeti.normalizedCubicalChainComplex k).map map)).f n)) c = (ModuleCat.Hom.hom (HomologicalComplex.iCycles (cubicalChainComplex k P) n)) r ∧ (ModuleCat.Hom.hom (HomologicalComplex.homologyπ (cubicalChainComplex k P) n)) r = μ

theorem TopPair.exists_isCubicalRepresentative (k : Type u) [Ring k] (P : TopPair) {n : ℕ} (μ : ↑(HomologicalComplex.homology (cubicalChainComplex k P) n)) : ∃ (c : TauCeti.NormalizedCubicalChain (↑fst) k n), IsCubicalRepresentative k P c μ

Every class of the relative cubical homology of a pair is represented by a chain of the ambient space.

noncomputable def TopPair.cubicalChainComplexXDesc (k : Type u) [Ring k] {P : TopPair} {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module k M] (g : TauCeti.NormalizedCubicalChain (↑fst) k n →ₗ[k] M) (hg : g ∘ₗ TauCeti.NormalizedCubicalChain.map k (TopCat.Hom.hom map) n = 0) : ↑((cubicalChainComplex k P).X n) →ₗ[k] M

A linear map out of the normalized cubical n-chains of the ambient space of a pair which vanishes on the chains of the subspace, descended to the relative chains (TopPair.cubicalChainComplexXDesc_π).

@[simp]

theorem TopPair.cubicalChainComplexXDesc_π (k : Type u) [Ring k] {P : TopPair} {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module k M] (g : TauCeti.NormalizedCubicalChain (↑fst) k n →ₗ[k] M) (hg : g ∘ₗ TauCeti.NormalizedCubicalChain.map k (TopCat.Hom.hom map) n = 0) (x : ↑(((TauCeti.normalizedCubicalChainComplex k).obj fst).X n)) : (cubicalChainComplexXDesc k g hg) ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Limits.cokernel.π ((TauCeti.normalizedCubicalChainComplex k).map map)).f n)) x) = g x

noncomputable def TopPair.cubicalChainComplexMap (k : Type u) [Ring k] {P P' : TopPair} (f : P ⟶ P') : cubicalChainComplex k P ⟶ cubicalChainComplex k P'

The map of relative normalized cubical chains induced by a map of pairs.

@[simp]

theorem TopPair.π_cubicalChainComplexMap (k : Type u) [Ring k] {P P' : TopPair} (f : P ⟶ P') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π ((TauCeti.normalizedCubicalChainComplex k).map map)) (cubicalChainComplexMap k f) = CategoryTheory.CategoryStruct.comp ((TauCeti.normalizedCubicalChainComplex k).map (Hom.fst f)) (CategoryTheory.Limits.cokernel.π ((TauCeti.normalizedCubicalChainComplex k).map map))

@[simp]

theorem TopPair.π_cubicalChainComplexMap_assoc (k : Type u) [Ring k] {P P' : TopPair} (f : P ⟶ P') {Z : ChainComplex (ModuleCat k) ℕ} (h : cubicalChainComplex k P' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π ((TauCeti.normalizedCubicalChainComplex k).map map)) (CategoryTheory.CategoryStruct.comp (cubicalChainComplexMap k f) h) = CategoryTheory.CategoryStruct.comp ((TauCeti.normalizedCubicalChainComplex k).map (Hom.fst f)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π ((TauCeti.normalizedCubicalChainComplex k).map map)) h)

@[simp]

theorem TopPair.cubicalChainComplexMap_id (k : Type u) [Ring k] (P : TopPair) : cubicalChainComplexMap k (CategoryTheory.CategoryStruct.id P) = CategoryTheory.CategoryStruct.id (cubicalChainComplex k P)

@[simp]

theorem TopPair.cubicalChainComplexMap_comp (k : Type u) [Ring k] {P P' P'' : TopPair} (f : P ⟶ P') (g : P' ⟶ P'') : cubicalChainComplexMap k (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (cubicalChainComplexMap k f) (cubicalChainComplexMap k g)

Singular cubes as relative chains

noncomputable def TopPair.cubicalChainOfCube (k : Type u) [Ring k] {P : TopPair} {m : ℕ} (c : TauCeti.SingularCube (↑fst) m) : ↑((cubicalChainComplex k P).X m)

A singular cube of the ambient space of P, as a relative normalized cubical chain of P.

theorem TopPair.cubicalChainOfCube_def (k : Type u) [Ring k] {P : TopPair} {m : ℕ} (c : TauCeti.SingularCube (↑fst) m) : cubicalChainOfCube k c = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Limits.cokernel.π ((TauCeti.normalizedCubicalChainComplex k).map map)).f m)) ((TauCeti.normalizedCubicalChainComplexXEquiv fst m).symm (TauCeti.NormalizedCubicalChain.ofCube (↑fst) k c))

@[simp]

theorem TopPair.cubicalChainOfCube_eq_zero (k : Type u) [Ring k] {P : TopPair} {m : ℕ} {c : TauCeti.SingularCube (↑fst) m} (hc : c.IsDegenerate) : cubicalChainOfCube k c = 0

A degenerate cube vanishes as a relative chain.

@[simp]

theorem TopPair.cubicalChainOfCube_map_comp_eq_zero (k : Type u) [Ring k] {P : TopPair} {m : ℕ} (c : TauCeti.SingularCube (↑snd) m) : cubicalChainOfCube k ((TopCat.Hom.hom map).comp c) = 0

A cube of the subspace vanishes as a relative chain.

theorem TopPair.d_cubicalChainOfCube_eq_sum (k : Type u) [Ring k] {P : TopPair} {m : ℕ} (c : TauCeti.SingularCube (↑fst) (m + 1)) : (CategoryTheory.ConcreteCategory.hom ((cubicalChainComplex k P).d (m + 1) m)) (cubicalChainOfCube k c) = ∑ i : Fin (m + 1), (-1) ^ ↑i • (cubicalChainOfCube k (TauCeti.SingularCube.face i 0 c) - cubicalChainOfCube k (TauCeti.SingularCube.face i 1 c))

The relative boundary of a cube is the signed sum of the relative chains of its faces.

theorem TopPair.cubicalChainComplexX_linearMap_ext {k : Type u} [Ring k] {P : TopPair} {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module k M] {f₁ f₂ : ↑((cubicalChainComplex k P).X n) →ₗ[k] M} (h : ∀ (c : TauCeti.SingularCube (↑fst) n), f₁ (cubicalChainOfCube k c) = f₂ (cubicalChainOfCube k c)) : f₁ = f₂

Two linear maps out of the relative normalized cubical n-chains of a pair agree if they agree on the relative chain of every cube.

theorem TopPair.cubicalChainComplexX_linearMap_ext_iff {k : Type u} [Ring k] {P : TopPair} {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module k M] {f₁ f₂ : ↑((cubicalChainComplex k P).X n) →ₗ[k] M} : f₁ = f₂ ↔ ∀ (c : TauCeti.SingularCube (↑fst) n), f₁ (cubicalChainOfCube k c) = f₂ (cubicalChainOfCube k c)

@[simp]

theorem TopPair.cubicalChainComplexXDesc_cubicalChainOfCube (k : Type u) [Ring k] {P : TopPair} {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module k M] (g : TauCeti.NormalizedCubicalChain (↑fst) k n →ₗ[k] M) (hg : g ∘ₗ TauCeti.NormalizedCubicalChain.map k (TopCat.Hom.hom map) n = 0) (c : TauCeti.SingularCube (↑fst) n) : (cubicalChainComplexXDesc k g hg) (cubicalChainOfCube k c) = g (TauCeti.NormalizedCubicalChain.ofCube (↑fst) k c)

The descent of a linear map g to the relative chains takes the relative chain of a cube c to the value of g on the class of c.

@[simp]

theorem TopPair.cubicalChainComplexMap_f_cubicalChainOfCube (k : Type u) [Ring k] {P P' : TopPair} (f : P ⟶ P') {m : ℕ} (c : TauCeti.SingularCube (↑fst) m) : (CategoryTheory.ConcreteCategory.hom ((cubicalChainComplexMap k f).f m)) (cubicalChainOfCube k c) = cubicalChainOfCube k ((TopCat.Hom.hom (Hom.fst f)).comp c)

The chain map induced by a map of pairs f sends the relative chain of a cube c to that of f ∘ c.

theorem TopPair.d_cubicalChainOfCube (k : Type u) [Ring k] {P : TopPair} {m : ℕ} {c : TauCeti.SingularCube (↑fst) (m + 1)} (hc : Set.MapsTo (⇑c) (Cube.boundary (Fin (m + 1))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom map))) : (CategoryTheory.ConcreteCategory.hom ((cubicalChainComplex k P).d (m + 1) m)) (cubicalChainOfCube k c) = 0

A singular cube sending the boundary of the cube into the subspace is a relative cycle.

noncomputable def TopPair.cubicalCycleOfCube (k : Type u) [Ring k] {P : TopPair} {m : ℕ} (c : TauCeti.SingularCube (↑fst) (m + 1)) (hc : Set.MapsTo (⇑c) (Cube.boundary (Fin (m + 1))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom map))) : ↑(HomologicalComplex.cycles (cubicalChainComplex k P) (m + 1))

A singular cube sending the boundary of the cube into the subspace, as a relative cycle of the normalized cubical chains of P.

@[simp]

theorem TopPair.iCycles_cubicalCycleOfCube (k : Type u) [Ring k] {P : TopPair} {m : ℕ} (c : TauCeti.SingularCube (↑fst) (m + 1)) (hc : Set.MapsTo (⇑c) (Cube.boundary (Fin (m + 1))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom map))) : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (cubicalChainComplex k P) (m + 1))) (cubicalCycleOfCube k c hc) = cubicalChainOfCube k c

theorem TopPair.cyclesMap_cubicalCycleOfCube (k : Type u) [Ring k] {P P' : TopPair} (f : P ⟶ P') {m : ℕ} (c : TauCeti.SingularCube (↑fst) (m + 1)) (hc : Set.MapsTo (⇑c) (Cube.boundary (Fin (m + 1))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom map))) (hfc : Set.MapsTo (⇑((TopCat.Hom.hom (Hom.fst f)).comp c)) (Cube.boundary (Fin (m + 1))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom map))) : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.cyclesMap (cubicalChainComplexMap k f) (m + 1))) (cubicalCycleOfCube k c hc) = cubicalCycleOfCube k ((TopCat.Hom.hom (Hom.fst f)).comp c) hfc

The map on cycles induced by a map of pairs f sends the relative cycle of a cube c to that of f ∘ c.

The boundary of a relative cube

noncomputable def TopPair.cubicalBoundaryChainOfCube (k : Type u) [Ring k] {P : TopPair} {m : ℕ} (c : TauCeti.SingularCube (↑fst) (m + 1)) (hc : Set.MapsTo (⇑c) (Cube.boundary (Fin (m + 1))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom map))) : TauCeti.NormalizedCubicalChain (↑snd) k m

The boundary of a relative cube, read in the subspace. A singular cube c of X sending the boundary of the cube into A has its faces in A, and this is the signed sum ∑ᵢ (-1)ⁱ (cᵢ⁰ - cᵢ¹) of these faces as a normalized cubical chain of A. Its image in X is the boundary of c (TopPair.map_cubicalBoundaryChainOfCube).

theorem TopPair.cubicalBoundaryChainOfCube_def (k : Type u) [Ring k] {P : TopPair} {m : ℕ} (c : TauCeti.SingularCube (↑fst) (m + 1)) (hc : Set.MapsTo (⇑c) (Cube.boundary (Fin (m + 1))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom map))) : cubicalBoundaryChainOfCube k c hc = ∑ i : Fin (m + 1), (-1) ^ ↑i • (TauCeti.NormalizedCubicalChain.ofCube (↑snd) k (P.liftSnd (TauCeti.SingularCube.face i 0 c) ⋯) - TauCeti.NormalizedCubicalChain.ofCube (↑snd) k (P.liftSnd (TauCeti.SingularCube.face i 1 c) ⋯))

The boundary of a relative cube is the signed sum ∑ᵢ (-1)ⁱ (cᵢ⁰ - cᵢ¹) of its faces, lifted to the subspace.

@[simp]

theorem TopPair.map_cubicalBoundaryChainOfCube (k : Type u) [Ring k] {P : TopPair} {m : ℕ} (c : TauCeti.SingularCube (↑fst) (m + 1)) (hc : Set.MapsTo (⇑c) (Cube.boundary (Fin (m + 1))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom map))) : (TauCeti.NormalizedCubicalChain.map k (TopCat.Hom.hom map) m) (cubicalBoundaryChainOfCube k c hc) = (TauCeti.NormalizedCubicalChain.boundary (↑fst) k m) (TauCeti.NormalizedCubicalChain.ofCube (↑fst) k c)

The boundary of a relative cube, read in the subspace, is carried to the boundary of the cube by the inclusion of the subspace.

@[simp]

theorem TopPair.boundary_cubicalBoundaryChainOfCube (k : Type u) [Ring k] {P : TopPair} {m : ℕ} (c : TauCeti.SingularCube (↑fst) (m + 2)) (hc : Set.MapsTo (⇑c) (Cube.boundary (Fin (m + 2))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom map))) : (TauCeti.NormalizedCubicalChain.boundary (↑snd) k m) (cubicalBoundaryChainOfCube k c hc) = 0

The boundary of a relative cube, read in the subspace, is a cycle.

@[simp]

theorem TopPair.d_cubicalBoundaryChainOfCube (k : Type u) [Ring k] {P : TopPair} {m : ℕ} (c : TauCeti.SingularCube (↑fst) (m + 1)) (hc : Set.MapsTo (⇑c) (Cube.boundary (Fin (m + 1))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom map))) (j : ℕ) : (CategoryTheory.ConcreteCategory.hom (((TauCeti.normalizedCubicalChainComplex k).obj snd).d m j)) (cubicalBoundaryChainOfCube k c hc) = 0

The boundary of a relative cube, read in the subspace, is killed by every differential of the normalized cubical chain complex of the subspace.

noncomputable def TopPair.cubicalBoundaryCycleOfCube (k : Type u) [Ring k] {P : TopPair} {m : ℕ} (c : TauCeti.SingularCube (↑fst) (m + 1)) (hc : Set.MapsTo (⇑c) (Cube.boundary (Fin (m + 1))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom map))) : ↑(HomologicalComplex.cycles ((TauCeti.normalizedCubicalChainComplex k).obj snd) m)

The boundary of a singular cube c of X sending the boundary of the cube into A, as a normalized cubical cycle of A.

@[simp]

theorem TopPair.iCycles_cubicalBoundaryCycleOfCube (k : Type u) [Ring k] {P : TopPair} {m : ℕ} (c : TauCeti.SingularCube (↑fst) (m + 1)) (hc : Set.MapsTo (⇑c) (Cube.boundary (Fin (m + 1))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom map))) : (ModuleCat.Hom.hom (HomologicalComplex.iCycles ((TauCeti.normalizedCubicalChainComplex k).obj snd) m)) (cubicalBoundaryCycleOfCube k c hc) = cubicalBoundaryChainOfCube k c hc

The relative comparison maps

noncomputable def TopPair.singularRelπ (k : Type u) [Ring k] (P : TopPair) : (TauCeti.singularChains k).obj fst ⟶ P.singularChainComplex ↧k

The quotient map from the simplicial singular chains of the ambient space to the relative singular chains, with its source written as (singularChains k).obj P.fst.

instance TopPair.instEpiChainComplexModuleCatNatSingularRelπ (k : Type u) [Ring k] (P : TopPair) : CategoryTheory.Epi (singularRelπ k P)

theorem TopPair.singularRelπ_naturality (k : Type u) [Ring k] {P P' : TopPair} (f : P ⟶ P') : CategoryTheory.CategoryStruct.comp ((TauCeti.singularChains k).map (Hom.fst f)) (singularRelπ k P') = CategoryTheory.CategoryStruct.comp (singularRelπ k P) (singularChainComplexMap f ↧k)

theorem TopPair.singularRelπ_naturality_assoc (k : Type u) [Ring k] {P P' : TopPair} (f : P ⟶ P') {Z : ChainComplex (ModuleCat k) ℕ} (h : P'.singularChainComplex ↧k ⟶ Z) : CategoryTheory.CategoryStruct.comp ((TauCeti.singularChains k).map (Hom.fst f)) (CategoryTheory.CategoryStruct.comp (singularRelπ k P') h) = CategoryTheory.CategoryStruct.comp (singularRelπ k P) (CategoryTheory.CategoryStruct.comp (singularChainComplexMap f ↧k) h)

theorem TopPair.singularRelπ_hom_ext (k : Type u) [Ring k] {P : TopPair} {T : ChainComplex (ModuleCat k) ℕ} {g g' : P.singularChainComplex ↧k ⟶ T} (h : CategoryTheory.CategoryStruct.comp (singularRelπ k P) g = CategoryTheory.CategoryStruct.comp (singularRelπ k P) g') : g = g'

noncomputable def TopPair.singularToCubicalRel (k : Type u) [Ring k] (P : TopPair) : P.singularChainComplex ↧k ⟶ cubicalChainComplex k P

The comparison map from relative simplicial to relative cubical chains, induced by singularToCubical.

@[simp]

theorem TopPair.singularRelπ_singularToCubicalRel (k : Type u) [Ring k] (P : TopPair) : CategoryTheory.CategoryStruct.comp (singularRelπ k P) (singularToCubicalRel k P) = CategoryTheory.CategoryStruct.comp ((TauCeti.singularToCubical k).app fst) (CategoryTheory.Limits.cokernel.π ((TauCeti.normalizedCubicalChainComplex k).map map))

@[simp]

theorem TopPair.singularRelπ_singularToCubicalRel_assoc (k : Type u) [Ring k] (P : TopPair) {Z : ChainComplex (ModuleCat k) ℕ} (h : cubicalChainComplex k P ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularRelπ k P) (CategoryTheory.CategoryStruct.comp (singularToCubicalRel k P) h) = CategoryTheory.CategoryStruct.comp ((TauCeti.singularToCubical k).app fst) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π ((TauCeti.normalizedCubicalChainComplex k).map map)) h)

noncomputable def TopPair.cubicalToSingularRel (k : Type u) [Ring k] (P : TopPair) : cubicalChainComplex k P ⟶ P.singularChainComplex ↧k

The comparison map from relative cubical to relative simplicial chains, induced by cubicalToSingular.

@[simp]

theorem TopPair.π_cubicalToSingularRel (k : Type u) [Ring k] (P : TopPair) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π ((TauCeti.normalizedCubicalChainComplex k).map map)) (cubicalToSingularRel k P) = CategoryTheory.CategoryStruct.comp ((TauCeti.cubicalToSingular k).app fst) (singularRelπ k P)

@[simp]

theorem TopPair.π_cubicalToSingularRel_assoc (k : Type u) [Ring k] (P : TopPair) {Z : ChainComplex (ModuleCat k) ℕ} (h : P.singularChainComplex ↧k ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π ((TauCeti.normalizedCubicalChainComplex k).map map)) (CategoryTheory.CategoryStruct.comp (cubicalToSingularRel k P) h) = CategoryTheory.CategoryStruct.comp ((TauCeti.cubicalToSingular k).app fst) (CategoryTheory.CategoryStruct.comp (singularRelπ k P) h)

noncomputable def TopPair.singularToCubicalShortComplex (k : Type u) [Ring k] (P : TopPair) : P.singularChainComplexShortComplex ↧k ⟶ cubicalChainComplexShortComplex k P

The comparison maps as a morphism of short complexes from the simplicial chain sequence of a pair to the cubical one.

@[simp]

theorem TopPair.singularToCubicalShortComplex_τ₁ (k : Type u) [Ring k] (P : TopPair) : (singularToCubicalShortComplex k P).τ₁ = (TauCeti.singularToCubical k).app snd

@[simp]

theorem TopPair.singularToCubicalShortComplex_τ₂ (k : Type u) [Ring k] (P : TopPair) : (singularToCubicalShortComplex k P).τ₂ = (TauCeti.singularToCubical k).app fst

@[simp]

theorem TopPair.singularToCubicalShortComplex_τ₃ (k : Type u) [Ring k] (P : TopPair) : (singularToCubicalShortComplex k P).τ₃ = singularToCubicalRel k P

noncomputable def TopPair.cubicalToSingularShortComplex (k : Type u) [Ring k] (P : TopPair) : cubicalChainComplexShortComplex k P ⟶ P.singularChainComplexShortComplex ↧k

The comparison maps as a morphism of short complexes from the cubical chain sequence of a pair to the simplicial one.

noncomputable def TopPair.singularToCubicalRelCompHomotopy (k : Type u) [Ring k] (P : TopPair) : _root_.Homotopy (CategoryTheory.CategoryStruct.comp (singularToCubicalRel k P) (cubicalToSingularRel k P)) (CategoryTheory.CategoryStruct.id (P.singularChainComplex ↧k))

The relative comparison maps compose, on relative simplicial chains, to a map chain homotopic to the identity: the natural homotopy singularToCubicalCompHomotopy descends to the quotient by the chains of the subspace.

@[simp]

theorem TopPair.singularRelπ_singularToCubicalRelCompHomotopy_hom (k : Type u) [Ring k] (P : TopPair) (i j : ℕ) : CategoryTheory.CategoryStruct.comp ((singularRelπ k P).f i) ((singularToCubicalRelCompHomotopy k P).hom i j) = CategoryTheory.CategoryStruct.comp ((TauCeti.singularToCubicalCompHomotopy k fst).hom i j) ((singularRelπ k P).f j)

The quotient equation for the homotopy operator on relative simplicial chains.

@[simp]

theorem TopPair.singularRelπ_singularToCubicalRelCompHomotopy_hom_assoc (k : Type u) [Ring k] (P : TopPair) (i j : ℕ) {Z : ModuleCat k} (h : (P.singularChainComplex ↧k).X j ⟶ Z) : CategoryTheory.CategoryStruct.comp ((singularRelπ k P).f i) (CategoryTheory.CategoryStruct.comp ((singularToCubicalRelCompHomotopy k P).hom i j) h) = CategoryTheory.CategoryStruct.comp ((TauCeti.singularToCubicalCompHomotopy k fst).hom i j) (CategoryTheory.CategoryStruct.comp ((singularRelπ k P).f j) h)

The quotient equation for the homotopy operator on relative simplicial chains.

instance TopPair.quasiIso_singularToCubicalRel (k : Type u) [Ring k] (P : TopPair) : QuasiIso (singularToCubicalRel k P)

The relative comparison map to cubical chains is a quasi-isomorphism.

instance TopPair.quasiIso_cubicalToSingularRel (k : Type u) [Ring k] (P : TopPair) : QuasiIso (cubicalToSingularRel k P)

The relative comparison map to simplicial chains is a quasi-isomorphism.

theorem TopPair.singularToCubicalRel_naturality (k : Type u) [Ring k] {P P' : TopPair} (f : P ⟶ P') : CategoryTheory.CategoryStruct.comp (singularToCubicalRel k P) (cubicalChainComplexMap k f) = CategoryTheory.CategoryStruct.comp (singularChainComplexMap f ↧k) (singularToCubicalRel k P')

The relative comparison map to cubical chains is natural in the pair.

theorem TopPair.singularToCubicalRel_naturality_assoc (k : Type u) [Ring k] {P P' : TopPair} (f : P ⟶ P') {Z : ChainComplex (ModuleCat k) ℕ} (h : cubicalChainComplex k P' ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularToCubicalRel k P) (CategoryTheory.CategoryStruct.comp (cubicalChainComplexMap k f) h) = CategoryTheory.CategoryStruct.comp (singularChainComplexMap f ↧k) (CategoryTheory.CategoryStruct.comp (singularToCubicalRel k P') h)

The relative comparison map to cubical chains is natural in the pair.

noncomputable def TopPair.singularCubicalHomologyIso (k : Type u) [Ring k] (P : TopPair) (n : ℕ) : P.singularHomology (↧k) n ≅ HomologicalComplex.homology (cubicalChainComplex k P) n

Relative cubical singular homology is relative singular homology.

@[simp]

theorem TopPair.singularCubicalHomologyIso_hom (k : Type u) [Ring k] (P : TopPair) (n : ℕ) : (singularCubicalHomologyIso k P n).hom = HomologicalComplex.homologyMap (singularToCubicalRel k P) n

@[simp]

theorem TopPair.singularCubicalHomologyIso_inv (k : Type u) [Ring k] (P : TopPair) (n : ℕ) : (singularCubicalHomologyIso k P n).inv = HomologicalComplex.homologyMap (cubicalToSingularRel k P) n

theorem TopPair.singularCubicalHomologyIso_hom_naturality (k : Type u) [Ring k] {P P' : TopPair} (f : P ⟶ P') (n : ℕ) : CategoryTheory.CategoryStruct.comp (singularCubicalHomologyIso k P n).hom (HomologicalComplex.homologyMap (cubicalChainComplexMap k f) n) = CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap f (↧k) n) (singularCubicalHomologyIso k P' n).hom

The relative comparison isomorphism on homology is natural in the pair.

theorem TopPair.singularCubicalHomologyIso_hom_naturality_assoc (k : Type u) [Ring k] {P P' : TopPair} (f : P ⟶ P') (n : ℕ) {Z : ModuleCat k} (h : HomologicalComplex.homology (cubicalChainComplex k P') n ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularCubicalHomologyIso k P n).hom (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (cubicalChainComplexMap k f) n) h) = CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap f (↧k) n) (CategoryTheory.CategoryStruct.comp (singularCubicalHomologyIso k P' n).hom h)

The relative comparison isomorphism on homology is natural in the pair.

theorem TopPair.singularCubicalHomologyIso_inv_naturality (k : Type u) [Ring k] {P P' : TopPair} (f : P ⟶ P') (n : ℕ) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (cubicalChainComplexMap k f) n) (singularCubicalHomologyIso k P' n).inv = CategoryTheory.CategoryStruct.comp (singularCubicalHomologyIso k P n).inv (TopPair.singularHomologyMap f (↧k) n)

The inverse of the relative comparison isomorphism on homology is natural in the pair.

theorem TopPair.singularCubicalHomologyIso_inv_naturality_assoc (k : Type u) [Ring k] {P P' : TopPair} (f : P ⟶ P') (n : ℕ) {Z : ModuleCat k} (h : P'.singularHomology (↧k) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (cubicalChainComplexMap k f) n) (CategoryTheory.CategoryStruct.comp (singularCubicalHomologyIso k P' n).inv h) = CategoryTheory.CategoryStruct.comp (singularCubicalHomologyIso k P n).inv (CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap f (↧k) n) h)

The inverse of the relative comparison isomorphism on homology is natural in the pair.

theorem TopPair.homologyMap_π_comp_singularCubicalHomologyIso_inv (k : Type u) [Ring k] (P : TopPair) (n : ℕ) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (CategoryTheory.Limits.cokernel.π ((TauCeti.normalizedCubicalChainComplex k).map map)) n) (singularCubicalHomologyIso k P n).inv = CategoryTheory.CategoryStruct.comp (TauCeti.singularCubicalHomologyIso k fst n).inv (P.singularHomologyπ (↧k) n)

The inverse comparison isomorphisms of absolute and relative homology commute with the maps from absolute to relative homology: an absolute cubical class, read in relative cubical homology and then in relative singular homology, is its image in absolute singular homology read in relative singular homology.

theorem TopPair.homologyMap_π_comp_singularCubicalHomologyIso_inv_assoc (k : Type u) [Ring k] (P : TopPair) (n : ℕ) {Z : ModuleCat k} (h : P.singularHomology (↧k) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (CategoryTheory.Limits.cokernel.π ((TauCeti.normalizedCubicalChainComplex k).map map)) n) (CategoryTheory.CategoryStruct.comp (singularCubicalHomologyIso k P n).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (TauCeti.singularCubicalHomologyIso k fst n).inv (P.singularHomologyπ (↧k) n)) h

The inverse comparison isomorphisms of absolute and relative homology commute with the maps from absolute to relative homology: an absolute cubical class, read in relative cubical homology and then in relative singular homology, is its image in absolute singular homology read in relative singular homology.

theorem TopPair.Homotopy.congr_homologyMap_cubicalChainComplexMap {k : Type u} [Ring k] {P P' : TopPair} {f g : P ⟶ P'} (H : Homotopy f g) (n : ℕ) : HomologicalComplex.homologyMap (cubicalChainComplexMap k f) n = HomologicalComplex.homologyMap (cubicalChainComplexMap k g) n

Homotopic maps of pairs induce the same map on relative cubical homology, transported from relative singular homology through the relative comparison.