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.
Diffeomorphisms and local diffeomorphisms of manifolds
Definition
Let and be smooth manifolds. A diffeomorphism from to is a bijective smooth map whose inverse is smooth. Since a bijective smooth map and its smooth inverse are both continuous (Smooth maps are continuous), every diffeomorphism is a homeomorphism, but the converse fails. The manifolds and are diffeomorphic, written , when a diffeomorphism exists.
Let be a smooth map. Then is a local diffeomorphism when every has an open neighbourhood such that is open in and the corestriction is a diffeomorphism onto the open submanifold (An open subset of a smooth manifold has a canonical restricted smooth structure).
Remarks
-
Smoothness of the inverse is not automatic. A bijective smooth map need not be a diffeomorphism, and this is exactly why the definition demands smoothness of outright: the map on is smooth and bijective, but is not differentiable at .
-
A diffeomorphism is a local diffeomorphism. Taking at every point exhibits a diffeomorphism as a local diffeomorphism; no local inverse other than the global inverse is needed.