Alphabeta Math
TheoremStatement: 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.

Parametric transversality

Statement

Let F:M×SN be a smooth family of maps and let ZN be an embedded submanifold. If FZ, then the set of parameters sS for which the slice Fs:MN fails to be transverse to Z is a null subset of S.

Facts & Assumptions

Given: A smooth family F:M×SN transverse to an embedded submanifold ZN.

[F1]

The slice maps Fs come from the evaluation map F (Smooth families of maps and their evaluation maps).

[F2]

Transversality to an embedded submanifold means a tangent-space spanning condition at each point of the preimage (A smooth map transverse to an embedded submanifold).

[L1]

The preimage W=F1(Z) is an embedded submanifold, and for the projection πS:WS, regular values are dense outside a null set (The transverse preimage theorem, Morse-Sard for smooth manifolds).

Proof

technique · direct
1.1

Because FZ, [L1] makes W:=F1(Z)M×S an embedded submanifold. Let πS:WS be the restriction of the second projection.

L1givenconstruct
2.1

Fix (p,s)W and write z:=F(p,s). The fibre of πS over s is πS1(s)={(q,s)M×S:F(q,s)Z}, which identifies with Fs1(Z) by [F1]. A pair (u,w)TpM×TsS lies in T(p,s)W exactly when dF(p,s)(u,w)TzZ, so d(πS)(p,s) is surjective exactly when every wTsS admits some uTpM with dF(p,s)(u,w)TzZ.

F1step 1.1algebra
3.1

If FsZ at p, then [F2] gives dF(p,s)(TpM×{0})+TzZ=TzN. For any wTsS, choose uTpM so that dF(p,s)(u,0)+dF(p,s)(0,w)TzZ. Then (u,w)T(p,s)W, so step 2.1 makes πS a submersion at (p,s).

F2step 2.1algebra
3.2

Conversely, assume πS is a submersion at (p,s). Given ξTzN, the transversality of F in [F2] gives (u,w)TpM×TsS and ηTzZ with ξ=dF(p,s)(u,w)+η. By step 2.1 choose uTpM with (u,w)T(p,s)W, so dF(p,s)(u,w)TzZ. Then ξ=dF(p,s)(uu,0)+(η+dF(p,s)(u,w))dF(p,s)(TpM×{0})+TzZ, which is exactly the transversality condition for Fs at p.

F2step 2.1algebra
4.1

Therefore s is a regular value of πS if and only if the slice Fs is transverse to Z at every point of its fibre. Applying the Sard statement in [L1] to πS shows that the bad parameters form a null subset of S.

L1step 3.1step 3.2

Depends on

Used by

Dependency tree · two levels

18 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