The CW structure on a sphere

The unit sphere Sⁿ of a Euclidean space EuclideanSpace ℝ ι of dimension n + 1 is a finite CW complex with one 0-cell, a pole, and one n-cell attached along the constant map to it (TauCeti.sphereCWComplex). The characteristic map of the n-cell collapses the boundary of the closed unit cube closedBall (0 : Fin n → ℝ) 1 to ∞ (TauCeti.unitBallToOnePoint) and then identifies the one-point compactification of Fin n → ℝ with Sⁿ (onePointEquivSphereOfFinrankEq); the pole is the image of ∞. For n = 0 the two cells are the two points of S⁰.

• TauCeti.spherePole h: the 0-cell of Sⁿ, for h : Fintype.card ι = n + 1.
• TauCeti.sphereTopCellMap h: the characteristic map of the n-cell, a bijection from the open unit cube onto the complement of the pole.
• TauCeti.sphereCWComplex h: the CW structure, which is finite (TauCeti.finite_sphereCWComplex) with one cell in dimension 0 and one in dimension n (TauCeti.nat_card_cell_sphereCWComplex); for 1 ≤ k ≤ n, skeletonLT k (the (k - 1)-skeleton) is the pole (TauCeti.skeletonLT_sphereCWComplex).
• TauCeti.finiteCWType_sphere: the unit sphere of every finite-dimensional real normed space has finite CW type.
• TauCeti.finiteCWType_onePoint: so has the one-point compactification of every finite-dimensional real vector space, for instance the Riemann sphere OnePoint ℂ.

References

• A. Hatcher, Algebraic Topology, Chapter 0, Example 0.3.

noncomputable def TauCeti.spherePole {ι : Type u} [Fintype ι] {n : ℕ} (h : Fintype.card ι = n + 1) : EuclideanSpace ℝ ι

The pole of the unit sphere Sⁿ of EuclideanSpace ℝ ι, for ι of cardinality n + 1: the 0-cell of its CW structure, onto which the boundary of the n-cell is collapsed.

theorem TauCeti.spherePole_mem_sphere {ι : Type u} [Fintype ι] {n : ℕ} (h : Fintype.card ι = n + 1) : spherePole h ∈ Metric.sphere 0 1

noncomputable def TauCeti.sphereTopCellMap {ι : Type u} [Fintype ι] {n : ℕ} (h : Fintype.card ι = n + 1) : PartialEquiv (Fin n → ℝ) (EuclideanSpace ℝ ι)

The characteristic map of the top cell of the unit sphere Sⁿ of EuclideanSpace ℝ ι, for ι of cardinality n + 1: it maps the open unit cube of Fin n → ℝ bijectively onto the complement of TauCeti.spherePole h and collapses the boundary of the cube to the pole.

@[simp]

theorem TauCeti.sphereTopCellMap_source {ι : Type u} [Fintype ι] {n : ℕ} (h : Fintype.card ι = n + 1) : (sphereTopCellMap h).source = Metric.ball 0 1

@[simp]

theorem TauCeti.sphereTopCellMap_target {ι : Type u} [Fintype ι] {n : ℕ} (h : Fintype.card ι = n + 1) : (sphereTopCellMap h).target = Metric.sphere 0 1 \ {spherePole h}

theorem TauCeti.sphereTopCellMap_apply {ι : Type u} [Fintype ι] {n : ℕ} (h : Fintype.card ι = n + 1) (x : Fin n → ℝ) : ↑(sphereTopCellMap h) x = ↑((onePointEquivSphereOfFinrankEq ⋯) (↑unitBallToOnePoint x))

The characteristic map of the top cell of Sⁿ is the boundary collapse TauCeti.unitBallToOnePoint followed by onePointEquivSphereOfFinrankEq.

theorem TauCeti.sphereTopCellMap_symm_apply {ι : Type u} [Fintype ι] {n : ℕ} (h : Fintype.card ι = n + 1) {y : EuclideanSpace ℝ ι} (hy : y ∈ Metric.sphere 0 1) : ↑(sphereTopCellMap h).symm y = ↑unitBallToOnePoint.symm ((onePointEquivSphereOfFinrankEq ⋯).symm ⟨y, hy⟩)

On Sⁿ, the inverse of the characteristic map of the top cell is the inverse of onePointEquivSphereOfFinrankEq followed by the inverse of TauCeti.unitBallToOnePoint.

theorem TauCeti.sphereTopCellMap_mem_sphere {ι : Type u} [Fintype ι] {n : ℕ} (h : Fintype.card ι = n + 1) (x : Fin n → ℝ) : ↑(sphereTopCellMap h) x ∈ Metric.sphere 0 1

@[simp]

theorem TauCeti.sphereTopCellMap_apply_of_norm_eq_one {ι : Type u} [Fintype ι] {n : ℕ} (h : Fintype.card ι = n + 1) {x : Fin n → ℝ} (hx : ‖x‖ = 1) : ↑(sphereTopCellMap h) x = spherePole h

The characteristic map of the top cell collapses the boundary of the cube to the pole.

theorem TauCeti.continuousOn_sphereTopCellMap {ι : Type u} [Fintype ι] {n : ℕ} (h : Fintype.card ι = n + 1) : ContinuousOn (↑(sphereTopCellMap h)) (Metric.closedBall 0 1)

The characteristic map of the top cell of Sⁿ is continuous on the closed unit ball, as a CW characteristic map must be.

theorem TauCeti.continuousOn_sphereTopCellMap_symm {ι : Type u} [Fintype ι] {n : ℕ} (h : Fintype.card ι = n + 1) : ContinuousOn (↑(sphereTopCellMap h).symm) (sphereTopCellMap h).target

The inverse of the characteristic map of the top cell of Sⁿ is continuous on the open cell Sⁿ \ {pole}.

@[instance_reducible]

noncomputable def TauCeti.sphereCWComplex {ι : Type u} [Fintype ι] {n : ℕ} (h : Fintype.card ι = n + 1) : Topology.CWComplex (Metric.sphere 0 1)

The CW structure on the unit sphere Sⁿ of EuclideanSpace ℝ ι, for ι of cardinality n + 1: one 0-cell, the pole TauCeti.spherePole h, and one n-cell with characteristic map TauCeti.sphereTopCellMap h.

theorem TauCeti.finite_sphereCWComplex {ι : Type u} [Fintype ι] {n : ℕ} (h : Fintype.card ι = n + 1) : Topology.RelCWComplex.Finite (Metric.sphere 0 1)

The CW structure on Sⁿ is finite.

theorem TauCeti.nat_card_cell_sphereCWComplex {ι : Type u} [Fintype ι] {n : ℕ} (h : Fintype.card ι = n + 1) (m : ℕ) : Nat.card (Topology.RelCWComplex.cell (Metric.sphere 0 1) m) = (if m = 0 then 1 else 0) + if m = n then 1 else 0

The CW structure on Sⁿ has one cell in dimension 0 and one in dimension n (two 0-cells when n = 0).

theorem TauCeti.isEmpty_cell_sphereCWComplex {ι : Type u} [Fintype ι] {n : ℕ} (h : Fintype.card ι = n + 1) {m : ℕ} (hm : n + 1 ≤ m) : IsEmpty (Topology.RelCWComplex.cell (Metric.sphere 0 1) m)

The CW structure on Sⁿ has no cells of dimension greater than n.

theorem TauCeti.skeletonLT_sphereCWComplex {ι : Type u} [Fintype ι] {n : ℕ} (h : Fintype.card ι = n + 1) {k : ℕ∞} (hk : 1 ≤ k) (hkn : k ≤ ↑n) : ↑(Topology.RelCWComplex.skeletonLT (Metric.sphere 0 1) k) = {spherePole h}

For 1 ≤ k ≤ n, skeletonLT k of the CW structure on Sⁿ, the (k - 1)-skeleton (the union of the cells of dimension less than k), is the pole.

instance TauCeti.finiteCWType_sphere {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] : FiniteCWType ↑(Metric.sphere 0 1)

The unit sphere of a finite-dimensional real normed space has finite CW type: it is homeomorphic to the unit sphere of EuclideanSpace ℝ (ULift (Fin (n + 1))) for n + 1 the dimension, or empty in dimension zero.

instance TauCeti.finiteCWType_onePoint {V : Type u} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul ℝ V] [T2Space V] : FiniteCWType (OnePoint V)

The one-point compactification of a finite-dimensional real vector space V has finite CW type: it is homeomorphic to the unit sphere of dimension dim V. In particular the Riemann sphere OnePoint ℂ has finite CW type.