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 generation from cap with a finite fundamental cycle
Statement
Assume AC. If is a closed -oriented -manifold and is a commutative PID, then every and is finitely generated over , and these groups vanish outside degrees . In particular this applies to and to every field. Closed means compact and boundaryless; connectedness is not required. The AC use is inherited from Poincaré duality.
Facts & Assumptions
Poincaré duality for oriented topological manifolds identifies cap with the fundamental class as an isomorphism for compact , under AC.
Cap product with cohomology written first evaluates a degree- cochain on the front -face of a simplex and retains its back face; singular chains are finite sums.
A submodule of a free module of finite rank over a PID is free of no larger rank proves that a submodule of a finite free PID module is free of finite rank no larger than the ambient rank.
The Axiom of Choice is assumed for [F1].
Proof
Given: and its orientation. Choose one finite singular cycle representing its fundamental class. Such a representative exists by the definition of the homology class in [F1]. If the class is zero the zero cycle is permitted.
Fix , and put . Let be the submodule of freely spanned by the distinct back faces occurring in . It is free of rank at most : these are a subset of the specified singular simplex basis, and repetitions are removed. For every degree- cochain , the cap formula [F2] gives In particular every cocycle caps to a cycle lying in .
Put . This is a submodule of the finite free module , so [F3] makes it finite free. Its map to , sending a cycle to its homology class, is onto: any homology class is by [F1], and a cocycle representative of gives the cycle in step 1.1. The images of a finite basis of therefore generate . This uses a finite generating module of cycles, not the unsupported claim that the individual back faces are cycles.
For , [F1] identifies with , and negative homology degrees are zero by convention. For , [F1] identifies with the finitely generated of step 2.1. If its target is a negative homology group, and if the cochain complex is zero, proving the stated vanishings. Since only finitely many degrees survive, even the direct sums over all degrees are finitely generated.
Empty has , all , and zero homology. A PID is nonzero by definition, so the zero ring is not a hypothesis here. At , and ; at , cap uses degree-zero cochains and retains the original simplices. For the same proof uses only those vertices. A one-simplex support gives rank at most one for . Degenerate simplices are legitimate basis elements, and duplicate back faces were removed explicitly. Beyond the AC inherited from [F1] for the countable atlas and local UCT, this proof chooses only a single representative cycle and a finite basis in one finite free module; it introduces no further infinite selection.
Depends on
Used by
Dependency tree · two levels
19 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
- Arvind Nair, Topology II (2024), Theorem 1.11.1, printed p.11; statement restricted here to PID coefficients with a direct finite-cap proof (standard reference, not scraped)
- Hatcher, Algebraic Topology, Poincare duality and finite generation discussion, section 3.3 (standard reference, not scraped)