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

Transverse preimages for maps from manifolds with boundary

Statement

Let $W$ be a smooth manifold with boundary, $N$ a smooth manifold without boundary, $Z \subseteq N$ a closed embedded submanifold, and $F : W \to N$ a smooth map. Suppose that at every $p \in F^{- 1} (Z)$ the differential is transverse to $Z$ , $d F_{p} (T_{p} W) + T_{F (p)} Z = T_{F (p)} N$ , and that the restriction $F ∣_{\partial W}$ is transverse to $Z$ . Then $F^{- 1} (Z)$ is an embedded smooth submanifold with boundary of $W$ of dimension $\dim W - codim Z$ , with

$T_{p} F^{- 1} (Z) = {v \in T_{p} W : d F_{p} (v) \in T_{F (p)} Z}$

and $F^{- 1} (Z) \cap \partial W = (F ∣_{\partial W})^{- 1} (Z)$ . If $\dim W - codim Z \geq 1$ , then $F^{- 1} (Z)$ is neat and

$\partial (F^{- 1} (Z)) = F^{- 1} (Z) \cap \partial W = (F ∣_{\partial W})^{- 1} (Z) .$

If $\dim W = codim Z$ , transversality of the boundary restriction forces $F^{- 1} (Z) \cap \partial W = \emptyset$ : a space of dimension $\dim W - 1$ cannot surject onto the $codim Z$ normal directions. Thus the zero-dimensional preimage also has the asserted empty boundary. If $\dim W < codim Z$ , the preimage is empty by the same rank bound. These include the empty-preimage cases.

Facts & Assumptions

Given: A smooth map $F : W \to N$ from a manifold with boundary to a boundaryless manifold, a closed embedded submanifold $Z \subseteq N$ of codimension $c$ , and transversality of $F$ and of $F ∣_{\partial W}$ to $Z$ .

[F1]

A slice chart for $Z$ at $z \in Z$ is a chart $y : V \to y (V) \subseteq R^{n^{'}}$ with $y (Z \cap V) = y (V) \cap (R^{n^{'} - c} \times {0})$ ; the last $c$ coordinates of $y$ then define a submersion on $V$ with zero set $Z \cap V$ (Embedded submanifolds and slice charts).

[F2]

Transversality of $F$ to $Z$ means $d F_{p} (T_{p} W) + T_{F (p)} Z = T_{F (p)} N$ at every $p \in F^{- 1} (Z)$ , and $F ∣_{\partial W}$ is transverse to $Z$ when the same condition holds for the restricted differential on $T_{p} \partial W$ at every $p \in F^{- 1} (Z) \cap \partial W$ (A smooth map transverse to an embedded submanifold).

[F3]

Boundary charts of $W$ are homeomorphisms $φ : U \to φ (U) \subseteq H^{n}$ with $φ (U \cap \partial W) = φ (U) \cap {x_{n} = 0}$ (Smooth charts, atlases, and structures with boundary).

[F4]

If $G : M^{m} \to N^{n^{'}}$ is smooth on a boundaryless manifold and transverse to $Z$ , then $G^{- 1} (Z)$ is an embedded submanifold of codimension $c$ with $T_{p} G^{- 1} (Z) = {v \in T_{p} M : d G_{p} (v) \in T_{G (p)} Z}$ (The transverse preimage theorem).

[F5]

An embedded submanifold with boundary $S \subseteq W$ is neat when $S \cap \partial W = \partial S$ and $S$ is transverse to $\partial W$ ; a neat submanifold has boundary charts simultaneously straightening $S$ and $\partial W$ (Neat submanifolds of a manifold with boundary, Neat submanifolds have boundary-adapted slice charts).

[F6]

A smooth function on a relatively open subset of $H^{n}$ extends locally to a smooth function on an open subset of $R^{n}$ , and the chain rule holds for smooth maps between manifolds with boundary (Smooth functions on relatively open half-space sets, Smooth maps between manifolds with boundary). The Euclidean inverse function theorem applies to an invertible local extension (The Euclidean inverse function theorem).

Proof

technique · reduce to a submersion identity in a half-space chart, then apply the inverse function theorem in the two cases

1.1F1F2F3F6givenalgebra

Fix $p \in F^{- 1} (Z)$ and put $z : = F (p)$ ; write $n : = \dim W$ and $n^{'} : = \dim N$ . At a boundary point choose a boundary chart $x : U \to x (U) \subseteq H^{n}$ with $x (p) = 0$ ; at an interior point use an ordinary Euclidean chart centred at $p$ and a slice chart $y : V \to y (V)$ of $Z$ at $z$ with $y (z) = 0$ , and let $g$ be the last $c$ coordinates of $y$ on $V$ . Then $G : = g \circ F$ is defined near $p$ on a relatively open half-space set, and for $q$ near $p$ one has $G (q) = 0$ exactly when $F (q) \in Z$ . At such a $q$ the differential $d G_{q} = d g_{F (q)} \circ d F_{q}$ is surjective: $d g_{F (q)}$ is surjective with kernel $T_{F (q)} Z$ , so its image of $d F_{q} (T_{q} W)$ is $(d F_{q} (T_{q} W) + T_{F (q)} Z) / T_{F (q)} Z = T_{F (q)} N / T_{F (q)} Z$ , which is all of $R^{c}$ by [F2]. At boundary points, on the face ${x_{n} = 0}$ the same computation with $T_{q} \partial W$ in place of $T_{q} W$ is surjective by the transversality of $F ∣_{\partial W}$ .

2.1F1F4step 1.1

(Interior points.) If $p \in F^{- 1} (Z) \cap int W$ , then $F ∣_{int W}$ is smooth and transverse to $Z$ on the boundaryless manifold $int W$ , so [F4] shows that $F^{- 1} (Z) \cap int W$ is an embedded submanifold of $int W$ of codimension $c$ with the stated tangent space; in the chart $x$ this exhibits $F^{- 1} (Z)$ near $p$ as a coordinate subspace ${x^{n - c + 1} = \dots = x^{n} = 0}$ intersected with the chart, so $p$ is an interior point of $F^{- 1} (Z)$ .

2.2F1F2F3F6step 1.1construct

(Boundary points.) If $p \in F^{- 1} (Z) \cap \partial W$ , then in the coordinates of 1.1 the differential $d G_{p} : R^{n} \to R^{c}$ is surjective and, by the face part of 1.1, its restriction to the face $R^{n - 1} \times {0}$ is surjective. Choose a set $A$ of $c$ coordinate directions inside the face on which the resulting square minor of $d G_{p}$ is invertible, let $B$ be the remaining $n - 1 - c$ face directions, and define $Φ : = (G, x_{B}, x_{n})$ near $p$ . Its differential is block triangular with invertible diagonal blocks, hence invertible; by [F6] the components extend smoothly to an open neighbourhood of $p$ in $R^{n}$ , so the inverse function theorem makes $Φ$ a local diffeomorphism at $p$ . Since $Φ$ has last coordinate $x_{n}$ , it carries ${G = 0, x_{n} \geq 0} = F^{- 1} (Z)$ near $p$ onto the relatively open subset ${0} \times R^{n - 1 - c} \times [0, \infty)$ of the half-space $H^{n - c}$ ; therefore $F^{- 1} (Z)$ is near $p$ an embedded $(n - c)$ -dimensional submanifold with boundary, with boundary exactly $F^{- 1} (Z) \cap \partial W$ and tangent space ${v \in T_{p} W : d F_{p} (v) \in T_{z} Z}$ , and the chart $Φ$ simultaneously straightens the preimage and the face.

3.1F4F5step 2.1step 2.2given∎

(Assembly.) The charts produced in 2.1 and 2.2 cover $F^{- 1} (Z)$ ; any two of them are restrictions of charts of $W$ , so their transitions are restrictions of smooth half-space transitions and the induced structure is a smooth structure on $F^{- 1} (Z)$ making it an embedded submanifold with boundary of $W$ , of dimension $n - c = \dim W - codim Z$ , with the tangent formula and with interior $F^{- 1} (Z) \cap int W$ and boundary $F^{- 1} (Z) \cap \partial W = (F ∣_{\partial W})^{- 1} (Z)$ . If $n - c \geq 1$ , the local model of 2.2 shows that the preimage is transverse to $\partial W$ and meets it exactly in its boundary, so $F^{- 1} (Z)$ is neat and $\partial F^{- 1} (Z) = F^{- 1} (Z) \cap \partial W$ ; the charts of 2.2 are precisely the boundary-adapted slice charts of [F5]. If $n - c = 0$ , boundary points are impossible because the face differential would have rank $c = n$ on an $(n - 1)$ -dimensional space. The preimage is discrete, lies in the interior, and has empty boundary. If $n < c$ , even the full differential cannot be surjective, so the preimage is empty. The construction uses the charts named at each point and no choice principle; the atlas of the preimage is the set of all charts so obtained.

Depends on

Used by

Dependency tree · two levels

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