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.
The singular homology of a disjoint union is the direct sum
Statement
Let be a disjoint union of topological spaces, and let be an abelian group. Then for every ,
Facts & Assumptions
Given: A disjoint union , an abelian group , and an integer .
Singular homology is computed from the singular chain complex (The singular chain complex and singular homology).
In the disjoint-union topology, each summand is an open and closed subspace of (The disjoint union (coproduct) with the final topology of the canonical injections: a set is open exactly when each of its traces is).
Proof
The standard simplex is path-connected: if and are points of , the straight-line map stays in . Therefore any singular simplex has connected image. Since the sets are pairwise disjoint and clopen by [L2], the image of lies in exactly one summand .
Step 1.1 identifies with the direct sum of the chain groups , degree by degree, and the singular boundary preserves the chosen summand because each face of a simplex in still lands in . Thus as chain complexes.
Cycles and boundaries of a direct-sum chain complex are taken componentwise, so homology also splits componentwise. Applying [L1] to the chain-complex isomorphism of step 2.1 yields
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
11 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
- Allen Hatcher, Algebraic Topology (standard reference, not scraped)