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.
Cohomology over a field is dual to homology over that field
Statement
Assume AC. For every field , every space , and , evaluation gives a natural -linear isomorphism There is no finite-dimensional hypothesis. The right side is the full algebraic dual.
Facts & Assumptions
Singular cochain complex with coefficients identifies -valued singular cochains with ; Singular cohomology with coefficients takes the cohomology quotient.
Singular UCT extension from cycle projections gives the natural exact evaluation sequence over every PID, with the Ext term computed by restrictions from to .
Under The Axiom of Choice, Zorn's lemma gives a basis between any linearly independent set and any spanning set containing it: if with independent and , there is a basis of with supplies a basis of a vector space and extends an independent subset to a basis.
Proof
Given: as stated and AC. Set .
A field is a PID: any nonzero ideal contains a nonzero , hence , and is the whole ring; the zero ideal is generated by zero. The complex is nonnegative and free on the singular simplex sets. Thus [F2] applies, and [F1] identifies its middle group with .
Put . Apply [F3] first to the empty independent set in to obtain a basis of , then to to extend it to a basis of . For any linear , define a map on by its existing values on and zero on . Every vector of has a unique finite basis expansion, so summing its coefficients against these values defines a linear with . Consequently restriction is onto, and the cokernel Ext term in [F2] is zero.
Exactness from step 1.1 and vanishing from step 1.2 make evaluation both injective and surjective. Its formula is , and its naturality in is exactly the chain-map naturality in [F2]. The auxiliary bases used to prove Ext vanishing do not occur in this map. Arbitrary functionals are admitted: step 1.2 uses finite expansions of individual vectors, with no finite support requirement on the functional or finite bound on the basis.
For , and the same result follows with empty bases. For empty , both sides are zero. On a point in degree zero, evaluation identifies with via multiplication by the value at the constant zero-simplex; the value yields the identity. If , the isomorphism forces . AC is inherited in [F2] and used explicitly in both basis applications of step 1.2. No identification of an infinite-dimensional vector space with its double dual is made.
Depends on
- Singular cohomology with coefficients
- Singular UCT extension from cycle projections
- The Axiom of Choice
- Singular cochain complex with coefficients
- Zorn's lemma gives a basis between any linearly independent set and any spanning set containing it: if $L \subseteq S \subseteq V$ with $L$ independent and $\operatorname{span}(S) = V$, there is a basis $B$ of $V$ with $L \subseteq B \subseteq S$
Used by
- Top squares do not determine lower squares Counterexample
- A proper singular curve with weight-zero cohomology Example
- Field cohomology of an infinite wedge of circles Example
- Mod-two cohomology ring of real projective space Example
- Proper Cech descent does not require acyclic fibers Example
- Steenrod squares on real projective space Example
- Stiefel-Whitney numbers of real projective space Example
- The punctured line has a weight-two logarithmic class Example
- The signature of the product of two 2-spheres is zero: the hyperbolic intersection form Example
- A Bockstein class on RP-two times RP-four has nonzero integral Sq-three Lemma
- Admissible square actions have distinct leading monomials Lemma
- Characteristic numbers of products satisfy the Whitney-sum and Kunneth product formulas Lemma
- Finite products and comparison cones have homological finite type Lemma
- Finite type and odd-primary acyclicity of K(F₂,q) Lemma
- Finite-cellular cyclic squares, Cartan formula, and cyclic-basis action Lemma
- Local path-fibration and cohomology inputs for mod-two Eilenberg–Mac Lane induction Lemma
- Mod-two cohomology ring of infinite real projective space Lemma
- Modification preserves open cohomology images Lemma
- Orientation coefficients are deck eigenspaces, with product and duality pairings Lemma
- Rational cohomology of K(Z,n) through weak CW fiber comparison Lemma
- Rational cohomology scalar comparison on compact smooth manifolds Lemma
- Rational sphere homotopy below the first unstable degree Lemma
- Real projective space cellular homology and the pinch map Lemma
- The boundary kernel of a compact oriented 3-manifold is Lagrangian Lemma
- The boundary middle form is well defined and glues Lemma
- The Lefschetz numbers of the two lifts sum to twice the base Lefschetz number Lemma
- The middle-dimensional intersection form is symmetric and nondegenerate Lemma
- The orientation-twisted diagonal realizes the Lefschetz trace Lemma
- The restriction image on a cobordism boundary is Lagrangian Lemma
- Whitney sum defines the connected coalgebra on stable Thom cohomology Lemma
- Products of complex projective spaces span rational oriented bordism Proposition
- The first Stiefel–Whitney class classifies orientability Proposition
- A transgressive simple fiber system gives a polynomial base Theorem
- Logarithmic construction of smooth-open mixed Hodge structures Theorem
- Proper cohomology and functorial mixed Hodge weights Theorem
Dependency tree · two levels
27 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
- Miller, section 27, Remark 27.3 and Theorem 27.1, printed pages 73–74 (standard reference, not scraped)