LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-01

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.

Transversality is equivalent to surjectivity on the normal quotient

Statement

Let $F : M \to N$ be smooth, let $Z \subseteq N$ be an embedded submanifold, and let $p \in F^{- 1} (Z)$ with $y = F (p)$ . Then $F$ is transverse to $Z$ at $p$ if and only if the composite

T_{p} M \overset{d F_{p}}{\to} T_{y} N ↠ T_{y} N / T_{y} Z

is surjective.

Facts & Assumptions

Given: A smooth map $F : M \to N$ , an embedded submanifold $Z \subseteq N$ , and a point $p \in F^{- 1} (Z)$ with $y = F (p)$ .

[F1]

Transversality at $p$ means $d F_{p} (T_{p} M) + T_{y} Z = T_{y} N$ (A smooth map transverse to an embedded submanifold).

[F2]

The normal space of $Z$ at $y$ is the quotient $T_{y} N / T_{y} Z$ (Normal and conormal bundles of an embedded submanifold).

Proof

technique · direct

1.1

Let $π : T_{y} N \to T_{y} N / T_{y} Z$ be the quotient map from [F2]. Its kernel is exactly $T_{y} Z$ . Therefore $π (d F_{p} (T_{p} M)) = T_{y} N / T_{y} Z$ if and only if $d F_{p} (T_{p} M) + T_{y} Z = T_{y} N$ .

F2givenalgebra

2.1

By [F1], the right-hand condition in step 1.1 is exactly transversality of $F$ to $Z$ at $p$ .

F1step 1.1

3.1

Hence transversality is equivalent to surjectivity on the normal quotient.

step 2.1∎

Depends on

Used by

Transversality is stable on a compact source Proposition
The transverse preimage theorem Theorem

Dependency tree · two levels

7 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 M. Lee, Introduction to Smooth Manifolds, 2nd ed. (standard reference, not scraped)