The characteristic maps of the n-cells induce isomorphisms on relative homology

For a relative CW complex, the characteristic maps of the n-cells assemble into a map of pairs TauCeti.characteristicPairMap C n : ∐ⱼ (Dⁿ, Sⁿ⁻¹) ⟶ (Xⁿ, Xⁿ⁻¹) from the disjoint union, over the n-cells j, of copies of the closed unit ball of Fin n → ℝ relative to their boundary spheres (TauCeti.sigmaDiskPair) to the skeletal pair. This map induces isomorphisms on relative singular homology in every degree; in degree n it identifies the cellular chain group Hₙ(Xⁿ, Xⁿ⁻¹) with the relative homology of the disjoint union of the disk pairs, through maps of pairs rather than abstract isomorphisms.

The proof compares both pairs with their versions in which the subspace has been thickened. On the side of the complex, TauCeti.isIso_singularHomologyMap_skeletonPairToNeighborhood replaces Xⁿ⁻¹ by its neighbourhood TauCeti.skeletonNeighborhood C n, obtained by removing the inner half of every open n-cell. On the side of the disks, the radial deformation TauCeti.radialPush 2⁻¹ replaces the boundary spheres by the shells 2⁻¹ ≤ ‖y‖ ≤ 1. The characteristic maps carry the thickened disk pairs to the thickened skeletal pair, and both thickened pairs contain the disjoint union of the open balls relative to their open shells: in the disks this is excision of the boundary spheres, and in the complex, where the open balls map homeomorphically onto the open n-cells (TauCeti.iUnionOpenCellHomeomorph), it is excision of Xⁿ⁻¹.

Main definitions and results

• TauCeti.sigmaDiskPair ι n: the pair ∐ᵢ (Dⁿ, Sⁿ⁻¹).
• TauCeti.characteristicPairMap C n: the characteristic maps of the n-cells, as a map of pairs ∐ⱼ (Dⁿ, Sⁿ⁻¹) ⟶ (Xⁿ, Xⁿ⁻¹).
• TauCeti.isIso_singularHomologyMap_characteristicPairMap: it induces isomorphisms on relative singular homology in every degree.
• TauCeti.cellularChainGroupIsoSigmaDiskPair: the resulting isomorphism from the cellular chain group Hₙ(Xⁿ, Xⁿ⁻¹) to the relative homology of ∐ⱼ (Dⁿ, Sⁿ⁻¹).

References

• A. Hatcher, Algebraic Topology, Section 2.2, Lemma 2.34 and its proof, and Proposition 2.22 for the comparison through good pairs.

@[reducible, inline]

abbrev TauCeti.sigmaDiskPair (ι : Type w) (n : ℕ) : TopPair

The pair ∐ᵢ (Dⁿ, Sⁿ⁻¹): the disjoint union, over i : ι, of copies of the closed unit ball of Fin n → ℝ, relative to the disjoint union of their boundary spheres. The closed unit ball is the domain of the characteristic maps of the n-cells of a CW complex.

Equations

• TauCeti.sigmaDiskPair ι n = TopPair.ofSubset {p : ↑↧((_ : ι) × ↑(Metric.closedBall 0 1)) | ‖↑p.snd‖ = 1}

def TauCeti.characteristicPairMap {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : sigmaDiskPair (Topology.RelCWComplex.cell C n) n ⟶ skeletonPair C n

The characteristic maps of the n-cells, as a map of pairs ∐ⱼ (Dⁿ, Sⁿ⁻¹) ⟶ (Xⁿ, Xⁿ⁻¹) from TauCeti.sigmaDiskPair to the skeletal pair TauCeti.skeletonPair C n. The boundary sphere of each disk lands in Xⁿ⁻¹ = skeletonLT C n because the frontier of an n-cell does.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.characteristicPairMap_fst_apply {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) (p : (_ : Topology.RelCWComplex.cell C n) × ↑(Metric.closedBall 0 1)) : ↑((CategoryTheory.ConcreteCategory.hom (TopPair.Hom.fst (characteristicPairMap C n))) p) = ↑(Topology.RelCWComplex.map n p.fst) ↑p.snd

@[simp]

theorem TauCeti.characteristicPairMap_snd_apply {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) (p : { p : (_ : Topology.RelCWComplex.cell C n) × ↑(Metric.closedBall 0 1) // ‖↑p.snd‖ = 1 }) : ↑((CategoryTheory.ConcreteCategory.hom (TopPair.Hom.snd (characteristicPairMap C n))) p) = ↑(Topology.RelCWComplex.map n (↑p).fst) ↑(↑p).snd

instance TauCeti.isIso_singularHomologyMap_characteristicPairMap {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n k : ℕ) : CategoryTheory.IsIso (TopPair.singularHomologyMap (characteristicPairMap C n) R k)

The characteristic maps of the n-cells induce isomorphisms Hₖ(∐ⱼ (Dⁿ, Sⁿ⁻¹)) ≅ Hₖ(Xⁿ, Xⁿ⁻¹) on relative singular homology, in every degree k.

noncomputable def TauCeti.cellularChainGroupIsoSigmaDiskPair {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : cellularChainGroup C R n ≅ (sigmaDiskPair (Topology.RelCWComplex.cell C n) n).singularHomology R n

The cellular chain group Hₙ(Xⁿ, Xⁿ⁻¹) is the relative singular homology of the disjoint union ∐ⱼ (Dⁿ, Sⁿ⁻¹) of one disk pair for each n-cell; the inverse is induced by the characteristic maps TauCeti.characteristicPairMap C n.

Equations

• TauCeti.cellularChainGroupIsoSigmaDiskPair C R n = (CategoryTheory.asIso (TopPair.singularHomologyMap (TauCeti.characteristicPairMap C n) R n)).symm

@[simp]

theorem TauCeti.cellularChainGroupIsoSigmaDiskPair_inv {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : (cellularChainGroupIsoSigmaDiskPair C R n).inv = TopPair.singularHomologyMap (characteristicPairMap C n) R n