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 chart bump at a point with prescribed support
Statement
Let be a smooth manifold, let , and let be open with . Then there exists a smooth function such that and .
Facts & Assumptions
Given: A smooth manifold , a point , and an open neighbourhood of .
Smooth charts are diffeomorphisms onto open subsets of Euclidean space (Chart maps are diffeomorphisms onto Euclidean open sets).
Compact sets inside Euclidean open sets admit smooth bumps with prescribed support (A Euclidean bump for a compact set inside an open set).
Smooth maps that agree on overlaps paste to a smooth global map, and composites of smooth maps are smooth (Smooth maps paste over an open cover, Identity maps and composites of smooth maps are smooth).
Closed bounded subsets of , , are compact (Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line); metric and topological compactness agree (For a metric space with its metric topology, compactness in the topological sense is compactness in the metric sense, and the two notions of compact subset coincide).
Continuous images of compact spaces are compact (A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism, clause 1), and compact subsets of a Hausdorff space are 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, clause 3). The manifold is Hausdorff by Smooth manifolds and their smooth charts.
For a real-valued function on , its support means the closure in of its nonzero locus.
Proof
If has dimension zero, each singleton is open by the chart condition and is closed since is Hausdorff. Define and elsewhere. This is locally constant, hence smooth in charts, and its support is . Henceforth assume the dimension is positive.
Choose a smooth chart with and put . Since is open, choose with , and put , . Then . By [L3], is compact. Apply [L1] inside to obtain a smooth equal to one on with support in .
The closed ball is compact by [L3]. Its image under the continuous inverse chart, viewed as a map into , is compact by [L4]. Thus is closed in and .
On the open cover , use on and on . The functions agree on , since its coordinate image misses and hence the support of . Composition and pasting in [L2] give a smooth global real-valued function whose values lie in .
The function equals one at by step 2.1. Its nonzero locus is contained in the closed set by step 4.1, so [F2] gives . This proves the positive-dimensional case, and step 1.1 proves the zero-dimensional case.
Depends on
- Smooth manifolds and their smooth charts
- Chart maps are diffeomorphisms onto Euclidean open sets
- A Euclidean bump for a compact set inside an open set
- Smooth maps paste over an open cover
- Identity maps and composites of smooth maps are smooth
- Heine-Borel in $\mathbb{R}^n$: with the Euclidean metric a subset of $\mathbb{R}^n$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line
- For a metric space with its metric topology, compactness in the topological sense is compactness in the metric sense, and the two notions of compact subset coincide
- A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism
- 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
Used by
- A nonzero-degree map to a connected manifold is surjective Corollary
- A finite coordinate-bump map embeds a compact manifold in some Euclidean space Lemma
- A manifold bump for a compact set inside an open set Lemma
- Every vector in a fibre extends to a compactly supported smooth section Lemma
- Finite chart localization gives choice-free integration and compact Stokes Lemma
- Trivial C¹ holonomy gives a saturated product neighbourhood Lemma
- Connection laws in directional form Proposition
- Integration is an isomorphism on top compactly supported de Rham cohomology Theorem
Dependency tree · two levels
69 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
- John M. Lee, Introduction to Smooth Manifolds (standard reference, not scraped)
- Will J. Merry, Differential Geometry (standard reference, not scraped)
- Nigel Hitchin, Differentiable Manifolds (standard reference, not scraped)