LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-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.

Compact oriented manifolds with boundary have finite-dimensional field cohomology

Statement

Assume the Axiom of Choice. Let $W$ be a compact oriented smooth $n$ -manifold with boundary $\partial W$ (possibly empty), let $F$ be a field, and let the cohomology be singular cohomology with coefficients in $F$ . Then every $H^{k} (W; F)$ and every relative group $H^{k} (W, \partial W; F)$ , $k \geq 0$ , is a finite-dimensional $F$ -vector space.

Facts & Assumptions

Given: A compact oriented smooth $n$ -manifold $W$ with boundary $\partial W$ and a field $F$ .

[A1]

The Axiom of Choice is assumed (The Axiom of Choice).

[L1]

Assuming ${A C}_{ω}$ , the labelled double $D M$ of a smooth manifold with boundary $M$ carries a smooth boundaryless manifold structure, and the double of The double of a smooth manifold with boundary is the quotient of $M_{+} ⊔ M_{-}$ identifying the two copies of the boundary (The double has a well-defined smooth structure).

[L2]

In ZF, $A C \Rightarrow D C \Rightarrow {A C}_{ω}$ (AC implies DC implies countable choice).

[L3]

For an oriented manifold $M$ with boundary, the induced boundary orientation is fixed by the outward-normal-first convention: its local generator is $(- 1)^{n}$ times the tangent generator for the product orientation, and each component inherits its sign from the supplied interior orientation (Relative fundamental class and boundary orientation).

[L4]

Assume AC. If $M$ is a closed $R$ -oriented $n$ -manifold and $R$ is a commutative PID, then every $H_{q} (M; R)$ and every $H^{p} (M; R)$ is finitely generated over $R$ (Finite generation from cap with a finite fundamental cycle).

[L5]

Singular homology with coefficients in an abelian group is covariantly functorial: a retraction $r \circ i = i d$ of spaces induces $r_{*} \circ i_{*} = i d$ on homology (Singular chains and singular homology are covariantly functorial).

[L6]

Singular cohomology is contravariantly functorial, so a retraction $r \circ i = i d$ induces $i^{*} \circ r^{*} = i d$ on cohomology (Singular cohomology is contravariantly functorial).

[L7]

Assume AC. For a compact $R$ -oriented $n$ -manifold $M$ with boundary $A$ , cap with the relative fundamental class gives isomorphisms $T_{p} : H^{p} (M, A; R) \tilde{\to} H_{n - p} (M; R)$ for every $p$ (Poincaré–Lefschetz duality).

Proof

technique · direct

1.1A1L1L2given

The double $D (W)$ of $W$ is a smooth boundaryless manifold by [L1], whose ${A C}_{ω}$ hypothesis holds because [A1] gives AC and [L2] gives $A C \Rightarrow {A C}_{ω}$ ; it is compact because $W$ is compact.

2.1step 1.1L3given

The double $D (W)$ is oriented: orient the labelled first copy $W_{+}$ by the given orientation of $W$ and the second copy $W_{-}$ by its reverse, so that at every boundary point the two induced boundary orientations are opposite and hence agree after this reversal; by [L3] the induced boundary orientations are determined by the interior orientations, so they glue to a global orientation of $D (W)$ , making $D (W)$ a closed oriented $n$ -manifold.

3.1step 2.1L5L6given

The folding map $r : D (W) \to W$ that maps both labelled copies identically onto $W$ is well defined on the quotient and continuous, and its composite with the inclusion $i : W \to D (W)$ of the first copy is $r \circ i = {i d}_{W}$ ; hence by [L5] the induced maps satisfy $r_{*} \circ i_{*} = i d$ on $H_{k} (-; Z)$ and on $H_{k} (-; F)$ , so $i_{*}$ is injective with left inverse $r_{*}$ , while by [L6] the induced maps satisfy $i^{*} \circ r^{*} = i d$ on $H^{k} (-; F)$ , so $r^{*}$ is injective with left inverse $i^{*}$ .

4.1step 3.1L4A1

Applying [L4] to the closed oriented manifold $D (W)$ with $R = Z$ , and again with $R = F$ (a field is a PID and a $Z$ -orientation induces an $F$ -orientation), shows that $H_{k} (D (W); Z)$ , $H_{k} (D (W); F)$ and $H^{k} (D (W); F)$ are finitely generated over their coefficient rings; a direct summand of a finitely generated module is finitely generated, so by step 3.1 the groups $H_{k} (W; Z)$ , $H_{k} (W; F)$ and $H^{k} (W; F)$ are finitely generated, and for the field $F$ this says exactly that $H_{k} (W; F)$ and $H^{k} (W; F)$ are finite-dimensional over $F$ .

5.1step 4.1L7A1

Cap with the relative fundamental class of the compact oriented manifold $W$ gives, by [L7] with $R = F$ and $A = \partial W$ , an $F$ -linear isomorphism $H^{k} (W, \partial W; F) \tilde{\to} H_{n - k} (W; F)$ for every $k \geq 0$ ; the target is finite-dimensional over $F$ by step 4.1.

6.1step 4.1step 5.1∎

Therefore every $H^{k} (W; F)$ is finite-dimensional by step 4.1 and every relative group $H^{k} (W, \partial W; F)$ is finite-dimensional by step 5.1, which is the assertion.

Depends on

Used by

Boundary middle form and boundary signature Definition
The boundary middle form is well defined and glues Lemma

Dependency tree · two levels

46 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, Cambridge University Press 2002 (complete book) (standard reference, not scraped)
Ioan Marcut, Manifolds (2017 lecture notes), sections 14.5 and 15.1 (standard reference, not scraped)