Foundation Singular Pair Gen Comp Gen Retract

The retraction lemma

In algebraic topology, a retraction is a one-sided inverse: a map that pulls a space back to a subspace while leaving the subspace fixed. The lemma gen_comp_genRetract in the Recognition Science library establishes that every injective continuous map between topological spaces admits such a retraction at the level of the framework's discrete records. Concretely, if a space A sits inside a space X by an injective map, then for every dimension n the framework's ledger records of X can be sent back to the ledger records of A in a way that composes with the forward map to give the identity on A's records.

The framework's ledger, a discrete record of events, assigns to each topological space a collection of algebraic objects, one for each dimension, built from its continuous maps from standard simplices. The lemma proves that an injective map between spaces induces an injective map on these ledger objects, and that the retraction exists precisely because the original map is injective. The proof works by showing that each ledger element of X that comes from A can be traced back to a unique ledger element of A, using the injectivity to rule out ambiguity. The result is a formal theorem in the machine-checked library of formal theorems, not a paper claim.

The lemma is one step in a longer argument that builds the framework's relative homology theory, the algebraic tool that measures how a subspace sits inside a larger space. It feeds directly into the proof that the ledger's chain complexes form short exact sequences, which in turn yield the long exact sequences of relative homology. The retraction itself is the technical workhorse that makes the injectivity of the chain maps possible, and that injectivity is what lets the framework compare the ledger records of a space with those of its subspaces.

What the lemma does not claim is just as important. It does not say that every injective map has a retraction as a continuous map between the original spaces; that is false in general. The retraction exists only on the ledger objects, not on the spaces themselves. It also does not say anything about the ledger records being complete invariants: two different spaces can share the same ledger records, and the lemma says nothing to rule that out. The result is purely about the algebraic structure induced on the ledger, not about the topology of the spaces beyond the initial injectivity assumption.

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

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

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

What this page does not claim

The lemma does not claim that every injective map has a retraction as a continuous map between the original topological spaces. The lemma does not claim that the ledger records are complete invariants that distinguish all non-homeomorphic spaces. The lemma does not claim anything about the physical interpretation of the ledger beyond its algebraic structure.

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: