relSC_id_isZero
plain-language theorem explainer
The relative singular chain complex of the identity map on any space X is the zero complex: C_*(X,X) = 0. Algebraic topologists and anyone wiring relative homology into the Recognition foundation cite this as the base sanity check on the cokernel definition. The proof is a three-line tactic argument: the induced singular chain map is the identity, hence epic, and the cokernel of an epi vanishes.
Claim. For every topological space $X$, the relative singular chain complex of the identity map $\mathrm{id}_X$ is the zero object in the category of chain complexes of $\mathbb{Z}$-modules: $C_*(X,X) = 0$.
background
In this module, pairs of spaces are encoded by a continuous map $f : A \to X$. The singular chain complex $C_(X)$ is the usual complex of free $\mathbb{Z}$-modules on singular simplices. A continuous map induces a chain map $C_(A) \to C_*(X)$ via the singular-chain functor.
The relative complex $C_*(X,A)$ is defined as the cokernel of that induced chain map (degreewise the quotient $C_n(X)/C_n(A)$ with the induced differential). This is the standard algebraic model of relative singular chains, packaged so that short exact sequences of pairs and the long exact sequence of relative homology are available in Lean.
The identity event in ObserverForcing sits at the J-cost minimum $x=1$; here the topological identity plays the analogous neutral role. The lemma records that the relative complex of $\mathrm{id}_X$ collapses completely, which is the expected null case of the cokernel construction.
proof idea
Three short steps. First, functoriality of the singular-chain functor gives that the chain map induced by $\mathrm{id}X$ equals the identity chain map on $C*(X)$ (CategoryTheory.Functor.map_id). Second, the identity morphism is epic, so after rewriting one obtains Epi on the induced chain map. Third, apply the general fact that the cokernel of an epimorphism is the zero object (isZero_cokernel_of_epi). The relative complex is defined as that cokernel, so it is zero.
why it matters
This is the chain-level sanity lock for the cokernel definition of relative singular chains in the Recognition foundation. Downstream, relative_homology_id_isZero lifts the result degreewise: $H_n(X,X)=0$ for every $n$, by applying the homology functor to a zero complex. The parent theorem's doc-comment states the intent explicitly: it "locks the semantics of the cokernel definition of the relative complex."
Without this vanishing, the pair short exact sequence and the long exact sequence of relative homology would be mis-calibrated at the identity pair. In the broader RS stack the singular-pair apparatus sits under the foundation layer that feeds forcing and observer constructions; a wrong relative complex would corrupt any later use of relative homology as a defect or comparison measure. The lemma itself is pure algebraic topology and does not invoke J-cost, $\varphi$, or the T0–T8 chain, but it is the base case those layers rely on when they treat pairs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.