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.
Space of immersions and space of formal immersions
Definition
Assume (The Axiom of Countable Choice ()) for the canonical smooth tangent bundles and the weak topology on their total spaces. For smooth manifolds with , let be the set of immersions and let be the set of formal immersions . Both carry the subspace topology inherited from the weak compact-open topologies on and defined above (for the product topology). The projection , , is continuous and its image contains under . The formal-immersion space fibres over with fibre over the set of injective smooth bundle maps ; this description is recorded but the fibre structure is not used until the normal-bundle items.
Depends on
- Formal immersion between smooth manifolds
- The weak compact-open C-infinity topology on mapping spaces
- Immersions, submersions, and constant-rank maps
- Smooth manifolds and their smooth charts
- The product set $\prod_{i \in I} X_i$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
Used by
- Regular homotopy classes of immersions are formal homotopy classes Corollary
- Compact parameter pairs and relative families Definition
- Regular homotopy of immersions Definition
- The derivative map from immersions to formal immersions Definition
- Immersing the circle in the plane from a formal line monomorphism Example
- Formal-immersion homotopies extend over a collar Lemma
- Formal-immersion homotopies extend over a subcritical handle Lemma
- Immersion extension on a disk: absolute and relative parametric forms Lemma
- Positive-codimension thickening reduces closed sources to the open case Lemma
- Regular homotopy preserves the formal Gauss class Lemma
- Restriction of formal-immersion data has the parametric lifting property Lemma
- Smooth families and path components in the weak topology Lemma
- Smoothing continuous families of formal immersions Lemma
- Smoothing continuous families of genuine immersions Lemma
- The derivative map is continuous Lemma
- Euclidean formal immersions are homotopy equivalent to Stiefel-bundle sections Proposition
- Smale-Hirsch makes rank reduction sufficient for Euclidean immersion in positive codimension Proposition
- Smale–Hirsch for open source manifolds Theorem
- Smale's classification of sphere immersions in Euclidean space Theorem
- The Smale–Hirsch immersion theorem Theorem
- Whitney–Graustein classification of plane circle immersions Theorem
Dependency tree · two levels
33 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
- Andrew Ranicki, Algebraic and Geometric Surgery, Ch. 7 §7.4 “The Smale–Hirsch classification of immersions”, printed pp. 142–146 (Theorem 7.35, Proposition 7.39) (standard reference, not scraped)
- John Francis, The h-Principle, Lecture 3: Immersion theory (notes by O. Gwilliam), PDF pp. 1–4: Proposition 2.2 (disk), Definition 2.5 (Serre fibration), Definition 2.6 and Proposition 2.7 (flexible sheaves) (standard reference, not scraped)
- Ralph L. Cohen, Bundles, Manifolds, and Homotopy, Ch. 7 §2 “Obstructions to the existence of embeddings and immersions, the Hirsch–Smale theorem”, printed pp. 226–232 (Theorem 7.5, Corollary 7.6) (standard reference, not scraped)