Pith. sign in
module module moderate

IndisputableMonolith.Foundation.SingularPair

show as:
view Lean formalization →

Singular homology infrastructure for topological pairs $(X,A)$: relative chain complexes, the canonical short exact sequence of chains, and monomorphisms induced by injective continuous maps. Algebraic topologists computing relative groups or Mayer–Vietoris sequences cite it. The module assembles Mathlib homology primitives with injectivity and retract lemmas into degreewise exact pair sequences.

claimFor a pair of spaces $(X,A)$, the relative singular chain complex $C_*(X,A)$ fits in a short exact sequence of chain complexes $0 \to C_*(A) \to C_*(X) \to C_*(X,A) \to 0$, exact in every degree. Injective continuous maps induce monomorphisms on singular $n$-simplices and on chain complexes; generating retracts compose compatibly with these chain maps.

background

Singular homology is built from the free abelian groups on continuous maps $\Delta^n \to X$. For a subspace $A \subseteq X$, the relative chains $C_n(X,A)$ are the quotient of $C_n(X)$ by the image of $C_n(A)$. The resulting complex computes relative homology $H_n(X,A)$, the natural home for excision, long exact sequences of pairs, and sphere computations.

The module sits on SingularPrism (singular simplices and prism operators) and Mathlib's homological-complex and homology-sequence libraries. Sibling material records that postcomposition with an injective continuous map remains injective on singular $n$-simplices, that generating retracts exist and compose, and that the induced chain maps are monomorphisms.

Local notation treats pairs as the basic input: relative singular chains, the pair short exact sequence, and its degreewise exactness.

proof idea

Definitions introduce relative singular chains and the pair short exact sequence of complexes. Injectivity of the map on singular simplices (postcomposition with an injective continuous map) lifts to monomorphisms of chain complexes. Generating retracts are constructed so that composition identities hold on generators and therefore on chain maps. Short exactness of the pair sequence is checked degreewise from the quotient definition of relative chains, then promoted to a short exact sequence of chain complexes via Mathlib's homological-complex API.

why it matters in Recognition Science

Relative pairs and their SES are the standard bridge from absolute singular homology to excision and Mayer–Vietoris. Downstream, SingularMayerVietoris and SingularSphere import this module, so sphere homology and MV gluing rest on the pair SES and the mono lemmas here. In the Recognition Science foundation layer this supplies the algebraic-topology substrate for dimensional and cellular arguments (including the forcing-chain step that isolates $D=3$), without yet committing to the J-cost or $\phi$-ladder physics layer.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (21)