Foundation Singular Pair

The singular pair

In algebraic topology, a singular pair is a topological space X together with a subspace A contained in it. The pair (X, A) gives rise to relative homology: the homology of the space X with the subspace A collapsed to a point. This measures the shape of X outside A, and it sits in a long exact sequence that links the homology of A, the homology of X, and the relative homology of the pair. The setup is classical and appears in every standard treatment of the subject.

The framework's machine-checked library of formal theorems builds this classical setup from scratch and proves its central structural facts. It constructs the singular chain complex of a space, defines the relative chain complex as the cokernel of the inclusion map, and proves that for an injective continuous map from A into X, the resulting short sequence of chain complexes is exact. From that exactness, it derives the long exact sequence of relative homology, with the connecting homomorphism and the three exactness properties that make the sequence work.

In Recognition Science, this setup establishes the formal scaffolding for how a subspace sits inside a space. Its key result is that an injective continuous map induces an injective map on singular simplices at every dimension. This injectivity is what lets the framework treat a subspace as a genuine subobject, not merely a quotient or a formal construction. The setup also proves that when the subspace is the whole space, the relative homology vanishes in every degree, which is the expected and necessary base case for the theory.

The practical payoff is that the framework can now reason about spaces with distinguished subspaces in a way that is fully checked by machine. The long exact sequence is the standard tool for computing homology in practice, and having it proved from first principles means the framework's later geometric and physical arguments can rely on it without re-deriving the foundations. This is the kind of infrastructure that makes larger claims trustworthy: the building blocks are verified before they are used.

/-- An injective continuous map induces an injective map on singular
`n`-simplices (postcomposition with an injective map is injective). -/
lemma toSSet_map_app_injective (f : A ⟶ X) (hf : Function.Injective f.hom) (n : ℕ) :
    Function.Injective ((TopCat.toSSet.map f).app (op ⦋n⦌)) := by
  intro a b hab
  have h1 : f.hom.comp (A.toSSetObjEquiv (op ⦋n⦌) a) =
      f.hom.comp (A.toSSetObjEquiv (op ⦋n⦌) b) := by
    rw [← toSSetObjEquiv_map f a, ← toSSetObjEquiv_map f b, hab]
  have h2 : A.toSSetObjEquiv (op ⦋n⦌) a = A.toSSetObjEquiv (op ⦋n⦌) b := by
    ext t
    apply hf
    simpa only [ContinuousMap.comp_apply] using ContinuousMap.congr_fun h1 t
  exact (A.toSSetObjEquiv (op ⦋n⦌)).injective h2

/-- An injective continuous map induces a degreewise monomorphism of
singular chain complexes. -/
lemma chainMap_mono (f : A ⟶ X) (hf : Function.Injective f.hom) (n : ℕ) :
    Mono (chainMap f n) :=
  mono_of_mono_fac (chainMap_comp_genRetract f hf n)

/-- An injective continuous map induces a monomorphism of singular chain
complexes. -/
lemma sChainMap_mono (f : A ⟶ X) (hf : Function.Injective f.hom) :
    Mono (sChainMap f) :=
  HomologicalComplex.mono_of_mono_f _ fun n => chainMap_mono f hf n

/-- For an injective continuous map, the sequence
`0 ⟶ C_*(A) ⟶ C_*(X) ⟶ C_*(X, A) ⟶ 0` is short exact. -/
lemma pairSES_shortExact (f : A ⟶ X) (hf : Function.Injective f.hom) :
    (pairSES f).ShortExact where
  exact := ShortComplex.exact_of_g_is_cokernel _ (cokernelIsCokernel (sChainMap f))
  mono_f := sChainMap_mono f hf
  epi_g := by
    show Epi (cokernel.π (sChainMap f))
    infer_instance

/-- Degreewise form of the short exact sequence: in every degree `n`,
`0 ⟶ C_n(A) ⟶ C_n(X) ⟶ C_n(X, A) ⟶ 0` is a short exact sequence of
`ℤ`-modules. -/
lemma pairSES_degreewise_shortExact (f : A ⟶ X) (hf : Function.Injective f.hom)
    (n : ℕ) :
    ((pairSES f).map
      (HomologicalComplex.eval (ModuleCat.{0} ℤ) (ComplexShape.down ℕ) n)).ShortExact :=
  (pairSES_shortExact f hf).map_of_exact _

/-- **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)

What this page does not claim

This setup does not prove that the singular pair is the unique or preferred way to set up relative homology. The setup does not establish any physical content about recognition or cost. The long exact sequence here is for singular homology, not for any other homology theory.

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: