Characteristic and attaching maps of a cell on the Euclidean disk

The characteristic map of an n-cell of a relative CW complex C is defined on the closed unit ball of the sup norm on Fin n → ℝ. Read on the Euclidean disk 𝔻 n of TopCat through the radial homeomorphism TauCeti.diskHomeomorphClosedBall, it is a morphism TauCeti.cellDiskHom to the skeleton skeletonLT C (n + 1), and its restriction to the boundary sphere ∂𝔻 n is the attaching map TauCeti.cellAttachingMap to skeletonLT C n.

The mathematical source is Hatcher, Algebraic Topology, Section 2.2 and Appendix.

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

The characteristic map of an n-cell, read on the Euclidean disk 𝔻 n through TauCeti.diskHomeomorphClosedBall, as a morphism to the n-skeleton skeletonLT C (n + 1).

theorem TauCeti.coe_cellDiskHom_apply {X : Type w} [TopologicalSpace X] [T2Space X] {D C : Set X} [Topology.RelCWComplex C D] {n : ℕ} (j : Topology.RelCWComplex.cell C n) (z : ↑(TopCat.disk n)) : ↑((CategoryTheory.ConcreteCategory.hom (cellDiskHom j)) z) = ↑(Topology.RelCWComplex.map n j) ↑((diskHomeomorphClosedBall n) z)

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

The attaching map of an n-cell: its characteristic map restricted to the boundary sphere ∂𝔻 n, as a morphism to skeletonLT C n.

theorem TauCeti.coe_cellAttachingMap_apply {X : Type w} [TopologicalSpace X] [T2Space X] {D C : Set X} [Topology.RelCWComplex C D] {n : ℕ} (j : Topology.RelCWComplex.cell C n) (z : ↑(TopCat.diskBoundary n)) : ↑((CategoryTheory.ConcreteCategory.hom (cellAttachingMap j)) z) = ↑(Topology.RelCWComplex.map n j) ↑((diskHomeomorphClosedBall n) ((CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion n)) z))

@[simp]

theorem TauCeti.range_cellAttachingMap {X : Type w} [TopologicalSpace X] [T2Space X] {D C : Set X} [Topology.RelCWComplex C D] {n : ℕ} (j : Topology.RelCWComplex.cell C n) : (Set.range fun (z : ↑(TopCat.diskBoundary n)) => ↑((CategoryTheory.ConcreteCategory.hom (cellAttachingMap j)) z)) = Topology.RelCWComplex.cellFrontier n j

The attaching map of a cell maps the boundary sphere onto the frontier of the cell.