def AlgebraicTopologyI.standardSimplex (n : ℕ) : Set (Fin (n + 1) → ℝ)

Definition 1.1. The standard $n$-simplex $\Delta^n \subseteq \mathbb{R}^{n+1}$, realised as the convex hull of the standard basis vectors: the set of points $(t_0, \ldots, t_n)$ with $t_i \ge 0$ and $\sum t_i = 1$.

def AlgebraicTopologyI.SingularSimplex (n : ℕ) (X : Type u_1) [TopologicalSpace X] : Type u_1

Definition 1.2. A singular $n$-simplex in a topological space $X$: a continuous map $\sigma : \Delta^n \to X$.

def AlgebraicTopologyI.SingularChains (n : ℕ) (X : Type u_1) [TopologicalSpace X] : Type u_1

Definition 1.3. The group of singular $n$-chains on $X$: the free abelian group $S_n(X) = \mathbb{Z}\langle \mathrm{SingularSimplex}_n(X) \rangle$ generated by all singular $n$-simplices in $X$.

@[implicit_reducible]

instance AlgebraicTopologyI.instAddCommGroupSingularChains (n : ℕ) (X : Type u_1) [TopologicalSpace X] : AddCommGroup (SingularChains n X)

The abelian group structure on $S_n(X)$, inherited from the free abelian group construction.

def AlgebraicTopologyI.SingularChainsZ (n : ℤ) (X : Type u_1) [TopologicalSpace X] : Type u_1

The integer-graded variant of singular chains: equals $S_n(X)$ for $n \ge 0$ and is trivial for $n < 0$. Convenient for stating chain-complex axioms uniformly.

theorem AlgebraicTopologyI.singularChainsZ_neg {n : ℤ} (hn : n < 0) (X : Type u_1) [TopologicalSpace X] : SingularChainsZ n X = PUnit.{u_1 + 1}

In negative degrees, SingularChainsZ reduces to PUnit.

def AlgebraicTopologyI.IsCycle {A : Type u_1} {B : Type u_2} [AddCommGroup A] [AddCommGroup B] (d : A →+ B) (c : A) : Prop

A chain $c \in A$ is a cycle with respect to a boundary map $d : A \to B$ if $d(c) = 0$.

def AlgebraicTopologyI.Cycles {A : Type u_1} {B : Type u_2} [AddCommGroup A] [AddCommGroup B] (d : A →+ B) : AddSubgroup A

The subgroup of cycles for a boundary map $d : A \to B$: the kernel of $d$.

def AlgebraicTopologyI.SingularCycles (n : ℕ) (X : Type u_1) [TopologicalSpace X] (d : SingularChains (n + 1) X →+ SingularChains n X) : AddSubgroup (SingularChains (n + 1) X)

The singular $n$-cycles of $X$ with respect to a given boundary map $d$: $Z_{n+1}(X) = \ker (d : S_{n+1}(X) \to S_n(X))$.

@[reducible, inline]

abbrev AlgebraicTopologyI.ChainComplexOfAbelianGroups : Type (u_1 + 1)

An integer-graded chain complex of abelian groups.

noncomputable def AlgebraicTopologyI.singularChainComplexZ (X : TopCat) : ChainComplex AddCommGrpCat ℕ

Definition 1.4. The singular chain complex $S_*(X; \mathbb{Z})$ of a topological space $X$ with integer coefficients, as a chain complex of abelian groups indexed by $\mathbb{N}$ with the differential $\partial$ assembled from face maps.

theorem AlgebraicTopologyI.singular_d_comp_d (X : TopCat) (i j k : ℕ) : CategoryTheory.CategoryStruct.comp ((singularChainComplexZ X).d i j) ((singularChainComplexZ X).d j k) = 0

Theorem 1.5 ($\partial^2 = 0$). Consecutive differentials in the singular chain complex compose to zero: $\partial \circ \partial = 0$.

noncomputable def AlgebraicTopologyI.SingularHomologyGroup (n : ℕ) (X : Type) [TopologicalSpace X] : AddCommGrpCat

Definition 1.7. The $n$-th singular homology group with integer coefficients, $H_n(X; \mathbb{Z}) = Z_n(X) / B_n(X)$, packaged as an abelian group.

theorem AlgebraicTopologyI.singularHomologyGroup_eq_homology (n : ℕ) (X : Type) [TopologicalSpace X] : SingularHomologyGroup n X = HomologicalComplex.homology (singularChainComplexZ (TopCat.of X)) n

Identification of SingularHomologyGroup n X with the categorical homology $H_n(S_*(X; \mathbb{Z}))$ of the singular chain complex.