LemmaStatement: AI-adaptedProof: AI-adapted

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 double point has two disjoint embedded sheet disks meeting transversely

Statement

Let $f : M^{m} \to X^{2 m}$ be a self-transverse immersion and let $x \neq y$ be a selected coincident branch pair with common image $r$ . Then there are disjoint closed embedded disks $D_{x} ∋ x$ , $D_{y} ∋ y$ in $M$ such that:

$f ∣_{D_{x}}$ and $f ∣_{D_{y}}$ are smooth embeddings whose images $A : = f (D_{x})$ and $B : = f (D_{y})$ are closed embedded $m$ -disks in $X$ meeting transversely, with $A \cap B = {r}$ ;
if $M$ and $X$ are oriented and the disks carry the induced branch orientations, the local sign of the branch pair $(A, B)$ at $r$ is the local sign of the selected branch pair (Self-transverse immersions and the double point locus, The local oriented intersection sign).

Equivalently, in suitable charts of $M$ at $x$ and $y$ and of $X$ at $r$ , the branch maps take the standard forms $u \mapsto (u, 0)$ and $v \mapsto (0, v)$ on $R^{m}$ , so that near $r$ the pair of branches is the standard transverse pair $(R^{m} \times {0}, {0} \times R^{m})$ in $R^{2 m}$ .

These disks describe the selected pair; they do not exclude other preimages over $r$ . If $r$ is a genuine double point, the selected two preimages are the entire fibre.

Facts & Assumptions

Given: A self-transverse immersion $f : M^{m} \to X^{2 m}$ and a selected coincident pair $x \neq y$ with common image $r$ .

[F1]

Self-transversality gives $d f_{x} (T_{x} M) + d f_{y} (T_{y} M) = T_{r} X$ , a sum of two $m$ -dimensional subspaces in the $2 m$ -dimensional space $T_{r} X$ , hence a direct sum; the branches at $r$ are the local images of $f$ near $x$ and near $y$ (Self-transverse immersions and the double point locus).

[F2]

A smooth embedding is an injective immersion that is a homeomorphism onto its image with the subspace topology (Smooth embeddings, Immersions, submersions, and constant-rank maps).

[L1]

Every immersion is locally an embedding: for each point there is a neighbourhood carried homeomorphically onto an embedded submanifold (Every immersion is locally an embedding).

[L2]

Embedded submanifolds are characterized by slice charts and carry the subspace topology (Embedded submanifolds and slice charts).

[L3]

If $S, T \subseteq X$ are transverse embedded submanifolds of codimensions $a$ and $b$ , then $S \cap T$ is an embedded submanifold of codimension $a + b$ and $T_{p} (S \cap T) = T_{p} S \cap T_{p} T$ at each intersection point (Transverse embedded submanifolds intersect in the expected codimension).

[L4]

If $d F_{p}$ is an isomorphism of tangent spaces at $p$ , then $F$ restricts to a diffeomorphism from a neighbourhood of $p$ onto a neighbourhood of $F (p)$ (The smooth inverse function theorem on manifolds, The differential of a smooth map).

[L5]

When $M$ and $X$ are oriented and the disks carry the induced branch orientations, the local sign of a double point is the local oriented intersection sign of the two oriented branch disks, computed with the first branch first (Self-transverse immersions and the double point locus, The local oriented intersection sign).

[L6]

A smooth manifold is a Hausdorff topological space (Smooth manifolds and their smooth charts); a compact subset of a Hausdorff space is closed (In a Hausdorff space a point and a disjoint compact set, and two disjoint compact sets, have disjoint open neighbourhoods; hence every compact subset is closed, and in a compact Hausdorff space the compact subsets are exactly the closed ones); smooth maps are continuous on compacta and continuous images of compact sets are compact (Smooth maps are continuous).

Proof

technique · direct

1.1L1L2L6

Since $f$ is an immersion and $x \neq y$ , [L1] supplies open neighbourhoods $U$ of $x$ and $V$ of $y$ with $U \cap V = \emptyset$ such that $f ∣_{U}$ and $f ∣_{V}$ are embeddings onto embedded $m$ -submanifolds $A_{0} : = f (U)$ and $B_{0} : = f (V)$ of $X$ ; disjointness of $U$ and $V$ is possible because $M$ is Hausdorff by [L6].

2.1F1step 1.1

The submanifolds $A_{0}$ and $B_{0}$ meet transversely at $r$ : their tangent spaces at $r$ are $d f_{x} (T_{x} M)$ and $d f_{y} (T_{y} M)$ , which span $T_{r} X$ by [F1] as a direct sum.

3.1L2L3step 2.1

By [L3], $A_{0} \cap B_{0}$ is an embedded submanifold of $X$ of codimension $m + m = 2 m = \dim X$ , that is, of dimension $0$ ; by the slice-chart description [L2] applied at $r$ , there is an open neighbourhood $W$ of $r$ in $X$ with $A_{0} \cap B_{0} \cap W = {r}$ .

4.1L6step 1.1step 3.1construct

Choose closed disks $D_{x} \subseteq U$ around $x$ and $D_{y} \subseteq V$ around $y$ so small that $f (D_{x}) \subseteq W$ and $f (D_{y}) \subseteq W$ ; this is possible by continuity of $f$ at $x$ and $y$ , which map to $r$ , and by taking, in a chart of $M$ at $x$ (respectively at $y$ ), a sufficiently small closed coordinate ball. Then $D_{x} \cap D_{y} = \emptyset$ , and $f (D_{x}) \cap f (D_{y}) \subseteq A_{0} \cap B_{0} \cap W = {r}$ , while $r = f (x) = f (y)$ lies in both images, so $A \cap B = {r}$ for $A : = f (D_{x})$ , $B : = f (D_{y})$ .

4.2L2L4step 2.1step 3.1

For the coordinate model, choose a slice chart $(W_{1}, χ_{1})$ of $X$ at $r$ for $A_{0}$ with $χ_{1} (r) = 0$ and $χ_{1} (A_{0} \cap W_{1}) = χ_{1} (W_{1}) \cap (R^{m} \times {0})$ by [L2], and shrink $W_{1}$ so that $r$ is the only point of $A_{0} \cap B_{0}$ in it, as in step 3.1. The image $C : = χ_{1} (B_{0} \cap W_{1})$ is an embedded $m$ -submanifold of $R^{2 m}$ through $0$ whose tangent space at $0$ is complementary to $R^{m} \times {0}$ by step 2.1, so the second projection $π_{2}$ restricts to $C$ with $d (π_{2} ∣_{C})_{0}$ an isomorphism; by [L4] the projection $π_{2} ∣_{C}$ is a local diffeomorphism at $0$ , whence $C$ is near $0$ the graph ${(g (w), w)}$ of a smooth map $g$ defined near $0$ in $R^{m}$ with $g (0) = 0$ . The map $Ψ (u, v) : = (u - g (v), v)$ is then a local diffeomorphism of $R^{2 m}$ at $0$ fixing $0$ , and it carries $C$ to ${0} \times R^{m}$ while fixing $R^{m} \times {0}$ pointwise; hence in the chart $Ψ \circ χ_{1}$ the branch $A_{0}$ is ${v = 0}$ and the branch $B_{0}$ is ${u = 0}$ . Composing with the (smooth) inverse of the embedding $f ∣_{U}$ in these coordinates exhibits $f$ near $x$ as $u \mapsto (u, 0)$ , and similarly near $y$ as $v \mapsto (0, v)$ , which is the displayed standard model.

5.1F2L6step 4.1

The maps $f ∣_{D_{x}}$ and $f ∣_{D_{y}}$ are smooth embeddings: they are restrictions of the embeddings $f ∣_{U}$ , $f ∣_{V}$ to the closed disks, hence injective immersions, and each is a continuous bijection from a compact disk onto its image, with continuous inverse because the inverse is the restriction of the continuous inverse of the ambient embedding. The images $A$ and $B$ are compact, hence closed in the Hausdorff space $X$ by [L6], and each is the image of a closed $m$ -disk under an embedding, so each is a closed embedded $m$ -disk in $X$ .

6.1L5step 4.1step 5.1

The disks $A$ and $B$ meet transversely at $r$ , with $A \cap B = {r}$ , and, when $M$ and $X$ are oriented and the disks have their induced branch orientations, the local sign of the branch pair $(A, B)$ at $r$ is the local sign of the selected branch pair: by [L5] the local sign of the selected branch pair is by definition the local oriented intersection sign of the two ordered branch disks at $r$ , computed with the first branch first, which is exactly the local sign of the pair $(A, B)$ .

7.1step 4.1step 5.1step 6.1step 4.2∎

The disks constructed in steps 4.1 and 5.1, with the model of step 4.2, satisfy clauses 1 and 2 of the statement.

Depends on

Used by

Whitney disjunction removes algebraically cancelling double points Proposition

Cited to discharge well-definedness by Self-transverse immersions and the double point locus.

Dependency tree · two levels

47 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.