TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Simplicial approximation after sufficient subdivision

Statement

Let $K, L$ be finite simplicial complexes, $A \subseteq K$ a subcomplex, and $f : ∣ K ∣ \to ∣ L ∣$ continuous. Suppose $f ∣_{∣ A ∣}$ is the realization of a simplicial map in the chosen triangulation of $A$ . For some $r \geq 0$ there is a simplicial map $g : D_{A}^{r} K ⟶ L$ whose realization agrees pointwise with $f$ on $∣ A ∣$ , and a homotopy from $f$ to $∣ g ∣$ relative to $∣ A ∣$ .

Here relative simplicial approximation means this relative homotopy conclusion. It imposes no additional requirement that $∣ g ∣ (x)$ lie in the carrier of $f (x)$ for every $x$ . With $A = \emptyset$ the subdivision is ordinary barycentric subdivision and the conclusion is ordinary simplicial approximation. No AC is needed.

Facts & Assumptions

[F1]

Relative simplicial approximation after subdivision supplies a simplicial map on $D_{A}^{r} K$ and a homotopy fixed on $∣ A ∣$ , under exactly the stated finite-complex and chosen-triangulation hypotheses. Its relative proof first adjusts the map near $A$ and then uses the open-star criterion.

[F2]

Relative derived subdivision of a finite simplicial pair defines $D_{A} K$ by retaining $A$ and coning the already triangulated boundaries of other simplices from their barycenters. It preserves the underlying polyhedron and becomes ordinary barycentric subdivision when $A$ has no vertices.

Proof

Given: The finite complexes, their specified subcomplex and triangulation, and the continuous map with its simplicial restriction.

1.1

The pair $(K, A)$ meets the hypotheses of [F1]: both complexes are finite, $A$ is a subcomplex, and the required simplicial restriction holds on this actual triangulation. Thus [F1] provides $r$ , a simplicial $g : D_{A}^{r} K \to L$ , and a continuous $H : ∣ K ∣ \times [0, 1] \to ∣ L ∣$ with $H (x, 0) = f (x)$ , $H (x, 1) = ∣ g ∣ (x)$ and $H (a, t) = f (a)$ for every $a \in ∣ A ∣$ and every $t$ . We have identified $∣ D_{A}^{r} K ∣$ with $∣ K ∣$ by [F2]'s polyhedron-preserving construction. At $t = 1$ the fixed-point formula gives $∣ g ∣ (a) = f (a)$ , so the map and the homotopy have exactly the asserted relative agreement.

F1F2given

2.1

In [F1]'s proved construction, the first homotopy runs from $f$ to $f h$ , where $h$ is homotopic to the identity fixing $A$ , and the second runs from $f h$ to $∣ g ∣$ by the carrier interpolation for $f h$ . These concatenate because their common endpoint is $f h$ , and both are fixed on $A$ . This explains why step 1.1 gives the stated relative homotopy without asserting a strict carrier condition for the original $f$ away from $A$ . No refinement of the source triangulation is silently assumed to preserve simpliciality of $f ∣_{A}$ ; [F1]'s prescribed-subdivision clause is conditional on that same simpliciality hypothesis on the new triangulation.

F1step 1.1

3.1

If $A$ is empty, [F2] gives $D_{A}^{r} K = {sd}^{r} K$ , and [F1] gives the ordinary approximation conclusion with no fixed-subspace restriction. If $A = K$ , take $r = 0$ , the supplied simplicial map $g = f$ , and $H (x, t) = f (x)$ ; the hypotheses make this a valid simplicial map and constant homotopy. If $K$ is empty, the empty map and empty homotopy suffice, also when $L$ is empty. If $L$ is empty and $K$ is nonempty, no map $f$ meeting the hypothesis exists. Zero-dimensional complexes and simplicial maps that collapse vertices or higher faces are included by [F1]. All vertex selections in that theorem's finite-complex construction are finite, so the present application introduces no AC.

F1F2given∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

8 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Hatcher, Algebraic Topology, Theorem 2C.1, pp.177–179 (standard reference, not scraped)
E. C. Zeeman, Relative simplicial approximation, pp.39–42 (standard reference, not scraped)