Foundation Singular Pair Relative Homology Id Is Zero

The identity pair

In algebraic topology, relative homology measures the shape of a space X relative to a subspace A. The idea is to count holes and cycles in X while ignoring anything that lies entirely inside A. The Recognition Science framework's machine-checked library of formal theorems contains a result about the simplest possible case: when A is the whole space X, and the map from A into X is the identity map. The theorem relative_homology_id_isZero states that in this case every relative homology group of every degree is zero.

The proof rests on a short exact sequence, a standard algebraic tool that relates the homology of A, of X, and of the pair (X, A). For the identity map, the chain map induced on singular chains is both injective and surjective, so the cokernel, which is the relative chain complex, is zero. Since homology of a zero complex is zero, the result follows. This is a formal theorem, verified by the Lean kernel with no axioms beyond the standard three, and it holds for every topological space and every natural number n.

The theorem is a sanity check rather than a surprise. It confirms that the framework's construction of relative homology behaves exactly as the classical theory demands. It does not claim that relative homology is trivial for any other pair, nor that the identity map is the only map with this property. It also does not address the long exact sequence of a pair, which the framework develops separately in the same file, nor does it say anything about the physical recognition cycle or the forcing chain that motivates the framework's existence.

/-- **Sanity**: the relative homology of the identity pair vanishes in every
degree: `H_n(X, X) = 0`.  This locks the semantics of the cokernel
definition of the relative complex. -/
theorem relative_homology_id_isZero (X : TopCat.{0}) (n : ℕ) :
    IsZero ((relSC (𝟙 X)).homology n) :=
  (HomologicalComplex.homologyFunctor (ModuleCat.{0} ℤ)
    (ComplexShape.down ℕ) n).map_isZero (relSC_id_isZero X)

/-- For the identity inclusion the relative chain complex is zero. -/
lemma relSC_id_isZero (X : TopCat.{0}) : IsZero (relSC (𝟙 X)) := by
  have h : sChainMap (𝟙 X) = 𝟙 (SC X) := CategoryTheory.Functor.map_id _ _
  have : Epi (sChainMap (𝟙 X)) := by rw [h]; infer_instance
  exact isZero_cokernel_of_epi _

What this page does not claim

The theorem does not claim that relative homology is zero for any pair other than the identity pair. The theorem does not claim that the identity map is the only map with a zero relative homology. The theorem does not address the long exact sequence of a pair, which is developed separately in the same file.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/SingularPair.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: