PropositionStatement: Literature-sourcedProof: 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 zero locus of a transverse section represents the Euler dual

Statement

Assume AC. Let $E \to M$ be a smooth $R$ -oriented rank- $r$ real vector bundle over a closed $R$ -oriented smooth $n$ -manifold, with $R = Z$ or $F_{2}$ . Let $s$ be a smooth section transverse to the zero section. Its zero locus $Z$ is a closed embedded submanifold of dimension $n - r$ when nonempty, and $ν_{Z} ≅ E ∣_{Z}$ . Orient its normal bundle by this isomorphism and orient $Z$ in tangent-first order. Then $e (E) \cap [M] = (- 1)^{r (n - r)} (i_{Z})_{*} [Z] \in H_{n - r} (M; R) .$ In particular $(i_{Z})_{*} [Z] \neq 0$ is equivalent to $e (E) \neq 0$ , and either implies $Z \neq \emptyset$ . When $r = n$ , the Euler number $⟨ e (E), [M] ⟩$ is the signed zero count; a nonzero count forces a zero. On a disconnected base the total count may cancel even when the zero-cycle class is nonzero. For $r \neq n$ , no evaluation of $e (E)$ on the $n$ -dimensional fundamental class is asserted. Over $F_{2}$ orientations are canonical and the sign disappears. The zero section defines the Euler class by absolute pullback, and, when $M \neq \emptyset$ , is transverse to itself exactly in rank zero; for $M = \emptyset$ transversality is vacuous.

Facts & Assumptions

Given: AC and $M, E, s, Z$ with the orientations of the statement.

[F1]

The vertical differential induces $ν_{Z} ≅ E ∣_{Z}$ , and this isomorphism defines the tangent-first induced orientation (Normal bundle of the zero locus of a transverse section).

[F2]

The absolute image $\overset{ˉ}{α}$ of the tangent-first normal Thom class satisfies $\overset{ˉ}{α} \cap [M] = (- 1)^{r z} (i_{Z})_{*} [Z]$ (The normal Thom class realizes the Poincare dual of a closed submanifold).

[F3]

The relative pullback of the Thom class through the punctured-bundle pair is the normal Thom class, and its absolute image is $e (E)$ (Pullback of the Thom class along a transverse section computes the Euler class).

[F4]

Cap duality is an isomorphism; degree-top cap followed by zero-chain augmentation is Kronecker evaluation (Poincaré duality for oriented topological manifolds, Cap product with cohomology written first, Kronecker evaluation pairing).

[F5]

Smooth manifolds are admissible bases and their bundles are numerable under AC. The Euler class of a rank-zero bundle is its supplied orientation unit (Smooth manifolds have CW homotopy type, Euler class by zero-section pullback of the Thom class).

[F6]

The relative cochain complex of $(M, M)$ is zero in every degree (Relative singular cochain complex). Singular chains, and hence homology, are zero in negative degrees (The singular boundary operator, The singular chain complex and singular homology). The empty manifold has zero fundamental class (Fundamental class of a compact oriented manifold); in the displayed formula an empty pushforward is the zero class in the indicated homology degree, without a negative-dimensional manifold assertion.

Proof

technique · identify the relative Thom pullback and then forget supports before applying normal Thom duality

1.1F3F6givencasesalgebra

If $Z = \emptyset$ , the relative group $H^{r} (M, M ∖ Z; R) = H^{r} (M, M; R)$ is zero by [F6]. The relative Thom pullback of [F3] therefore has zero absolute image, so $e (E) = 0$ . Its cap with $[M]$ is zero, and the empty pushforward in the displayed formula is the zero class as specified in [F6], also when $r > n$ and the target homology degree is negative. No normal-duality theorem is invoked with a negative-dimensional submanifold. Both nonvanishing assertions are false in this case. Henceforth assume $Z \neq \emptyset$ .

2.1F1F3F5step 1.1given

At an actual zero, transversality gives a surjection $T_{x} M \to E_{x}$ , so $r \leq n$ ; [F1] now gives the closed embedded $(n - r)$ -manifold $Z$ and its normal bundle $E ∣_{Z}$ with the prescribed orientation. By [F5] every bundle and base used here meets the Thom hypotheses. Let $α \in H^{r} (M, M ∖ Z; R)$ be its normal Thom extension and $\overset{ˉ}{α}$ its absolute image. By [F3], $\overset{ˉ}{α} = e (E)$ .

3.1F2F3F4step 1.1step 2.1algebra

In this nonempty case apply [F2] with $z = n - r \geq 0$ to obtain $e (E) \cap [M] = (- 1)^{r (n - r)} (i_{Z})_{*} [Z]$ . Together with step 1.1 this proves the formula in every case. Cap duality [F4] gives the stated equivalence of nonzero classes; either nonzero class excludes the empty case by step 1.1.

4.1F1F4F5step 3.1algebra∎

If $r = n$ , each zero is nondegenerate, and its point orientation is the sign of $D^{v} s : T_{x} M \to E_{x}$ in the supplied orientations. The cap formula of [F4] followed by augmentation therefore gives $⟨ e (E), [M] ⟩ = \sum_{x \in Z} sgn (D^{v} s_{x})$ . If $r = 0$ , $Z = M$ has dimension $n$ ; its induced orientation is the ambient orientation multiplied by the supplied rank-zero orientation unit $o$ (over $Z$ , $o^{- 1} = o$ ). Thus $[Z] = o [M]$ and the formula reads $e (0_{M}, o) \cap [M] = o [M]$ , as [F5] requires. For the zero section the vertical derivative is zero at every base point, so it is surjective exactly when $r = 0$ if the base is nonempty; there are no points to check when the base is empty. Empty manifolds and the canonical mod-two orientations satisfy the same formulas. AC is inherited from the stated suppliers.

The zero locus of a transverse section represents the Euler dual

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources