ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck pass

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 signature of the product of two 2-spheres is zero: the hyperbolic intersection form

Example

Assume AC, inherited from Poincare duality, the Kuenneth suppliers and the signature definition. Equip $S^{2}$ with its standard orientation and $S^{2} \times S^{2}$ with the product orientation and product smooth structure. Let $z \in H^{2} (S^{2}; Z)$ be the orientation class, characterized by $⟨ z, [S^{2}] ⟩ = 1$ , and set $a = {p r}_{1}^{*} z$ , $b = {p r}_{2}^{*} z$ . Then $H^{2} (S^{2} \times S^{2}; Z) = Z a \oplus Z b, a \cdot a = 0, b \cdot b = 0, a \cdot b = 1,$ so the middle-dimensional intersection form is the hyperbolic matrix $(\begin{array}{cc} 0 & 1 \\ 1 & 0 \end{array})$ and $σ (S^{2} \times S^{2}) = 0.$ Consequently the first Pontryagin number vanishes: $p_{1} [S^{2} \times S^{2}] = 0$ .

Facts & Assumptions

Given: AC; the standard orientation of $S^{2}$ with its orientation class $z$ and fundamental class $[S^{2}]$ ; the product orientation and product smooth structure on $S^{2} \times S^{2}$ ; the projections ${p r}_{1}, {p r}_{2}$ .

[F1]

For a commutative ring $R$ that is a PID with either every $H_{q} (Y; R)$ or every $H_{p} (X; R)$ finite free over $R$ , the external product is a graded-ring isomorphism $H^{*} (X; R) \otimes_{R} H^{*} (Y; R) \to H^{*} (X \times Y; R)$ ; this uses AC (Cohomological Kunneth cross product is a ring isomorphism).

[F2]

For $n \geq 1$ , ${\tilde{H}}_{k} (S^{n}; G) = G$ for $k = n$ and $0$ otherwise, so $H_{2} (S^{2}; Z) ≅ Z$ and $H_{*} (S^{2}; Z)$ is free (Homology of spheres). The fundamental class $[S^{2}]$ of Fundamental class of a compact oriented manifold restricts at every point to the local generator of the standard orientation, and for the compact connected boundaryless manifold $S^{2}$ restriction to every local stalk is injective with image $Z$ (Top homology of a connected manifold); hence under the identification $H_{2} (S^{2}; Z) ≅ Z$ the class $[S^{2}]$ corresponds to $\pm 1$ and generates $H_{2} (S^{2}; Z)$ .

[F3]

For every space $X$ and $n \geq 0$ the universal coefficient sequence $0 \to {Ext}_{Z}^{1} (H_{n - 1} (X; Z), G) \to H^{n} (X; G) \to {Hom}_{Z} (H_{n} (X; Z), G) \to 0$ is natural with evaluation as the second map; this uses AC (Topological universal coefficient short exact sequence for cohomology). Over a field the evaluation map alone is an isomorphism (Cohomology over a field is dual to homology over that field).

[F4]

With the product orientation and product smooth structure, $S^{2} \times S^{2}$ is a closed oriented smooth $4$ -manifold and $[S^{2} \times S^{2}] = [S^{2}] \times [S^{2}]$ (Product orientations, The fundamental class of a product is the cross product of the fundamental classes, Products of smooth manifolds have a canonical product smooth structure).

[F5]

The Kronecker pairing is multiplicative under cross products: $⟨ α \times β, c \times d ⟩_{X \times Y} = ⟨ α, c ⟩_{X} ⟨ β, d ⟩_{Y}$ (The Kronecker pairing is multiplicative under cross products).

[F6]

The middle-dimensional intersection form is $Q_{M} (x, y) = ⟨ x ⌣ y, [M] ⟩$ on $H^{2 k} (M; R)$ , it is symmetric and nondegenerate, and $σ (M)$ is the positive minus the negative inertia index of $Q_{M}$ (The middle-dimensional intersection form of a closed oriented 4k-manifold, The middle-dimensional intersection form is symmetric and nondegenerate, The signature of a closed oriented manifold of dimension divisible by four).

[F7]

For every closed oriented smooth $4$ -manifold $M$ , $p_{1} [M] = 3 σ (M)$ (The four-dimensional signature formula).

Verification

technique · compute the Kuenneth basis and evaluate the four products on the product fundamental class

1.1givenF2F3

By [F2], $H_{*} (S^{2}; Z)$ is free with $H^{0} (S^{2}; Z) = Z ⟨ 1 ⟩$ , the class $[S^{2}]$ generates $H_{2} (S^{2}; Z) ≅ Z$ , and by [F3] applied to $n = 2$ the evaluation $H^{2} (S^{2}; Z) \to {Hom}_{Z} (H_{2} (S^{2}; Z), Z)$ is an isomorphism because ${Ext}_{Z}^{1} (H_{1} (S^{2}; Z), Z) = 0$ ; hence the dual generator $z$ is the unique class in $H^{2} (S^{2}; Z)$ with $⟨ z, [S^{2}] ⟩ = 1$ , and it is the orientation class of the statement.

2.1step 1.1F1F2F3

By [F1] with $X = Y = S^{2}$ and $R = Z$ , the cross product is a ring isomorphism $H^{*} (S^{2}; Z) \otimes H^{*} (S^{2}; Z) \to H^{*} (S^{2} \times S^{2}; Z)$ ; on degree two it identifies $a = {p r}_{1}^{*} z$ with $z \otimes 1$ and $b = {p r}_{2}^{*} z$ with $1 \otimes z$ , so $H^{2} (S^{2} \times S^{2}; Z) = Z a \oplus Z b$ , while $a ⌣ a$ corresponds to $(z ⌣ z) \otimes 1$ , which is zero because $H^{4} (S^{2}; Z) = 0$ by [F3] and [F2]; $b ⌣ b = 0$ likewise.

3.1step 2.1F4F5F6

By [F4] the product is a closed oriented smooth $4$ -manifold with fundamental class $[S^{2}] \times [S^{2}]$ , so by [F6] and [F5], $Q (a, a) = ⟨ a ⌣ a, [S^{2}] \times [S^{2}] ⟩ = 0$ , $Q (b, b) = 0$ , and $Q (a, b) = ⟨ a ⌣ b, [S^{2}] \times [S^{2}] ⟩ = ⟨ z \times z, [S^{2}] \times [S^{2}] ⟩ = ⟨ z, [S^{2}] ⟩ ⟨ z, [S^{2}] ⟩ = 1$ .

4.1step 3.1F1F3F6

By [F1] over $R$ and field evaluation [F3], the coefficient images of $a, b$ form a real basis (the normalized integral class $z$ maps to the normalized real class); thus in the basis ${a, b}$ the matrix of $Q$ is the hyperbolic matrix $(\begin{array}{cc} 0 & 1 \\ 1 & 0 \end{array})$ ; the class $a + b$ satisfies $Q (a + b, a + b) = 2 > 0$ and $a - b$ satisfies $Q (a - b, a - b) = - 2 < 0$ , and $Q (a + b, a - b) = 0$ . Since $a + b, a - b$ form a basis, this diagonalizes the form to $diag (2, - 2)$ , so the inertia is $(1, 1, 0)$ and [F6] gives $σ (S^{2} \times S^{2}) = 1 - 1 = 0$ .

5.1step 4.1F7∎

By [F7], $p_{1} [S^{2} \times S^{2}] = 3 σ (S^{2} \times S^{2}) = 3 \cdot 0 = 0$ , as claimed.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

88 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)