The cellular boundary on a cell generator

The boundary of an (n + 1)-cell is the image of the fundamental class of its boundary sphere under the attaching map, followed by the quotient to Hₙ(Xⁿ, Xⁿ⁻¹). The theorem TauCeti.ι_cellularChainGroupIso_inv_comp_cellularDifferential expresses this formula using the coproduct identification of cellular chains. Thus computing the differential reduces to computing the maps induced by the attaching spheres, rather than choosing singular chains representing each cell.

The attaching maps here are restrictions of the characteristic maps, read on Euclidean disks through the same radial rescaling as the cellular generators. The sphere class uses reduced homology: for a one-cell its boundary is the difference of the two endpoints, not their sum. Coefficients are objects in an abelian category with coproducts; only the coproduct indexed by the source cells needs to be exact.

The mathematical source is Hatcher, Algebraic Topology, Section 2.2, the cellular boundary formula. This file proves its factorization through the attaching map; no identification of individual matrix entries with integer degrees is asserted here.

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

The characteristic map of one cell, as a map from the Euclidean disk pair to the pair of consecutive skeleta. The disk coordinates are rescaled to the sup-norm coordinates of the classical CW structure.

Equations

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

@[simp]

theorem TauCeti.coe_characteristicCellPairMap_fst_apply {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {n : ℕ} (j : Topology.RelCWComplex.cell C n) (x : ↑(TopCat.disk n)) : ↑((CategoryTheory.ConcreteCategory.hom (TopPair.Hom.fst (characteristicCellPairMap C j))) x) = ↑(Topology.RelCWComplex.map n j) ((EuclideanSpace.equiv (Fin n) ℝ).unitBallHomeomorph ↑x.down)

The ambient component of the single-cell pair map is the characteristic map in rescaled Euclidean coordinates.

noncomputable def TauCeti.cellAttachingMap {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {n : ℕ} (j : Topology.RelCWComplex.cell C n) : TopCat.diskBoundary n ⟶ skeletonObj C n

The attaching map of a cell into the preceding skeleton, obtained by restricting its Euclidean characteristic map to the boundary sphere.

Equations

• TauCeti.cellAttachingMap C j = TopPair.Hom.snd (TauCeti.characteristicCellPairMap C j)

theorem TauCeti.cellAttachingMap_comp_inclusion {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {n : ℕ} (j : Topology.RelCWComplex.cell C n) : CategoryTheory.CategoryStruct.comp (cellAttachingMap C j) TopPair.map = CategoryTheory.CategoryStruct.comp (TopCat.diskBoundaryInclusion n) (TopPair.Hom.fst (characteristicCellPairMap C j))

The attaching map followed by skeletal inclusion is the characteristic map restricted to the disk boundary.

theorem TauCeti.cellAttachingMap_comp_inclusion_assoc {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {n : ℕ} (j : Topology.RelCWComplex.cell C n) {Z : TopCat} (h : TopPair.fst ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (cellAttachingMap C j) TopPair.map) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (TopCat.diskBoundaryInclusion n) (TopPair.Hom.fst (characteristicCellPairMap C j))) h

The attaching map followed by skeletal inclusion is the characteristic map restricted to the disk boundary.

@[simp]

theorem TauCeti.coe_cellAttachingMap_apply {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {n : ℕ} (j : Topology.RelCWComplex.cell C n) (x : ↑(TopCat.diskBoundary n)) : ↑((CategoryTheory.ConcreteCategory.hom (cellAttachingMap C j)) x) = ↑(Topology.RelCWComplex.map n j) ((EuclideanSpace.equiv (Fin n) ℝ).unitBallHomeomorph ↑x.down)

The attaching map is the boundary restriction of the characteristic map in rescaled Euclidean coordinates.

theorem TauCeti.ι_cellularChainGroupIso_inv_comp_cellularDifferential {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 + 1))) A] (j : Topology.RelCWComplex.cell C (n + 1)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : Topology.RelCWComplex.cell C (n + 1)) => R) j) (CategoryTheory.CategoryStruct.comp (cellularChainGroupIso C R (n + 1)).inv (cellularDifferential C R n)) = CategoryTheory.CategoryStruct.comp (reducedSingularHomologyTopCatSphereIso R n).inv (CategoryTheory.CategoryStruct.comp ((reducedSingularHomologyι R n).app (TopCat.diskBoundary (n + 1))) (CategoryTheory.CategoryStruct.comp (SSet.homologyMap (TopCat.toSSet.map (cellAttachingMap C j)) R n) (skeletonPairπ C R n)))

The cellular boundary on a cell generator: take the reduced fundamental class of the boundary sphere, include it in ordinary homology, apply the attaching map, and pass to the relative homology of consecutive skeleta. This includes one-cells, whose reduced boundary class gives the signed difference of their endpoints.

theorem TauCeti.ι_cellularChainGroupIso_inv_comp_cellularDifferential_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 + 1))) A] (j : Topology.RelCWComplex.cell C (n + 1)) {Z : A} (h : cellularChainGroup C R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : Topology.RelCWComplex.cell C (n + 1)) => R) j) (CategoryTheory.CategoryStruct.comp (cellularChainGroupIso C R (n + 1)).inv (CategoryTheory.CategoryStruct.comp (cellularDifferential C R n) h)) = CategoryTheory.CategoryStruct.comp (reducedSingularHomologyTopCatSphereIso R n).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((reducedSingularHomologyι R n).app (TopCat.diskBoundary (n + 1))) (CategoryTheory.CategoryStruct.comp (SSet.homologyMap (TopCat.toSSet.map (cellAttachingMap C j)) R n) (skeletonPairπ C R n))) h)

The cellular boundary on a cell generator: take the reduced fundamental class of the boundary sphere, include it in ordinary homology, apply the attaching map, and pass to the relative homology of consecutive skeleta. This includes one-cells, whose reduced boundary class gives the signed difference of their endpoints.