Foundation Singular Pair Chain Map Comp Gen Retract

The retraction lemma

In algebraic topology, a singular simplex is a continuous map from a standard triangle into a topological space. A continuous injective map between spaces, such as an inclusion of a subspace, carries each singular simplex of the smaller space to a singular simplex of the larger one. The question is whether this carry-over loses information: can two distinct simplices in the smaller space be sent to the same simplex in the larger space? The lemma chainMap_comp_genRetract answers no, provided the original map is injective.

The proof works by constructing an explicit algebraic retraction. For each dimension n, the chain map induced by an injective continuous map has a right inverse on the subgroup generated by the image simplices. This right inverse, called genRetract, sends each image simplex back to its unique preimage, using the injectivity hypothesis to guarantee uniqueness. The composition of the chain map followed by this retraction is exactly the identity on the smaller chain group. This is the statement chainMap_comp_genRetract: the induced map on singular chains is a split monomorphism, meaning it has a one-sided inverse that recovers the original data.

The consequence is that an injective continuous map induces an injective map on singular chain complexes at every degree. This is the lemma chainMap_mono, which follows immediately from the retraction identity. Injectivity of chain maps is a standard prerequisite for exact sequences in homology; the framework's library uses this to build short exact sequences for pairs of spaces, such as a subspace included in a larger space. The retraction itself is a concrete computational device, not merely an existence statement: it is defined by cases, checking whether a given simplex lies in the image of the induced map.

In Recognition Science, this lemma supports the framework's treatment of recognition, the discrete record of events that the framework models as singular simplices. The framework uses the injectivity result to ensure that when one space is recognized as part of another, the record of the smaller space is preserved without merging distinct entries. This is a structural guarantee about the algebraic representation, not a statement about physical measurement. The lemma is proved in the machine-checked library of formal theorems, meaning its logical validity is verified by a computer.

The lemma does not claim that every continuous map is injective, nor that the induced map on homology is injective. It applies only to the chain level, not to the homology level, and only under the explicit hypothesis that the original map is injective. It also does not assert anything about the existence of a retraction for non-injective maps, where distinct simplices may collapse together. These limits are built into the statement itself, not added as afterthoughts.

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

/-- The chain map splits: `chainMap f n ≫ genRetract f n = 𝟙`. -/
lemma chainMap_comp_genRetract (f : A ⟶ X) (hf : Function.Injective f.hom) (n : ℕ) :
    chainMap f n ≫ genRetract f n = 𝟙 (Cgrp A n) := by
  apply Sigma.hom_ext
  intro a
  rw [comp_id, ← assoc, gen_map f n a]
  exact gen_comp_genRetract f hf n a

/-- For injective `f`, `genRetract` retracts the chain map on generators. -/
lemma gen_comp_genRetract (f : A ⟶ X) (hf : Function.Injective f.hom) (n : ℕ)
    (a : Idx A n) :
    gen X n ((TopCat.toSSet.map f).app (op ⦋n⦌) a) ≫ genRetract f n = gen A n a := by
  unfold genRetract
  rw [Sigma.ι_desc]
  have hx : ∃ a' : Idx A n, (TopCat.toSSet.map f).app (op ⦋n⦌) a' =
      (TopCat.toSSet.map f).app (op ⦋n⦌) a := ⟨a, rfl⟩
  rw [dif_pos hx]
  exact congrArg (gen A n) (toSSet_map_app_injective f hf n hx.choose_spec)

What this page does not claim

The lemma does not claim injectivity on homology groups, only on chain complexes. It does not apply to non-injective continuous maps, where distinct simplices may collapse. It does not assert that the retraction exists for arbitrary chain maps without the injectivity hypothesis.

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: