LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

Finite simplicial approximation for homology comparison

Statement

For finite simplicial pairs $(K, L)$ and $(P, Q)$ , every continuous map $f : (∣ K ∣, ∣ L ∣) \to (∣ P ∣, ∣ Q ∣)$ is homotopic through maps of pairs to a simplicial map $({sd}^{r} K, {sd}^{r} L) \to (P, Q)$ for some $r \geq 0$ .

Facts & Assumptions

Given: The objects and hypotheses in the statement above.

[F1]

Let $(V, K)$ and $(W, L)$ be abstract simplicial complexes. A function $f : V \to W$ is a simplicial map if $f (σ) : = {f (v) : v \in σ}$ is a simplex of $L$ whenever $σ$ is a simplex of $K$ . The geometric realization of $f$ is the map $∣ f ∣ : ∣ K ∣ \to ∣ L ∣$ defined by $∣ f ∣ (α) (w) : = \sum_{v \in f^{- 1} (w)} α (v) .$ Because $α$ has finite support, the sum is finite. The support of $∣ f ∣ (α)$ is contained in $f (supp (α))$ , so it is again a simplex of $L$ . (A simplicial map and its geometric realization)

[F2]

For an affine $n$ -simplex of finite diameter and $n > 0$ , every simplex in its $r$ -fold barycentric subdivision has diameter at most $(n / (n + 1))^{r}$ times the original diameter. Hence the mesh tends to zero. (Mesh tends to zero under iterated subdivision)

[F3]

Let $(X, d)$ be a compact metric space (def-metric-compactness, def-metric-space) and let $U$ be an open cover of $X$ . Then there is a real $δ > 0$ , a Lebesgue number for $U$ , such that every nonempty $A \subseteq X$ with $diam (A) < δ$ (def-metric-bounded-diameter) satisfies $A \subseteq U$ for some $U \in U$ . Diameters of nonempty subsets of $X$ are defined because a compact space is bounded (thm-compact-subset-is-closed-and-bounded) and a subset of a bounded set is bounded. No choice principle is used. (Every open cover of a compact metric space has a Lebesgue number: a $δ > 0$ such that every nonempty subset of diameter less than $δ$ lies inside a single member of the cover)

Proof

1.1

Realize the finite complexes in their barycentric Euclidean spaces. The open star of a vertex $w$ consists of points whose $w$ coordinate is positive. If several open stars intersect, their vertices belong to the support simplex of any point in the intersection; hence they span a simplex. This is the star criterion for a vertex map to extend as in F1.

F1given

1.2

For every $a \in ∣ L ∣$ , some vertex $w$ of $Q$ has positive coordinate at $f (a)$ . The open set $f^{- 1} ({st}_{P} w)$ therefore contains a metric ball $B (a, 2 ϵ_{a})$ . Finitely many $B (a, ϵ_{a})$ cover the compact set $∣ L ∣$ . Choose $η > 0$ smaller than all their radii. Every set of diameter less than $η$ containing a vertex $v \in ∣ L ∣$ lies in one of the corresponding $B (a, 2 ϵ_{a})$ , since $v$ lies in its inner ball. Thus any sufficiently small closed star at a vertex of $L$ maps into the star of a vertex of $Q$ . If $L$ is empty this constraint is absent.

givenchoose

2.1

The preimages of all vertex stars in $P$ cover the compact $∣ K ∣$ . F3 gives a Lebesgue number $λ > 0$ . By F2 choose a common iterated subdivision whose simplex diameters are less than $\min (η, λ) / 3$ , omitting $η$ if $L$ is empty. A closed vertex star has diameter at most twice the mesh. At vertices of the subdivided $L$ make the constrained choice of the preceding step; elsewhere use $λ$ . If $K$ is zero-dimensional the stars are singletons and no subdivision is needed; if $K$ is empty the assertion is vacuous.

F2F3step 1.2

3.1

Call the chosen vertex map $g$ . For a point $x$ in a source simplex with support vertices $v_{j}$ , $f (x)$ belongs to every ${st}_{P} g (v_{j})$ . The star criterion proves that these vertices lie in the support simplex of $f (x)$ . Thus $g$ extends simplicially and $H (x, t) = (1 - t) f (x) + t g (x)$ stays in that same target simplex. It is continuous in the ambient finite-dimensional vector space. If $x \in ∣ L ∣$ , its support simplex under $f$ lies in $Q$ , and so does the whole segment. Its endpoints are $f$ and $g$ , giving the required homotopy of pairs even if several chosen vertices coincide.

F1step 1.1step 2.1∎

Depends on

Used by

Dependency tree · two levels

21 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, §2C, Lemma 2C.2 and Theorem 2C.1, pp.177–179 (standard reference, not scraped)