@[reducible, inline]

abbrev CWSubcomplex (X : Type u_1) [TopologicalSpace X] [Topology.CWComplex Set.univ] : Type u_1

Definition 15.1. A subcomplex of a CW-complex $X$ is a closed subspace $Y \subseteq X$ that inherits a CW-structure from $X$: for each $n$ there is a subset $B_n$ of the $n$-cells $A_n$ such that $Y_n = Y \cap X_n$ is given a CW-structure by the characteristic maps $\{g_\beta : \beta \in B_n\}$.

In this formalization a CWSubcomplex X is unfolded to Mathlib's Topology.CWComplex.Subcomplex (Set.univ : Set X).

@[reducible, inline]

abbrev CWSubcomplex.cells {X : Type u_1} [TopologicalSpace X] [Topology.CWComplex Set.univ] (E : CWSubcomplex X) (n : ℕ) : Set (CWComplex.cells X n)

The indexing set of $n$-cells of the subcomplex E, viewed as a subset of the indexing set of $n$-cells of the ambient CW-complex X.

theorem CWSubcomplex.isClosed {X : Type u_1} [TopologicalSpace X] [Topology.CWComplex Set.univ] (E : CWSubcomplex X) : IsClosed ↑E

A subcomplex of a CW-complex is a closed subspace.

theorem CWSubcomplex.subset_univ {X : Type u_1} [TopologicalSpace X] [Topology.CWComplex Set.univ] (E : CWSubcomplex X) : ↑E ⊆ Set.univ

A subcomplex sits inside the ambient space; trivial inclusion into Set.univ.

def CWSubcomplex.IsFinite {X : Type u_1} [TopologicalSpace X] [Topology.CWComplex Set.univ] [T2Space X] (E : CWSubcomplex X) : Prop

A subcomplex E is finite if, with its induced CW-structure, it has only finitely many cells in total.

theorem CWSubcomplex.compact_subset_finite_subcomplex {X : Type u_1} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (S : Set X) (hS : IsCompact S) : ∃ (E : CWSubcomplex X), E.IsFinite ∧ S ⊆ ↑E

Proposition 15.3. Let $X$ be a CW-complex with a chosen cell structure. Any compact subspace $S \subseteq X$ lies in some finite subcomplex of $X$.

@[reducible, inline]

abbrev SphereInfty.l2 : Type

The Hilbert space $\ell^2(\mathbb{N}, \mathbb{R})$ of square-summable sequences of real numbers. This serves as the ambient space for the model of $\mathbb{R}^{\infty}$ and $S^{\infty}$ used below.

def SphereInfty.RInfty : Set l2

The subspace $\mathbb{R}^{\infty} \subseteq \ell^2$ consisting of sequences with finite support, i.e. those that are nonzero in only finitely many coordinates. This is the increasing union of all $\mathbb{R}^n$.

@[reducible, inline]

abbrev SphereInfty.Sphere : Type

The infinite sphere $S^{\infty} = \mathbb{R}^{\infty} \cap S(\ell^2, 1)$: unit vectors in $\ell^2$ with finite support. Proposition 15.5 asserts this space is contractible.

theorem SphereInfty.RInfty.add_mem {x y : l2} (hx : x ∈ RInfty) (hy : y ∈ RInfty) : x + y ∈ RInfty

The sum of two finitely supported sequences in $\ell^2$ is again finitely supported; closure of $\mathbb{R}^{\infty}$ under addition.

theorem SphereInfty.RInfty.smul_mem (c : ℝ) {x : l2} (hx : x ∈ RInfty) : c • x ∈ RInfty

Scaling a finitely supported sequence by a scalar preserves finite support; closure of $\mathbb{R}^{\infty}$ under scalar multiplication.

theorem SphereInfty.norm_eq_one (x : Sphere) : ‖↑x‖ = 1

Every point of $S^{\infty}$ has $\ell^2$-norm equal to $1$.

theorem SphereInfty.Sphere.mem_RInfty (x : Sphere) : ↑x ∈ RInfty

A point of $S^{\infty}$ has finite support, i.e. lies in $\mathbb{R}^{\infty}$.

def SphereInfty.shiftRight (x : ℕ → ℝ) : ℕ → ℝ

The shift operator on sequences sending $(x_0, x_1, x_2, \ldots)$ to $(0, x_0, x_1, \ldots)$. Used to build a sequence-level model of the operator $T : \ell^2 \to \ell^2$ that underlies the contraction of $S^{\infty}$.

theorem SphereInfty.finite_support_shiftRight {x : ℕ → ℝ} (hx : (Function.support x).Finite) : (Function.support (shiftRight x)).Finite

shiftRight preserves finite support; used to show $T$ maps $\mathbb{R}^{\infty}$ into itself.

theorem SphereInfty.memℓp_shiftRight {x : ℕ → ℝ} (hx : Memℓp x 2) : Memℓp (shiftRight x) 2

shiftRight preserves membership in $\ell^2$, since shifting does not change the multiset of nonzero values.

def SphereInfty.T (x : l2) : l2

The right-shift operator $T : \ell^2 \to \ell^2$, sending $(x_0, x_1, \ldots)$ to $(0, x_0, x_1, \ldots)$. It is a linear isometry of $\ell^2$ which is not surjective; this defect drives the contraction of $S^{\infty}$.

theorem SphereInfty.T_norm (x : l2) : ‖T x‖ = ‖x‖

The shift operator $T$ preserves $\ell^2$-norm: $\|T x\| = \|x\|$.

theorem SphereInfty.T_sub (x y : l2) : T x - T y = T (x - y)

The shift operator $T$ is additive on subtractions: $T x - T y = T(x - y)$.

theorem SphereInfty.T_isometry : Isometry T

The shift operator $T : \ell^2 \to \ell^2$ is an isometry, combining T_sub and T_norm.

theorem SphereInfty.continuous_T : Continuous T

Continuity of the shift operator $T$, an immediate consequence of being an isometry.

theorem SphereInfty.T_mem_RInfty {x : l2} (hx : x ∈ RInfty) : T x ∈ RInfty

T preserves $\mathbb{R}^{\infty}$: the shift of a finitely supported sequence is finitely supported.

theorem SphereInfty.T_mem_sphere_set (x : Sphere) : T ↑x ∈ RInfty ∩ Metric.sphere 0 1

The shift $T$ maps $S^{\infty}$ to itself: it preserves both finite support and unit norm.

def SphereInfty.TOnSphere : C(Sphere, Sphere)

The shift operator $T$ restricted to a continuous self-map of $S^{\infty}$.

theorem SphereInfty.shiftRight_affine_zero_imp {x : ℕ → ℝ} {t : ℝ} (ht : 0 < t) (h : ∀ (n : ℕ), t * x n + (1 - t) * shiftRight x n = 0) (n : ℕ) : x n = 0

Coordinate-level key lemma: if $t > 0$ and the affine combination $t \cdot x + (1 - t) \cdot \text{shiftRight}(x)$ vanishes identically, then $x = 0$. Used to prove that the affine homotopy from $\text{id}$ to $T$ never passes through $0$.

theorem SphereInfty.norm_affine_id_T_pos (x : l2) (hx : ‖x‖ = 1) (t : ℝ) (ht0 : 0 ≤ t) : t ≤ 1 → 0 < ‖t • x + (1 - t) • T x‖

For a unit vector $x$ and any $t \in [0, 1]$, the affine combination $t \cdot x + (1 - t) \cdot T x$ is nonzero. This ensures the straight-line homotopy from $T$ to the identity is well-defined after normalization.

def SphereInfty.e1 : l2

The standard first basis vector $e_1 = (1, 0, 0, \ldots) \in \ell^2$. This will be the basepoint to which all of $S^{\infty}$ is contracted.

theorem SphereInfty.e1_norm : ‖e1‖ = 1

The basis vector $e_1$ has unit norm.

theorem SphereInfty.e1_mem_RInfty : e1 ∈ RInfty

The basis vector $e_1$ has finite support, so lies in $\mathbb{R}^{\infty}$.

theorem SphereInfty.e1_mem_sphere_set : e1 ∈ RInfty ∩ Metric.sphere 0 1

The basis vector $e_1$ lies in $S^{\infty}$, since it has unit norm and finite support.

theorem SphereInfty.norm_affine_T_e1_pos (x : l2) (hx : ‖x‖ = 1) (t : ℝ) : 0 ≤ t → ∀ (ht1 : t ≤ 1), 0 < ‖t • T x + (1 - t) • e1‖

For a unit vector $x$ and any $t \in [0, 1]$, the affine combination $t \cdot T x + (1 - t) \cdot e_1$ is nonzero. This ensures the straight-line homotopy from the constant map $e_1$ to $T$ is well-defined after normalization.

theorem SphereInfty.continuous_normalize_comp {α : Type u_1} [TopologicalSpace α] (v : α → l2) (hv_cont : Continuous v) (hv_ne : ∀ (x : α), v x ≠ 0) : Continuous fun (x : α) => ‖v x‖⁻¹ • v x

A continuous family of nonzero vectors can be continuously normalized to unit vectors.

theorem SphereInfty.norm_normalize (v : l2) (hv : v ≠ 0) : ‖v‖⁻¹ • v ∈ Metric.sphere 0 1

Normalizing a nonzero vector yields a unit vector, i.e. a point on the unit sphere in $\ell^2$.

noncomputable def SphereInfty.normalizeToSphere (v : l2) (hv : v ≠ 0) (hR : v ∈ RInfty) : Sphere

Given a nonzero finitely supported vector $v \in \mathbb{R}^{\infty}$, its normalization $v / \|v\|$ as a point of $S^{\infty}$.

noncomputable def SphereInfty.v_id_T (p : ↑unitInterval × Sphere) : l2

The straight-line family in $\ell^2$ joining $T x$ to $x$: at time $t$, the vector $t \cdot x + (1 - t) \cdot T x$. After normalization this gives the homotopy from $T$ (at $t = 0$) to the identity (at $t = 1$) on $S^{\infty}$.

theorem SphereInfty.v_id_T_mem_RInfty (p : ↑unitInterval × Sphere) : v_id_T p ∈ RInfty

The affine combination v_id_T p is finitely supported, since both $x$ and $T x$ are.

theorem SphereInfty.continuous_v_id_T : Continuous v_id_T

The straight-line family v_id_T depends continuously on $(t, x)$.

theorem SphereInfty.v_id_T_ne_zero (p : ↑unitInterval × Sphere) : v_id_T p ≠ 0

The straight-line family v_id_T never vanishes, so normalization is well-defined throughout.

noncomputable def SphereInfty.v_T_e1 (p : ↑unitInterval × Sphere) : l2

The straight-line family in $\ell^2$ joining $e_1$ to $T x$: at time $t$, the vector $t \cdot T x + (1 - t) \cdot e_1$. After normalization this gives the homotopy from the constant map $e_1$ (at $t = 0$) to $T$ (at $t = 1$) on $S^{\infty}$.

theorem SphereInfty.v_T_e1_mem_RInfty (p : ↑unitInterval × Sphere) : v_T_e1 p ∈ RInfty

The straight-line family v_T_e1 is finitely supported.

theorem SphereInfty.continuous_v_T_e1 : Continuous v_T_e1

The straight-line family v_T_e1 depends continuously on $(t, x)$.

theorem SphereInfty.v_T_e1_ne_zero (p : ↑unitInterval × Sphere) : v_T_e1 p ≠ 0

The straight-line family v_T_e1 never vanishes.

noncomputable def SphereInfty.constE1 : C(Sphere, Sphere)

The constant continuous map from $S^{\infty}$ to itself sending every point to the basepoint $e_1$.

noncomputable def SphereInfty.homotopy_T_to_id : TOnSphere.Homotopy (ContinuousMap.id Sphere)

A homotopy on $S^{\infty}$ from the shift map $T$ to the identity, obtained by normalizing the straight-line family v_id_T.

noncomputable def SphereInfty.homotopy_e1_to_T : constE1.Homotopy TOnSphere

A homotopy on $S^{\infty}$ from the constant map at $e_1$ to the shift map $T$, obtained by normalizing the straight-line family v_T_e1.

instance SphereInfty.contractibleSpace : ContractibleSpace Sphere

Proposition 15.5. $S^{\infty}$ is contractible.

Proof: We compose the two homotopies $\text{const}_{e_1} \simeq T$ and $T \simeq \text{id}$ to obtain $\text{const}_{e_1} \simeq \text{id}$, showing the identity on $S^{\infty}$ is nullhomotopic.