CorollaryStatement: Literature-sourcedProof: Literature-sourcedPipeline-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.

A cycle has zero algebraic intersection with a bounding cycle

Statement

Assume ${A C}_{ω}$ . Let $M$ be a closed oriented $n$ -manifold, $A^{a} \subseteq M$ a closed oriented embedded submanifold, and $W^{b + 1} \subseteq M$ a compact oriented embedded submanifold with boundary, with $a + b = n$ and $B : = \partial W$ oriented outward-normal-first. Assume the inclusion of $A$ is transverse to $W$ and to $\partial W$ . Then $I (A, B) = 0 and I_{2} (A, B) = 0.$ The same vanishing holds for the mod 2 number without orientability hypotheses, provided the intersection is transverse. The compactness of $W$ is essential: an extension over a noncompact trace, or an intersection escaping at infinity, need not preserve the count.

Facts & Assumptions

Given: A closed oriented $A^{a} \subseteq M^{n}$ , a compact oriented $W^{b + 1} \subseteq M$ with boundary $B = \partial W$ , $a + b = n$ , and transversality of the inclusion of $A$ to $W$ and to $\partial W$ .

[F1]

Since $A$ is closed in the closed manifold $M$ and $W$ is compact, the inclusion $i_{W} : W \to M$ is transverse to $A$ , and its boundary restriction is transverse to $A$ ; hence $W \cap A$ is a compact embedded submanifold with boundary of $W$ , neat, of dimension $b + 1 - b = 1$ , with $\partial (W \cap A) = W \cap A \cap \partial W = A \cap B$ (Transverse preimages for maps from manifolds with boundary, Embedded smooth submanifolds with boundary, Transverse embedded submanifolds).

[F2]

Orient $S = W \cap A$ by the normal-first quotient $Q = T M / T A$ and kernel-first convention $\det T W = \det T S \otimes \det Q$ , and orient $\partial S$ outward-normal-first (Preimage orientation agrees with the local intersection sign, Induced boundary orientation).

[F3]

Local intersection signs compare the written factor order; swapping blocks of dimensions $a, b$ multiplies the sign by $(- 1)^{a b}$ (Swapping direct summands scales oriented bases by a sign, The local oriented intersection sign).

[F4]

The signed boundary sum of the compact oriented $1$ -manifold $W \cap A$ vanishes (Oriented boundary counts of a compact oriented 1-manifold cancel), and its boundary has even cardinality (Boundary of a compact 1-manifold has even cardinality); both rest on the classification of compact $1$ -manifolds, so this corollary inherits ${A C}_{ω}$ through them and steps 1.1-3.1 add no further choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F5]

$I (A, B)$ is the finite sum of the local signs over $A \cap B$ , and $I_{2} (A, B)$ is its cardinality modulo two (The oriented intersection number, The mod 2 intersection number).

Proof

technique · direct; count the boundary of the compact oriented $1$-manifold $W\cap A$

1.1F1F2F4F5given

By [F1] the set $W \cap A$ is a compact oriented $1$ -manifold with boundary $A \cap B$ , oriented as in [F2]; its boundary is finite by [F4], so $A \cap B$ is a finite transverse intersection and both $I (A, B)$ and $I_{2} (A, B)$ are defined.

2.1F2F3F4F5step 1.1algebra

At $p \in A \cap B$ , the map $T B \to Q$ is an isomorphism. Choose an outward vector $r$ tangent to $S$ ; its existence follows from neatness, and let $u$ be a positive determinant of $T B$ . Then $(r, u)$ is positive for $T W$ by the boundary convention. The sign of $d i_{B} (u)$ in $Q$ is the local sign $ε_{(B, A)}$ , since quotient lifts precede $T A$ . The kernel-first convention therefore assigns the outward $r$ that same sign in $T S$ , so the boundary point sign is $ε_{(B, A)} = (- 1)^{a b} ε_{(A, B)}$ . This determinant-element argument also covers $b = 0$ . Summing over $\partial S = A \cap B$ gives $\sum ε_{\partial S} = (- 1)^{a b} I (A, B)$ . The sum vanishes by [F4], hence $I (A, B) = 0$ .

3.1F1F4F5step 1.1algebra∎

Independently of orientations, [F4] says that the boundary of the compact $1$ -manifold $W \cap A$ has even cardinality; that boundary is $A \cap B$ by [F1], so $# (A \cap B)$ is even and $I_{2} (A, B) = 0$ by [F5]. This mod 2 statement assumes no orientability of $A$ , $W$ or $M$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

59 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

Victor Guillemin and Alan Pollack, Differential Topology (Prentice-Hall, 1974; complete 236-page PDF) (standard reference, not scraped)
John Milnor, Topology from the Differentiable Viewpoint (Princeton University Press; complete 76-page PDF, including the appendix Classifying 1-manifolds) (standard reference, not scraped)