theorem AlgebraicTopologyI.SingularChains.map_id {n : ℕ} {X : Type} [TopologicalSpace X] (c : SingularChains n X) : (map (ContinuousMap.id X)) c = c

The chain-level map induced by the identity continuous map is the identity.

theorem AlgebraicTopologyI.singularSimplex_punit_eq (n : ℕ) (σ τ : SingularSimplex n PUnit.{u_1 + 1}) : σ = τ

Any two singular n-simplices of PUnit are equal, since PUnit is a subsingleton.

theorem AlgebraicTopologyI.singularChains_punit_eq_smul (n : ℕ) (σ₀ : SingularSimplex n PUnit.{u_1 + 1}) (c : SingularChains n PUnit.{u_1 + 1}) : ∃ (m : ℤ), c = m • FreeAbelianGroup.of σ₀

Any singular n-chain on PUnit is an integer multiple of the unique generator FreeAbelianGroup.of σ₀.

theorem AlgebraicTopologyI.FreeAbelianGroup.smul_of_eq_zero {T : Type u_1} (a : T) (m : ℤ) (h : m • FreeAbelianGroup.of a = 0) : m = 0

If m • FreeAbelianGroup.of a = 0 in a free abelian group, then the scalar m is zero.

theorem AlgebraicTopologyI.alternating_sum_range (N : ℕ) : ∑ i ∈ Finset.range N, (-1) ^ i = if Odd N then 1 else 0

The alternating sum ∑_{i < N} (-1)^i equals 1 if N is odd and 0 otherwise.

theorem AlgebraicTopologyI.alternating_sum_fin (n : ℕ) : ∑ i : Fin (n + 2), (-1) ^ ↑i = if Odd n then 1 else 0

The alternating sum ∑_{i : Fin (n+2)} (-1)^i equals 1 if n is odd and 0 otherwise — this captures the value of the boundary map on a chain of constant simplices on PUnit.

theorem AlgebraicTopologyI.boundaryMap_punit_generator (n : ℕ) (σ : SingularSimplex (n + 1) PUnit.{u_1 + 1}) (σ₀ : SingularSimplex n PUnit.{u_1 + 1}) : (boundaryMap n PUnit.{u_1 + 1}) (FreeAbelianGroup.of σ) = (∑ i : Fin (n + 2), (-1) ^ ↑i) • FreeAbelianGroup.of σ₀

The boundary of the singular simplex FreeAbelianGroup.of σ on PUnit equals the alternating sum of signs times the unique n-simplex generator σ₀.

theorem AlgebraicTopologyI.punit_acyclic (n : ℕ) (c : SingularChains (n + 1) PUnit.{u_1 + 1}) (hc : (boundaryMap n PUnit.{u_1 + 1}) c = 0) : ∃ (d : SingularChains (n + 2) PUnit.{u_1 + 1}), (boundaryMap (n + 1) PUnit.{u_1 + 1}) d = c

Acyclicity of the singular chain complex of PUnit in positive degrees: every (n+1)-cycle on PUnit is the boundary of some (n+2)-chain. This is the cone-style acyclicity input feeding into the chain-homotopy machinery for star-shaped regions (Proposition 5.13).