ExampleConstruction: Literature-sourcedVerification: 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.

An open parallelizable manifold immerses in Euclidean space of equal dimension

Example

Assume ${A C}_{ω}$ . Let $M$ be an open (no compact component) smooth $m$ -manifold whose tangent bundle is trivial, $T M ≅ M \times R^{m}$ ; for instance $M = R^{m}$ minus a point, the open annulus $S^{1} \times (0, 1) \subset R^{2}$ in the case $m = 2$ , or any open subset of $R^{m}$ . Then $M$ immerses in $R^{m}$ , and even every formal immersion $M \to R^{m}$ (equivalently, after fixing a global frame of $T M$ and the standard frame of $T R^{m}$ , a pair consisting of a smooth map $M \to R^{m}$ and a smooth map $M \to G L_{m} (R)$ ) is homotopic through formal immersions to a genuine immersion. Indeed a global frame of $T M$ together with the standard frame of $T R^{m}$ defines a formal immersion $(f, F)$ for every smooth $f$ , and the open-source Smale–Hirsch theorem deforms it to a genuine immersion in the equidimensional case. For $m \geq 1$ , a nonempty closed $m$ -manifold is excluded by the equidimensional obstruction, so the open-source hypothesis is essential. In dimension zero an open manifold in this convention is empty; nonempty compact zero-manifolds do admit immersions into $R^{0}$ .

Facts & Assumptions

Given: ${A C}_{ω}$ and an open (no compact component) smooth $m$ -manifold $M$ whose tangent bundle is trivial, $T M ≅ M \times R^{m}$ .

[F1]

A vector bundle is trivial if and only if it has a global frame, and a global frame is the same as a family of everywhere linearly independent sections (Local and global frames of a vector bundle, A vector bundle is trivial if and only if it has a global frame).

[L1]

The open-source Smale–Hirsch theorem: for an open source $M$ and $m \leq n$ the derivative map $D : Imm (M, N) \to FImm (M, N)$ is a weak homotopy equivalence, with the relative parametric form; in particular every formal immersion is homotopic through formal immersions to a genuine immersion (Smale–Hirsch for open source manifolds).

[L2]

A smooth map $f : M \to R^{m}$ together with a bundle map $F : T M \to T R^{m}$ over $f$ that is fibrewise injective is a formal immersion (Formal immersion between smooth manifolds); after fixing frames of both trivial bundles, smooth bundle maps $T M \to T R^{m}$ over a fixed base correspond exactly to smooth matrix-valued maps $M \to {Mat}_{m \times m} (R)$ ; the fibrewise injective maps correspond exactly to smooth maps $M \to G L_{m} (R)$ (Smooth vector bundles, rank, fibres, and trivial bundles).

Verification

technique · direct

1.1F1L2givenconstruct

Choose a global frame of $T M$ by [F1] and the standard frame of $T R^{m}$ ; for any smooth $f : M \to R^{m}$ , define $F$ to be the bundle map over $f$ that carries the frame of $T M$ to the standard frame of $T R^{m}$ fibrewise. Then $F$ is a fibrewise linear isomorphism, hence fibrewise injective, and $(f, F)$ is a formal immersion by [L2].

2.1L1step 1.1

Since $M$ has no compact component, [L1] applies in the equidimensional case $m = n$ : the formal immersion $(f, F)$ is homotopic through formal immersions to a genuine immersion $g : M \to R^{m}$ , so $M$ immerses in $R^{m}$ and every formal immersion is homotopic through formal immersions to a genuine one.

3.1L1step 2.1∎

For $m \geq 1$ , a nonempty closed $m$ -manifold is excluded: by the equidimensional obstruction A nonempty closed n-manifold cannot immerse in R-n for n at least one no nonempty closed $m$ -manifold immerses in $R^{m}$ , so openness of the source is essential; the examples $M = R^{m}$ minus a point, the open annulus $S^{1} \times (0, 1) \subset R^{2}$ , and open subsets of $R^{m}$ have trivial tangent bundles and no compact component, so the theorem applies to them. For $m = 0$ , the no-compact-component condition forces $M = \emptyset$ , since each point is a compact component; its unique map to $R^{0}$ is an immersion. The countable-choice assumption of [L1] is inherited.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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