Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedverified 2026-09-24 (gpt-6-sol)
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 and singular homology agree

Statement

For every simplicial complex K and abelian group G, there is a canonical natural isomorphism Hnsimp(K;G)≅Hn(∣K∣;G) for all n. When the vertex set has a supplied total order, it is induced by the simplicial-to-singular chain map of The degreewise simplicial-to-singular homomorphisms, extended G-linearly. Different supplied orders induce the same homology map. For an arbitrary vertex set, the isomorphism is defined compatibly on its finite subcomplexes and requires no choice principle.

Facts & Assumptions

Given: An abstract simplicial complex K with weak geometric realization and an abelian group G.

Proof

technique · induction
1.1givenbase

Every finite complex has a total order on its finite vertex set. For a chosen order, the characteristic-simplex homomorphisms give a chain map Φ:C∗simp(K;G)→C∗sing(∣K∣;G) by the cited boundary lemma, and give a map of pair exact sequences for every subcomplex. No tensor-exactness is used: the chain groups in both pair sequences are degreewise split by their simplex bases.

1.2givenconstruct

We will use finite simplicial-subcomplex excision without invoking the later CW-homology-axioms item. Let L be a nonempty subcomplex of a finite K. Under the canonical homeomorphism ∣sd⁡K∣≅∣K∣ of Barycentric subdivision realizes homeomorphically, the vertices of sd⁡L are the nonempty faces of L. They span a full subcomplex of sd⁡K: in any face chain, the faces belonging to L form an initial segment because L is closed under taking faces. For x∈∣sd⁡K∣, let s(x) be the sum of its barycentric coordinates at these vertices. This is a continuous function, and U={s>0} is an open neighborhood of ∣sd⁡L∣. On U discard the other coordinates and divide the retained ones by s(x), obtaining a continuous map r:U→∣sd⁡L∣. In each subdivided simplex the straight-line homotopy (1−t)x+tr(x) stays in that simplex, fixes ∣sd⁡L∣, and retracts U onto it. Thus every such finite pair is a good pair in Good pairs and quotient reduced homology. If finite complexes K=L∪σ with L∩σ=∂σ, their quotient map-out descriptions give ∣K∣/∣L∣≅∣σ∣/∣∂σ∣, so inclusion (∣σ∣,∣∂σ∣)→(∣K∣,∣L∣) induces an isomorphism on relative singular homology when dim⁡σ>0. The same argument applies to ∂Δr=F∪Λ with F∩Λ=∂F for r≥2, giving H∗(F,∂F;G)≅H∗(∂Δr,Λ;G). These are exactly the two finite excisions used below.

1.3givenalgebra

We compute the singular relative group of an oriented simplex without using any simplicial-to-singular comparison. For r=0, H0(Δ0,∅;G)=G, generated by its vertex. For r=1, the pair sequence of the contractible interval and its two endpoints gives H1(Δ1,∂Δ1;G)=ker⁡(G2→(a,b)↦a+bG); the oriented edge maps to its endpoint difference and generates this kernel. All other relative groups vanish.

1.4givenconstruct

We prove finite support for a compact subset C⊆∣K∣ without making choices from the set of simplices. The weak realization is Hausdorff: every vertex-coordinate function is continuous by testing its restriction on each finite simplex, and distinct points differ in some coordinate. Thus C is closed. For each open simplex σ∘ meeting C and integer m≥1, define Tσ,m=C∩{x∈∣σ∣:αv(x)≥1/m for every v∈σ}. Let mσ be the least m for which this set is nonempty, and put Tσ=Tσ,mσ. Such an integer exists because every coordinate of a point in C∩σ∘ is positive. The set Tσ is closed in the compact finite-dimensional simplex ∣σ∣, hence is nonempty compact, and every point of it remains in σ∘. For each of the finitely many total orders o on the finite vertex set of σ, successively minimize the coordinates in that order on Tσ; finite-dimensional compactness and the extreme-value theorem give a unique lexicographic minimum xσ,o∈Tσ. Define Fσ={xσ,o:o is a total order on σ}. This is a canonically defined nonempty finite subset of C∩σ∘, even though no order on the vertices of K has been chosen.

2.1step 1.2step 1.3ihalgebra

For r≥2 let F be the facet of Δr opposite its first vertex and let Λ be the union of the other facets. Then ∂Δr=F∪Λ and F∩Λ=∂F. Both Δr and Λ are contractible and nonempty: Λ is the cone from the first vertex on ∂F. The pair long exact sequence gives Hk(Δr,Λ;G)=0 for every k. The short exact sequence of relative singular chain complexes 0→C∗(∂Δr,Λ;G)→C∗(Δr,Λ;G)→C∗(Δr,∂Δr;G)→0 therefore gives, by its homology long exact sequence, an isomorphism Hk(Δr,∂Δr;G)→∂Hk−1(∂Δr,Λ;G) for k≥1. The explicit finite-subcomplex excision in step 1.2 identifies the right group with Hk−1(F,∂F;G). By induction from the degree-zero and degree-one computations of step 1.3, the only nonzero relative group is G in degree k=r. Under the two isomorphisms, the affine characteristic simplex [v0,…,vr] maps first to its alternating boundary and then, modulo Λ, to the opposite facet with coefficient +g (up to the fixed orientation sign); the other facets vanish in that quotient. Thus its relative class is exactly a generator, with no appeal to a prior sphere or simplicial comparison. Degree zero vanishes because ∂Δr is nonempty.

2.2step 1.4algebra

Put S=⋃σ∘∩C≠∅Fσ. Each closed simplex ∣τ∣ meets only those Fσ for which σ is a face of τ, and there are finitely many such faces; hence S∩∣τ∣ is finite. The same holds for every subset of S, so every subset of S is closed in the weak topology of ∣K∣. In particular S is closed in the compact space C, hence compact, and it is discrete because its singleton complements are closed. The singleton open cover of a compact discrete space has a finite subcover, so S is finite. The pairwise disjoint nonempty sets Fσ⊆σ∘ therefore occur for only finitely many occupied simplices σ. Their faces form a finite subcomplex containing C. The construction used finite total orders within each simplex only as an indexed finite set, never a simultaneous selection of one order per simplex.

3.1step 1.1step 1.2step 1.3step 2.1ihalgebra

Let K be finite and build it one simplex at a time in a face-respecting order. Suppose L has already been built and the next simplex is σ. Then L∩σ=∂σ. The simplicial relative chain complex of (K,L) is one copy of G in degree dim⁡σ and zero elsewhere. If dim⁡σ>0, the finite-subcomplex excision proved in step 1.2 identifies H∗(∣K∣,∣L∣;G) with H∗(∣σ∣,∣∂σ∣;G). If dim⁡σ=0, then ∣K∣=∣L∣⊔∣σ∣ and its singular relative chain complex is directly the singular complex of the isolated vertex, giving the same relative comparison even when L is empty. Step 1.3 or 2.1 shows that Φ maps the relative simplicial generator to its singular generator. The commuting pair long exact sequences and the five lemma extend the isomorphism from L to K. The empty complex starts the induction.

4.1step 3.1step 2.2

Every singular cycle and every singular chain witnessing a boundary is a finite sum of compact simplex images, so step 2.2 supports each in some finite subcomplex. Simplicial chains already have finite support. The finite comparison from step 3.1 is therefore surjective and injective on the directed union of finite subcomplexes, proving the isomorphism for all K. Finite unions make this directed system choice-free. [step 3.1, step 2.2].

5.1step 1.1step 3.1step 4.1discharge-induction∎

It remains to make the comparison canonical and natural. On a finite complex two vertex orders give chain maps Φ,Ψ agreeing on vertices. Construct a chain homotopy recursively on each oriented simplex σ. If it is already defined on proper faces, the chain z=(Φ−Ψ)(σ)−H(∂σ) is a cycle in the convex ∣σ∣; in degree zero the difference is zero. Coning z to the barycenter of σ gives H(σ) with boundary z (the augmented cone identity also handles a zero-chain of augmentation zero). This is a finite explicit prescription and works G-linearly. Hence different orders induce the same map on homology. For a simplicial map f:K→P, the two chain maps f#ΦK and ΦPf∗ agree on vertices, and their values on σ lie in the convex simplex ∣f(σ)∣. The identical coning induction proves they are chain homotopic, including when f collapses a simplex. On finite subcomplexes this proves order independence and naturality; step 4.1 passes them to arbitrary complexes without selecting orders simultaneously for all finite subcomplexes.

Depends on

Used by

Dependency tree · two levels

73 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