Foundation Singular Pair To Sset Map App Injective

Injectivity on simplices

In algebraic topology, a singular simplex is a continuous map from a standard triangle (or tetrahedron, or higher-dimensional analogue) into a space. The declaration toSSet_map_app_injective is a formal lemma in the framework's machine-checked library of formal theorems. It states that if a continuous map between two spaces is injective, then the induced map on singular n-simplices is also injective, for every dimension n.

The proof is short and direct. Postcomposing an injective map with another map preserves injectivity: if two simplices become equal after composition with an injective map, they must have been equal to begin with. The lemma formalizes this intuition in the framework's categorical language, where a space is viewed through its singular set, a discrete record of all possible simplices in that space.

This injectivity result is a building block for deeper theorems. It feeds into the proof that an injective continuous map induces a monomorphism on the chain complexes used to define homology, and that the associated relative homology sequence is exact. These are standard tools for computing how a subspace sits inside a larger space.

In Recognition Science, the lemma appears in the construction of relative homology for a pair of spaces, where one space is a subspace of another. The injectivity condition is what guarantees the short exact sequence of chain complexes, a fundamental structure in homological algebra. The framework's library uses this to build the long exact sequence of relative homology, a classical result that relates the homology of a space, its subspace, and the quotient.

The lemma does not claim that every continuous map is injective, nor that injectivity holds for maps between singular simplices themselves. It also does not assert that the induced map on homology is injective; that is a separate, stronger statement that requires additional hypotheses. The lemma is specifically about the map on the level of simplices, before passing to homology.

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

What this page does not claim

The lemma does not claim that every continuous map is injective. The lemma does not claim that the induced map on homology is injective. The lemma does not claim that injectivity holds for maps between singular simplices themselves.

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: