The cellular chain group is a coproduct of copies of the coefficients, one per cell

For a relative CW complex and coefficients R in an abelian category in which coproducts indexed by the n-cells are exact (for instance modules over a ring), the cellular chain group Hₙ(Xⁿ, Xⁿ⁻¹) is the coproduct of one copy of R for each n-cell (TauCeti.cellularChainGroupIso). For modules over a ring k, this is the direct sum of copies of the coefficient module R, one per n-cell; when R = k, it is the free k-module on the n-cells.

The identification is induced by maps: the summand of the cell j is the image of the relative homology Hₙ(Dⁿ, Sⁿ⁻¹) ≅ R of the Euclidean disk pair under the characteristic map of j (TauCeti.ι_cellularChainGroupIso_inv). It combines three facts.

• The characteristic maps identify Hₙ(Xⁿ, Xⁿ⁻¹) with the relative homology of the disjoint union ∐ⱼ (Dⁿ, Sⁿ⁻¹) of closed unit balls of the sup norm on Fin n → ℝ relative to their boundary spheres (TauCeti.cellularChainGroupIsoSigmaDiskPair).
• That disjoint union is isomorphic, as a pair, to the disjoint union of copies of the Euclidean disk pair TauCeti.diskBoundaryPair n (TauCeti.sigmaDiskBoundaryPairIso), through the radial rescaling ContinuousLinearEquiv.unitBallHomeomorph of the coordinate identification of EuclideanSpace ℝ (Fin n) with Fin n → ℝ.
• Relative singular homology is additive (TopPair.isColimitCofanSingularHomology), and the Euclidean disk pair has Hₙ(Dⁿ, Sⁿ⁻¹) ≅ R (TauCeti.singularHomologyDiskBoundaryPairIso).

The same ingredients show that the relative homology of ∐ᵢ (Dⁿ, Sⁿ⁻¹) vanishes outside degree n (TauCeti.isZero_singularHomology_sigmaDiskPair_of_ne).

References

• A. Hatcher, Algebraic Topology, Section 2.2, Lemma 2.34.

noncomputable def TauCeti.sigmaDiskBoundaryPairIso (ι : Type w) (n : ℕ) : (TopPair.sigma fun (x : ι) => diskBoundaryPair n) ≅ sigmaDiskPair ι n

The disjoint union of copies, indexed by ι, of the Euclidean disk pair TauCeti.diskBoundaryPair n is isomorphic to TauCeti.sigmaDiskPair ι n, the disjoint union of closed unit balls of the sup norm on Fin n → ℝ relative to their unit spheres. On each summand the isomorphism is the radial rescaling ContinuousLinearEquiv.unitBallHomeomorph of the coordinate identification EuclideanSpace.equiv.

Equations

• TauCeti.sigmaDiskBoundaryPairIso ι n = CategoryTheory.asIso (TauCeti.sigmaDiskBoundaryPairHom✝ ι n)

@[simp]

theorem TauCeti.sigmaDiskBoundaryPairIso_hom_fst_apply_fst (ι : Type w) (n : ℕ) (p : ↑TopPair.fst) : ((CategoryTheory.ConcreteCategory.hom (TopPair.Hom.fst (sigmaDiskBoundaryPairIso ι n).hom)) p).fst = p.fst

On the ambient spaces, TauCeti.sigmaDiskBoundaryPairIso preserves the summand.

@[simp]

theorem TauCeti.coe_sigmaDiskBoundaryPairIso_hom_fst_apply_snd (ι : Type w) (n : ℕ) (p : ↑TopPair.fst) : ↑((CategoryTheory.ConcreteCategory.hom (TopPair.Hom.fst (sigmaDiskBoundaryPairIso ι n).hom)) p).snd = (EuclideanSpace.equiv (Fin n) ℝ).unitBallHomeomorph ↑p.snd.down

On the ambient spaces, TauCeti.sigmaDiskBoundaryPairIso is the radial rescaling of the coordinate identification EuclideanSpace.equiv in every summand.

theorem TauCeti.isZero_singularHomology_sigmaDiskPair_of_ne {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (ι : Type w) [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete ι) A] {n k : ℕ} (hk : k ≠ n) : CategoryTheory.Limits.IsZero ((sigmaDiskPair ι n).singularHomology R k)

The relative singular homology of the disjoint union ∐ᵢ (Dⁿ, Sⁿ⁻¹) of disk pairs vanishes outside degree n, when coproducts indexed by ι are exact.

noncomputable def TauCeti.cellularChainGroupIso {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 : ℕ) [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C n)) A] : cellularChainGroup C R n ≅ ∐ fun (x : Topology.RelCWComplex.cell C n) => R

The cellular chain group is a coproduct of copies of the coefficients: if coproducts indexed by the n-cells are exact in A, then Hₙ(Xⁿ, Xⁿ⁻¹) is the coproduct of one copy of R for each n-cell. The summand of a cell is the image of Hₙ(Dⁿ, Sⁿ⁻¹) ≅ R under its characteristic map (TauCeti.ι_cellularChainGroupIso_inv).

Equations

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

theorem TauCeti.ι_cellularChainGroupIso_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 : ℕ) [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C n)) A] (j : Topology.RelCWComplex.cell C n) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : Topology.RelCWComplex.cell C n) => R) j) (cellularChainGroupIso C R n).inv = CategoryTheory.CategoryStruct.comp (singularHomologyDiskBoundaryPairIso R n).inv (TopPair.singularHomologyMap (CategoryTheory.CategoryStruct.comp (TopPair.sigmaι (fun (x : Topology.RelCWComplex.cell C n) => diskBoundaryPair n) j) (CategoryTheory.CategoryStruct.comp (sigmaDiskBoundaryPairIso (Topology.RelCWComplex.cell C n) n).hom (characteristicPairMap C n))) R n)

The inverse of TauCeti.cellularChainGroupIso on the summand of the cell j is the inverse of Hₙ(Dⁿ, Sⁿ⁻¹) ≅ R followed by the map induced by the characteristic map of j, read on the Euclidean disk pair.

theorem TauCeti.ι_cellularChainGroupIso_inv_assoc {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 : ℕ) [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C n)) A] (j : Topology.RelCWComplex.cell C n) {Z : A} (h : cellularChainGroup C R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : Topology.RelCWComplex.cell C n) => R) j) (CategoryTheory.CategoryStruct.comp (cellularChainGroupIso C R n).inv h) = CategoryTheory.CategoryStruct.comp (singularHomologyDiskBoundaryPairIso R n).inv (CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (CategoryTheory.CategoryStruct.comp (TopPair.sigmaι (fun (x : Topology.RelCWComplex.cell C n) => diskBoundaryPair n) j) (CategoryTheory.CategoryStruct.comp (sigmaDiskBoundaryPairIso (Topology.RelCWComplex.cell C n) n).hom (characteristicPairMap C n))) R n) h)

The inverse of TauCeti.cellularChainGroupIso on the summand of the cell j is the inverse of Hₙ(Dⁿ, Sⁿ⁻¹) ≅ R followed by the map induced by the characteristic map of j, read on the Euclidean disk pair.