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.
and smooth maps between smooth manifolds
Definition
Let and be smooth manifolds, let be a map, let and let , where . For and an open set , a map is of class as follows. When , every such map is declared . When , each component with must be in the sense of maps and multi-index derivative notation in Euclidean space; when this component condition is vacuous. Suppose is continuous at . Then is of class at when there are smooth charts of at and of at with such that the coordinate representative
(The coordinate representation of a map between manifolds) is of class on a neighbourhood of in this componentwise Euclidean sense. By Chart independence of smoothness ↗, this condition is independent of the chosen charts: if one such representative is , then every one is, so "some charts" may be read as "any charts". A map is on an open set when it is continuous on and at every point of . A map that is for every finite — equivalently — is called smooth; the term map between smooth manifolds is reserved for the case where is continuous and the representative condition holds at every point of .
Remarks
-
Continuity is part of the hypothesis, not a consequence, at this point. The representative is only a map between open Euclidean sets when is continuous, as The coordinate representation of a map between manifolds records; that Smooth maps are continuous later derives continuity from the representative condition does not change the definition.
-
The choice of charts is discharged. The well-definedness obligation — that testing one chart pair agrees with testing every chart pair — is discharged by Chart independence of smoothness ↗, which is why that lemma is named in
justified_byrather thandeps.
Depends on
Used by
- Diffeomorphisms and local diffeomorphisms of manifolds Definition
- A bijective smooth map need not be a diffeomorphism False statement
- Chart independence of Cʳ smoothness Lemma
- A map from a disjoint union is smooth iff each restriction is smooth Proposition
- A map into a product is smooth iff its components are smooth Proposition
- Chart maps are diffeomorphisms onto Euclidean open sets Proposition
- Identity maps and composites of smooth maps are smooth Proposition
- Smooth maps are continuous Proposition
- Smoothness is local on the source Proposition
Dependency tree · two levels
11 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
- Nigel Hitchin, Differentiable Manifolds, §2.4 (standard reference, not scraped)
- Rob van der Vorst, Introduction to differentiable manifolds, §2 (standard reference, not scraped)