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 middle-dimensional intersection form is symmetric and nondegenerate

Statement

Assume AC (The Axiom of Choice), inherited from Poincare duality. Let $M$ be a closed oriented smooth $4 k$ -manifold with middle form $Q_{M}$ (The middle-dimensional intersection form of a closed oriented 4k-manifold). Then: (1) $Q_{M} (x, y) = Q_{M} (y, x)$ for all $x, y \in H^{2 k} (M; R)$ ; (2) the adjoint maps $x \mapsto Q_{M} (x, -)$ and $y \mapsto Q_{M} (-, y)$ are isomorphisms onto the full $R$ -linear dual, so $Q_{M}$ is nondegenerate and $H^{2 k} (M; R)$ is finite dimensional; (3) on the free quotient $H^{2 k} (M; Z) / Tor$ the integral pairing is unimodular, and the torsion subgroup lies in its kernel; (4) for $M = M_{1} ⊔ \dots ⊔ M_{r}$ with induced orientations, $Q_{M}$ is the orthogonal direct sum $⨁_{j} Q_{M_{j}}$ under $H^{2 k} (M; R) ≅ ⨁_{j} H^{2 k} (M_{j}; R)$ . All statements hold verbatim with $Q$ in place of $R$ .

Facts & Assumptions

Given: AC; a closed oriented smooth $4 k$ -manifold $M$ with fundamental class $[M]$ and middle form $Q_{M}$ ; the field $F$ is $R$ or $Q$ .

[F1]

$Q_{M} (x, y) = ⟨ x ⌣ y, [M] ⟩$ on $H^{2 k} (M; R) \times H^{2 k} (M; R)$ , restricting on integral classes to the integral pairing, and $Q_{\emptyset} = 0$ (The middle-dimensional intersection form of a closed oriented 4k-manifold).

[F2]

Cup product is graded commutative: $u ⌣ v = (- 1)^{p q} v ⌣ u$ for $u \in H^{p}$ , $v \in H^{q}$ (Singular cohomology is graded commutative).

[F3]

Assume AC. For a closed $F$ -oriented $n$ -manifold with $F$ a field, the pairing $H^{p} \times H^{n - p} \to F$ , $(a, b) \mapsto ⟨ a ⌣ b, [M] ⟩$ , is perfect with both adjoints onto the full dual, and the groups are finite-dimensional; for $R = Z$ and an integral orientation the same formula induces a unimodular pairing on the free quotients $H^{p} (M; Z) / Tor$ and $H^{n - p} (M; Z) / Tor$ , which are finite free abelian groups with both adjoints to the integer duals isomorphisms (Poincaré duality gives a nonsingular cup pairing).

[F4]

Cap with the compatible compact orientation classes gives the duality isomorphisms $D_{M} : H_{c}^{p} (M; R) \to H_{n - p} (M; R)$ , and for compact $M$ one has $D_{M} (a) = a \cap [M]$ (Poincaré duality for oriented topological manifolds).

[F5]

For a closed $R$ -oriented $n$ -manifold with $R$ a commutative PID, every $H_{q} (M; R)$ and $H^{p} (M; R)$ is finitely generated and vanishes outside degrees $0, \dots, n$ (Finite generation from cap with a finite fundamental cycle).

[F6]

The Kronecker pairing is additive in both variables, independent of representatives, and natural: $⟨ f^{*} α, z ⟩ = ⟨ α, f_{*} z ⟩$ (Kronecker evaluation pairing, The kronecker pairing is independent of cocycle and cycle representatives).

[F7]

The fundamental class of a disjoint union corresponds to the finite tuple of component fundamental classes: for $M = ⨆_{j = 1}^{r} M_{j}$ with inclusions $i_{j}$ , the class $[M]$ is $\sum_{j} (i_{j})_{*} [M_{j}]$ , and the orientation of $M$ restricts to the given orientation on each component (Fundamental class of a compact oriented manifold).

[F8]

For every field $k$ and space $X$ , evaluation is an isomorphism $H^{n} (X; k) \to {Hom}_{k} (H_{n} (X; k), k)$ (Cohomology over a field is dual to homology over that field).

[F9]

Singular homology of a disjoint union splits: $H_{n} (⨆_{α} X_{α}; G) ≅ ⨁_{α} H_{n} (X_{α}; G)$ (The singular homology of a disjoint union is the direct sum).

Proof

technique · direct; symmetry from graded commutativity, nondegeneracy from Poincare duality, and the componentwise clause from naturality

1.1givenF1F2F6

Symmetry: for $x, y \in H^{2 k} (M; F)$ the cup product has $p = q = 2 k$ in [F2], so $x ⌣ y = (- 1)^{4 k^{2}} y ⌣ x = y ⌣ x$ because $4 k^{2}$ is even; since the Kronecker evaluation is additive in the first variable by [F6], $Q_{M} (x, y) = Q_{M} (y, x)$ .

1.2givenF1F3F4F5

Nondegeneracy and finite-dimensionality: with $p = n - p = 2 k$ the perfectness clause of [F3] says that $H^{2 k} (M; F)$ is finite dimensional and that the adjoint maps $x \mapsto ⟨ x ⌣ -, [M] ⟩$ and $y \mapsto ⟨ - ⌣ y, [M] ⟩$ into the full $F$ -linear dual are isomorphisms; these maps are exactly $x \mapsto Q_{M} (x, -)$ and $y \mapsto Q_{M} (-, y)$ by [F1], the duality isomorphisms underlying the perfectness being the cap isomorphisms of [F4]; finite generation for $F = R, Q$ also follows from [F5] with $R = F$ .

1.3givenF1F3F5F6algebra

Integral clause: the second clause of [F3] gives that the integral pairing descends to a unimodular pairing on $H^{2 k} (M; Z) / Tor$ with both adjoints to the integer duals isomorphisms, with these groups finite free abelian. The torsion subgroup lies in the kernel: if $n x = 0$ in $H^{2 k} (M; Z)$ , then $n (x ⌣ y) = (n x) ⌣ y = 0$ by bilinearity, so $x ⌣ y$ is torsion in $H^{4 k} (M; Z)$ , and any group homomorphism from a torsion group to the torsion-free group $Z$ is zero, whence $⟨ x ⌣ y, [M] ⟩ = 0$ for every $y$ by [F1].

1.4givenF1F6F7F8F9

Componentwise clause: write $M = ⨆_{j = 1}^{r} M_{j}$ with inclusions $i_{j}$ . By [F7] $[M] = \sum_{j} (i_{j})_{*} [M_{j}]$ , and by [F6] evaluated on this sum, $Q_{M} (x, y) = \sum_{j} ⟨ x ⌣ y, (i_{j})_{*} [M_{j}] ⟩ = \sum_{j} ⟨ i_{j}^{*} (x ⌣ y), [M_{j}] ⟩ = \sum_{j} ⟨ i_{j}^{*} x ⌣ i_{j}^{*} y, [M_{j}] ⟩ = \sum_{j} Q_{M_{j}} (i_{j}^{*} x, i_{j}^{*} y)$ , using naturality of the cup product. The restriction maps $(i_{j}^{*})_{j}$ identify $H^{2 k} (M; F)$ with $⨁_{j} H^{2 k} (M_{j}; F)$ : by [F8] and [F9] the group is ${Hom}_{F} (⨁_{j} H_{2 k} (M_{j}; F), F) ≅ \prod_{j} H^{2 k} (M_{j}; F)$ , a finite product, hence the direct sum, and naturality of the duality isomorphism in the inclusions identifies the factors with the restrictions. Under this identification the displayed identity says precisely that $Q_{M}$ is the orthogonal direct sum of the forms $Q_{M_{j}}$ : classes from distinct components pair to zero and each summand carries its own form.

2.1step 1.1step 1.2step 1.3step 1.4given∎

Steps 1.1-1.4 prove clauses (1)-(4); replacing $F$ by $Q$ throughout uses the field clauses of [F3] and [F5] verbatim, while clause (3) remains the assertion about integral coefficients. For $k = 0$ the pairing is $Q_{M} (x, y) = \sum_{j} ε_{j} x_{j} y_{j}$ on the component-wise constant classes, the signed count; for $M = \emptyset$ all groups vanish and $Q_{\emptyset} = 0$ , and both assertions hold trivially.

Depends on

Used by

Dependency tree · two levels

41 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

Daniel S. Freed, Bordism: Old and New (lecture notes, UT Austin, Fall 2012) (standard reference, not scraped)
John Milnor and James Stasheff, Characteristic Classes (re-typeset scan; original pagination) (standard reference, not scraped)
Tom Weston, An Introduction to Cobordism Theory (lecture notes, Stanford) (standard reference, not scraped)