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.

The relative square equals the mixed evaluation

Statement

Let $W$ be a compact oriented eight-manifold with boundary $M$ , let $j : H^{4} (W, M; Z) \to H^{4} (W; Z)$ be the forgetful map, and let $a \in H^{4} (W, M; Z)$ . Then $⟨ a ⌣ a, [W, M] ⟩ = ⟨ a ⌣ j (a), [W, M] ⟩,$ where the left product uses two relative factors and the right product uses one relative and one absolute factor, and the evaluations are relative Kronecker evaluations.

Facts & Assumptions

Given: A compact oriented eight-manifold $W$ with boundary $M$ , an element $a \in H^{4} (W, M; Z)$ , and the maps $j : H^{4} (W, M; Z) \to H^{4} (W; Z)$ .

[L1]

Relative singular cochains vanish on simplices in $M$ and form the complex whose cohomology is $H^{*} (W, M; Z)$ ; the forgetful map $j$ is induced by the quotient $C_{*} (W; Z) \to C_{*} (W; Z) / C_{*} (M; Z)$ , so a relative cocycle representing $a$ also represents $j (a)$ as an absolute cocycle (Relative singular cochain complex).

[L2]

The relative cup product is built from the front/back cochain product, which vanishes on $N = C_{*} (A; R) + C_{*} (B; R)$ , followed by the comparison $q^{*} : H^{*} (X, U; R) \to H^{*} ({Hom}_{R} (C_{*} (X; R) / N, R))$ ; when $A = B = M$ the comparison is the identity because $N = C_{*} (M; R) = C_{*} (U; R)$ , and when $A = M$ , $B = \emptyset$ it is again the identity because $N = C_{*} (M; R) = C_{*} (U; R)$ (Relative cup product for an excisive triad).

[L3]

The relative products are natural and compatible with the connecting maps (Relative cup products are natural and connector-compatible).

[L4]

Relative Kronecker evaluation is well defined and biadditive, so equal relative cohomology classes have equal evaluations on $[W, M]$ (Relative Kronecker evaluation is well defined, biadditive and natural).

Proof

technique · direct

1.1L1given

Choose a relative cocycle $α$ representing $a$ ; by [L1] the same cochain $α$ , viewed as an absolute cochain, represents $j (a)$ , and $α$ vanishes on every simplex in $M$ .

2.1step 1.1L2

For the product of two relative factors take $A = B = M$ ; the union is $M$ , each copy is open in it, and $C_{*} (M) + C_{*} (M) = C_{*} (M)$ , so the comparison in [L2] is the identity and $a ⌣ a$ is the class of the cochain $α ⌣ α$ in $C^{8} (W, M; Z)$ .

3.1step 2.1L2L3

For the mixed product take $A = M$ and $B = \emptyset$ ; then $U = M$ and $N = C_{*} (M; Z) + 0 = C_{*} (M; Z) = C_{*} (U; Z)$ , so the comparison is again the identity and $a ⌣ j (a)$ is represented by the very same cochain $α ⌣ α$ , which vanishes on $C_{*} (M)$ because its first factor does.

4.1step 3.1L4∎

The two classes therefore have the same relative cochain representative $α ⌣ α$ , so by [L4] their evaluations on the relative fundamental class agree: $⟨ a ⌣ a, [W, M] ⟩ = ⟨ a ⌣ j (a), [W, M] ⟩$ , which is the assertion.

Depends on

Used by

Dependency tree · two levels

23 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

John Milnor, On Manifolds Homeomorphic to the 7-Sphere, Annals of Mathematics 64 (1956), 399-405 (standard reference, not scraped)
Allen Hatcher, Algebraic Topology, Cambridge University Press 2002 (complete book) (standard reference, not scraped)