FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013)
FC08 — Lee, Introduction to Smooth Manifolds.
This chapter contains 10 definitions, 9 theorems, 10 propositions, 1 lemma, 2 corollaries, 8 examples and 1 convention.
Of the 41 statements checked against Lean, 4 are formalized somewhere and 37 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 37 | 90% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 4 | 10% | Mathlib states and proves it. |
| checked in total | 41 |
- Canonical source block: FC08 Lee, Chapter 4,
FC08-C04-U001–FC08-C04-U041, exactly 41 unique contiguous rows retrieved from FC08 — John M. Lee, Introduction to Smooth Manifolds throughagent-memory. - The chapter title is Submersions, Immersions, and Embeddings in Lee’s second edition. Search order followed the Sweep-II plan: project source first at
A=3b2239e161592472b34e02ad3b7da308f9ce7280, then pinned MathlibP=db584cd6d46c92f209a44c0f1c829460d327499d(Apache-2.0, Lean 4.33.0), current upstream MathlibH=5315eef9e4ffb98e0f89f278b765c50a149f66ca(Apache-2.0, Lean 4.34.0-rc2), then targeted current/indexed/external Lean searches and local project/reference probes. Noproject-existing,package-import, orreference-portC04 owner survived strict whole-row checking. - Every promoted Mathlib path exists at exact
P./tmp/fc08-c04-witness.leancompiled the strict form of Lee’s U021 Dirichlet bound fromexists_int_int_abs_mul_sub_leand checked the exact Kronecker-delta formula used for U012./tmp/fc08-c04-sphere.leancompiled U023’s smooth sphere inclusion, injective manifold derivative, topological embedding, and compactness ingredients. These witnesses are audit evidence only, not project source. - C04 has 4 pinned
mathlibrows and 37 datedunmatchedrows. Positive rows are: U006, U012, U021, U023. - The controlling semantic issue is explicit in pinned
Immersion.leanandSubmersion.lean: Mathlib defines immersions/submersions by local normal forms, while Lee C04 defines them by injectivity/surjectivity of the differential. AtP, both files say the finite-dimensional equivalence is future work. CurrentHaddsImmersionDiff.leanand proves local-normal-form immersion implies injectivemfderiv, plus that injectivity yields a split differential in finite dimensions, but it still does not prove the converse toIsImmersion; there is no parallel differential-submersion file/equivalence. Consequently none of U003–U005, U009, U015–U017, U022, U024, or U028–U033 is credited through an unproved bridge. - The manifold inverse/rank theorems are also genuinely absent from the checked interface.
LocalDiffeomorph.leanat bothPandHleaves “invertiblemfderivimplies local diffeomorphism” as TODO, so U007 cannot be inferred from the Banach-space inverse function theorem. No checked manifold constant-rank/rank theorem was found for U011–U014, and the boundary normal form U015 is likewise absent. - U006 is direct from
IsLocalDiffeomorphAt/IsLocalDiffeomorph: the witness is a smooth equivalence between open neighborhoods. U012 is Mathlib’s identity-matrix entry formulaMatrix.one_apply. U021 is a strict corollary of the stronger pinned Dirichlet bound and was compiled. U023 is a specialized existing formalization:Instances/Sphere.leanproves both smoothness and injectivity of the sphere inclusion derivative, while generic topology/compactness APIs supply the topological embedding and compact domain. - U008 is not promoted despite substantial local-diffeomorphism coverage: P has composition, local-homeomorphism/open-map consequences, diffeomorphisms as local diffeomorphisms, and bijective local diffeomorphisms as diffeomorphisms, but the complete seven-clause source bundle was not found. Similarly, U035–U041 are not inferred from topological covering APIs: Mathlib’s
IsCoveringMapis topological and explicitly allows nonsurjective coverings, while Lee’s smooth-covering predicate additionally requires smooth/diffeomorphic sheets and connected/surjective hypotheses. - Project-first search found only the specialized
LeanCategories/ForMathlib/QuotientManifold.lean, where a discrete-subgroup quotient is given a manifold structure using local sections of a quotient covering. It is useful adjacent evidence for U038 but is a proper specialization, not the general covering-space smooth-structure theorem. The project source remained unmodified. - Targeted indexed searches for Lean formalizations of the manifold rank theorem, smooth-submersion local sections/descent, smooth covering maps, and proper-local-diffeomorphism covering theorems found no compatible general owner beyond the checked Mathlib/topological ingredients. Current upstream was inspected by git object without changing the pinned worktree.
N=2026-09-07denotes a dated unmatched decision after the prescribed search layers. Strict whole-row semantics apply uniformly.
Definition/convention — rank of F at p to be the rank of the linear map d F
Suppose M and N are smooth manifolds with or without boundary. Given a smooth map F M N and a point \(p \in M ,\) ; we define the rank of F at p to be the rank of the linear map d \(F _ { p } \colon T _ { p } M \to T _ { F ( p ) } N\) ; it is the rank of the Jacobian matrix of F in any smooth chart, or the dimension of Im d \(F _ { p } \subseteq T _ { F ( p ) } N . \mathrm { I f }\) F has the same rank r at every point, we say that it has constant rank, and write set and p is an element of X.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib has LinearMap.rank, mfderiv, matrix/Jacobian infrastructure, and tangent spaces, but no checked manifold-map rank interface that packages rank of dF_p, chart-Jacobian invariance, image dimension, and the constant-rank predicate as this whole row. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Definition/convention — linear map
\(F = r .\) Because the rank of a linear map is never higher than the dimension of either its domain or its codomain (Exercise B.22), the rank of F at each point is bounded above by the minimum of dim M; dim N . If the rank of \(d F _ { p }\) is equal to this upper bound, we say that F has full rank at p, and if F has full rank everywhere, we say F has full rank.
Not formalized. none; no complete checked declaration under strict bundle semantics — Generic linear-map rank bounds are formalized, but the checked manifold API has no source-facing full-rank-at-a-point/full-rank-everywhere interface tied to U001, so the complete definition is not owned. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Definition/convention — smooth submersion
The most important constant-rank maps are those of full rank. \(\mathbf { A }\) smooth map \(F \colon M \to N\) is called a smooth submersion if its differential is surjective at each point (or equivalently, if rank \(F = \dim N )\) . It is called a smooth immersion if its differential is injective at each point (equivalently, rank d topological manifolds and pointed continuous maps \(\mathsf { D i f f } _ { * } \colon\) pointed smooth manifolds and pointed smooth maps We use the word class instead of \(s e t\) for the collections of objects and morphisms in a category because in some categories they are “too large” to be considered sets.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned IsImmersion and IsSubmersion are defined by local normal forms, not by injectivity/surjectivity of mfderiv; both files explicitly say the finite-dimensional equivalence is future work. Current H adds only the direction IsImmersion → injective mfderiv plus a differential-immersion predicate; it still lacks the converse and has no corresponding differential-submersion package. The combined Lee definition therefore has no checked owner. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Proposition 4.1
Proposition 4.1. Suppose \(F \colon M \to N\) is a smooth map and \(p \in M\) If d \(F _ { p }\) is surjective, then p has a neighborhood U such that \(F | _ { U }\) is a submersion. \(I f d F _ { p } i s\) injective, then p has a neighborhood U such that \(F | _ { U }\) is an immersi e” to be considered sets.
Not formalized. none; no complete checked declaration under strict bundle semantics — This proposition requires persistence of injectivity/surjectivity of one manifold derivative to a neighborhood in Lee’s derivative-based sense. P has no such theorem, and current H still lacks the converse from differential injectivity/surjectivity to the local-normal-form immersion/submersion predicates. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Example 4.2
Example 4.2 (Submersions and Immersions). (a) Suppose } , , M _ { k }$ are smooth manifolds. Then each of the projection maps $ smooth submersion. In particular, the projection \(\pi \colon \mathbb { R } ^ { n + k } \mathbb { R } ^ { n }\) onto the first n coordinates is a smooth submersion. (b) If \(\gamma \colon J \to M\) is a smooth curve in a smooth manifold M with or without bound-\(\operatorname { a r y } ,\) then is a smooth if \(\gamma ^ { \prime } ( t ) \neq 0\) for all \(t \in J\) (c) If M is a smooth manifold and its tangent bundle TM is given the smooth manifold structure described in Proposition 3.18, the projection \(T M \to M\) is a smooth submersion. To verify this, just note that with respect to any smooth local coordinates \(\left( x ^ { i } \right)\) on an open subset \(U \subseteq M\) and the corresponding natural coordinates \(( x ^ { i } , v ^ { i } )\) on \(\pi ^ { - 1 } ( U ) \subseteq T M\) Proposition 3.18), the coordinate representation of is \({ \widehat { \pi } } ( x , v ) = x\)
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has product projections, tangent-bundle projection infrastructure, smooth curves, and sphere/torus-adjacent APIs, but no checked declaration owns the complete four-part example, including the curve iff characterization and the explicit torus parametrization. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Definition/convention — local diffeomorphism
If M and N are smooth manifolds with or without boundary, a map \(F \colon M \to N\) is called a local diffeomorphism if every point \(p \in M\) has a neighborhood U such that F .U / is open in N and \(F | _ { U } \colon U \to F ( U )\) is a diffeomorphism. The next theorem is the key to the most important properties of local diffeomo ravariant functor from Diff to VecR defined by assigning to each smooth manifold M the vector space \(C ^ { \infty } ( M )\) , and to each smooth map \(F \colon M \to N\) the linear map \(F ^ { * } \colon C ^ { \infty } ( N ) \to C ^ { \infty } ( M )\) defined by \(F ^ { * } ( f ) = f \circ F\) The discussion in this chapter has given us some other important examples of functors.
Formalized. Mathlib/Geometry/Manifold/LocalDiffeomorph.lean::PartialDiffeomorph, IsLocalDiffeomorphAt, IsLocalDiffeomorph — IsLocalDiffeomorphAt says that near the point the map agrees on an open source with a PartialDiffeomorph; a PartialDiffeomorph is an equivalence between open source/target sets whose forward and inverse maps are C^n. Requiring this at every point is exactly Lee’s local-diffeomorphism definition, including openness of the image neighborhood.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Theorem 4.5
Theorem 4.5 (Inverse Function Theorem for Manifolds). Suppose M and N are smooth manifolds, and \(F \colon M \to N\) is a smooth map. If \(p \in M\) is a point such that d \(F _ { p }\) is invertible, then there are connected neighborhoods U0 of p and V0 of \(F ( p )\) such that \(F | _ { U _ { 0 } } \colon U _ { 0 } \to V _ { 0 }\) is a diffeom e other important examples of functors.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned and current LocalDiffeomorph.lean explicitly leave “invertible mfderiv implies local diffeomorphism” as TODO. Banach-space inverse-function theorems do not supply the missing manifold chart theorem, so Lee’s manifold inverse function theorem is unmatched. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Proposition 4.6
(Elementary Properties of Local Diffeomorphisms). (a) Every composition of local diffeomorphisms is a local diffeomorphism. (b) Every finite product of local diffeomorphisms between smooth manifolds is a local diffeomorphism. (c) Every local diffeomorphism is a local homeomorphism and an open map. (d) The restriction of a local diffeomorphism to an open submanifold with or without boundary is a local diffeomorphism. (e) Every diffeomorphism is a local diffeomorphism. (f) Every bijective local diffeomorphism is a diffeomorphism. (g) A map between smooth manifolds with or without boundary is a local diffeomorphism if and only if in a neighborhood of each point of its domain, it has a coordinate representation that is a local diffeomorphism.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned local-diffeomorphism APIs prove composition, local-homeomorphism/open-map consequences, diffeomorphism-to-local-diffeomorphism, and bijective-local-diffeomorphism-to-diffeomorphism. The complete seven-clause row additionally needs finite products, arbitrary open restrictions, and the coordinate characterization; no checked full bundle was found. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Proposition 4.8
Proposition 4.8. Suppose M and N are smooth manifolds (without boundary), and \(F \colon M \to N\) is a map. (a) F is a local diffeomorphism if and only if it is both a smooth immersion and a smooth submersion. (b) If dim M dim N and F is either a smooth immersion or a smooth submersion, then it is a local diffeomorphi omorphism.
Not formalized. none; no complete checked declaration under strict bundle semantics — Both clauses depend on the finite-dimensional equivalence between Lee’s differential injective/surjective definitions and Mathlib’s local-normal-form immersion/submersion predicates. That bridge is incomplete even at current H, and the inverse-function converse is also still a TODO. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Example 4.11
Example 4.11 (Local Diffeomorphisms). The map \(\varepsilon \colon \mathbb { R } \to \mathbb { S } ^ { 1 }\) defined in Example 2.13(b) is a local diffeomorphism because in a neighborhood of each point it has a coordinate representation of the form \(t \mapsto 2 \pi t + c\) , which is a local diffeomorphism. Similarly, the map \(\varepsilon ^ { n } \colon \mathbb { R } ^ { n } \to \mathbb { T } ^ { n }\) defined in Example 2.13(c) is a local diffeomorphism because it is a prod s discussion is the rank theorem, a corollary of the inverse function theorem.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib has the circle exponential as a smooth topological covering/local homeomorphism, but no checked smooth local-diffeomorphism theorem for Lee’s ε, nor the complete product statement for ε^n; the whole example is not promoted. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Theorem 4.12
Theorem 4.12 (Rank Theorem). Suppose M and N are smooth manifolds of dimensions m and n, respectively, and \(F \colon M \to N\) is a smooth map with constant rank r. For each \(p \in M\) there exist smooth charts \(( U , \varphi )\) for M centered at p and \(( V , \psi )\) for N centered at \(F ( p )\) such that \(F ( U ) \subseteq V\) in which F has a coordinate representation of the form \[ \widehat {F} \left(x ^ {1}, \dots , x ^ {r}, x ^ {r + 1}, \dots , x ^ {m}\right) = \left(x ^ {1}, \dots , x ^ {r}, 0, \dots , 0\right).\tag{4.1} \] In particular, if F is a smooth submersion, this becomes \[ \widehat {F} \left(x ^ {1}, \dots , x ^ {n}, x ^ {n + 1}, \dots , x ^ {m}\right) = \left(x ^ {1}, \dots , x ^ {n}\right),\tag{4.2} \] and if F is a smooth immersion, it is \[ \widehat {F} \left(x ^ {1}, \ldots , x ^ {m}\right) = \left(x ^ {1}, \ldots , x ^ {m}, 0, \ldots , 0\right).\tag{4.3} \] Proof. Because the theorem is local, after choosing smooth coordinates we can replace M and N by open subsets \(U \subseteq \mathbb { R } ^ { m }\)
Not formalized. none; no complete checked declaration under strict bundle semantics — No pinned/current/indexed Lean declaration proves the finite-dimensional manifold constant-rank normal form, and the immersion/submersion specializations cannot substitute for the missing general rank theorem. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Convention/notation — Kronecker delta
Here \(\delta^{i}_{j}\) denotes the Kronecker delta, defined for positive integers \(i\) and \(j\) by \[ \delta^{i}_{j} = \begin{cases} 1 & \text{if } i = j, \\ 0 & \text{if } i \neq j. \end{cases} \tag{4.4} \]
Formalized. Mathlib/Data/Matrix/Diagonal.lean::Matrix.one_apply, Matrix.one_apply_eq, Matrix.one_apply_ne — Mathlib represents the Kronecker delta as the entries of the identity matrix: Matrix.one_apply is exactly 1 when the two indices agree and 0 otherwise. The diagonal/off-diagonal corollaries give Lee’s two cases separately.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Corollary 4.13
Let \(M\) and \(N\) be smooth manifolds, let \(F \colon M \to N\) be a smooth map, and suppose \(M\) is connected. Then the following are equivalent: (a) for each \(p \in M\) there exist smooth charts containing \(p\) and \(F(p)\) in which the coordinate representation of \(F\) is linear; (b) \(F\) has constant rank.
Not formalized. none; no complete checked declaration under strict bundle semantics — This equivalence is a direct corollary of the rank theorem plus connectedness/locally constant rank. Since the checked sources do not own the required rank theorem or a complete equivalent statement, the row remains unmatched. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Theorem 4.14
Theorem 4.14 (Global Rank Theorem). Let M and N be smooth manifolds, and suppose F M N is a smooth map of constant rank.
Not formalized. none; no complete checked declaration under strict bundle semantics — The canonical extraction records Lee’s Global Rank Theorem heading and constant-rank hypothesis, but no checked pinned/current theorem with the corresponding global constant-rank conclusion was found. No incomplete source row is inferred from adjacent rank infrastructure. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Theorem 4.15
Theorem 4.15 (Local Immersion Theorem for Manifolds with Boundary). Suppose M is a smooth m-manifold with boundary, N is a smooth n-manifold, and \(F \colon M \to N\) M$ ; there exist a smooth boundary chart \(( U , \varphi )\) for M centered at p and a smooth coordinate chart \(( V , \psi )\) for N centered at \(F ( p )\) with \(F \subseteq V\) , in which F has the coordinate representation \[ \hat {F} \left(x ^ {1}, \dots , x ^ {m}\right) = \left(x ^ {1}, \dots , x ^ {m}, 0, \dots , 0\right).\tag{4.7} \] Proof. By choosing initial smooth charts for M and N , we may assume that M and N are open subsets of $
Not formalized. none; no complete checked declaration under strict bundle semantics — The checked manifold APIs do not contain Lee’s boundary immersion normal-form theorem. P’s local-normal-form IsImmersion is a different predicate from Lee’s derivative-injective hypothesis, and the required finite-dimensional/boundary bridge is absent. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Definition/convention — smooth embedding of M into N
One special kind of immersion is particularly important. If M and N are smooth manifolds with or without boundary, a smooth embedding of M into N is a smooth immersion \(F \colon M \to N\) that is also a topological embedding, i.e., a homeomorphism onto its image \(F ( M ) \subseteq N\) in the subspace topology. A smooth embedding is a map that is both a topological embedding and a smooth immersion, not just a topological embedding that happens to be smooth.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib/Geometry/Manifold/SmoothEmbedding.lean::IsSmoothEmbedding combines topological embedding with Mathlib’s local-normal-form IsImmersion. Because the checked sources do not prove equivalence of that immersion notion with Lee’s differential-injective definition, this apparently close structure is not a checked equivalent owner for Lee’s definition. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Example 4.17
Example 4.17 (Smooth Embeddings). (a) If M is a smooth manifold with or without boundary and M$ is an open submanifold, the inclusion map $ M$ is a smooth embedding. (b) If \(M _ \ldots , M _ { k }\) are smooth manifolds and \(p _ } \in M _ { i }\) are arbitrarily chosen points, each of the maps \(\iota _ { j } \colon \cdots \times M _ { k }\) given by \[ \iota_ {j} (q) = (p _ {1}, \dots , p _ {j - 1}, q, p _ {j + 1}, \dots , p _ {k}) \] is a smooth embedding. In particular, the inclusion map $ ^ { n + k }$ given by sending $ , x ^ { n } , 0 , , 0 )$ is a smooth embedding. (c) Problem 4-12 shows that the map $ ^ { 2 } ^ { ^ { } } { } ^ { 3 }$ of Example 4.2(d) descends to a smooth embedding of the torus $
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib proves open-submanifold inclusions and products for its IsSmoothEmbedding predicate, but the row also includes the explicit standard torus embedding, and the immersion predicate itself is not bridged to Lee’s derivative definition. The full three-part example is not owned. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Example 4.18
Example 4.18 (A Smooth Topological Embedding). The map \(\gamma \colon { \mathbb { R } } \to { \mathbb { R } } ^ { 2 }\) given by \(\gamma ( t ) = { \bigl ( } t ^ { 3 } , 0 { \bigr ) }\) is a smooth map and a topological embedding, but it is not a smooth embedding because \(\gamma ^ { \prime } ( 0 ) = 0\)
Not formalized. none; no complete checked declaration under strict bundle semantics — The generic calculus/topology library can analyze t ↦ (t^3,0), but no checked source declaration packages the complete example: smoothness, topological embedding, zero derivative at 0, and consequent failure of Lee-smooth-embedding. Reconstructing it from primitives would be new proof work rather than mapping an existing owner. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Example 4.19
Example 4.19 (The Figure-Eight Curve). Consider the curve \(\beta \colon ( - \pi , \pi ) \to { \mathbb { R } } ^ { 2 }\) defined by \[ \beta (t) = (\sin 2 t, \sin t). \] Its image is a set that looks like a figure-eight in the plane \(( \mathrm { F i g . ~ } 4 . 3 )\) ,sometimes called a lemniscate. (It is the locus of points \(( x , y )\) where \(x ^ { 2 } = 4 y ^ { 2 } \left( 1 - y ^ { 2 } \right)\) , as you can check.) It is easy to see that \(\beta\) is an injective smooth immersion because \(\beta ^ { \prime } ( t )\) never vanishes; but it is not a topological embedding, because its image is compact in the subspace topology, while its domain y \(V _ { 0 } =\) \(\left\{ ( v , w ) \in V : ( v , 0 ) \in \widetilde { U } _ { 0 } \right\}\) .
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Lean declaration formalizes this figure-eight parametrization with all of injectivity, immersion, its algebraic image description, and failure of topological embedding. Generic trigonometric/calculus ingredients are only partial evidence. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Example 4.20
(A Dense Curve on the Torus). Let \(\mathbb{T}^{2} = \mathbb{S}^{1} \times \mathbb{S}^{1} \subseteq \mathbb{C}^{2}\) be the torus and let \(\alpha\) be irrational. The map \(\gamma \colon \mathbb{R} \to \mathbb{T}^{2}\) given by \(\gamma(t) = (e^{2\pi i t}, e^{2\pi i \alpha t})\) is a smooth immersion, because \(\gamma'(t)\) never vanishes. Dirichlet’s approximation theorem gives, for every \(\varepsilon > 0\), integers \(n, m\) with \(|\alpha n - m| < \varepsilon\); so \(\gamma\) is not a homeomorphism onto its image, because \(\mathbb{Z}\) has no limit point in \(\mathbb{R}\). In fact \(\gamma(\mathbb{R})\) is dense in \(\mathbb{T}^{2}\).
Not formalized. none; no complete checked declaration under strict bundle semantics — Dirichlet approximation is formalized (U021), but no checked declaration packages the irrational torus curve as a smooth immersion with nonembedded dense image. The substantive density/nonembedding example is not inferred from the approximation ingredient. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Lemma 4.21
(Dirichlet’s Approximation Theorem). Given \(\alpha \in \mathbb{R}\) and any positive integer \(N\), there exist integers \(n, m\) with \(1 \leq n \leq N\) such that \(|n\alpha - m| < 1/N\).
Formalized. Mathlib/NumberTheory/DiophantineApproximation/Basic.lean::exists_int_int_abs_mul_sub_le — The pinned Dirichlet theorem is slightly stronger: for positive N it gives integers m,n with 0<n≤N and |n*α-m|≤1/(N+1). Since 1/(N+1)<1/N, this implies Lee’s strict bound. The exact specialization and inequality were compiled in the C04 audit witness.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition 4.22
Proposition 4.22. Suppose M and N are smooth manifolds with or without boundary, and F M N is an injective smooth immersion. If any of the following holds, then F is a smooth embedding. (a) \(F\) is an open or closed map. (b) \(F\) is a proper map. (c) \(M\) is compact. (d) \(M\) has empty boundary and \(\dim M = \dim N\).
Not formalized. none; no complete checked declaration under strict bundle semantics — Topology APIs cover several ingredients for cases (a)–(c), but the row is a four-case theorem about Lee’s derivative-defined injective immersion. Case (d) needs the missing equal-dimension inverse-function/local-diffeomorphism bridge, so no complete route survives whole-row checking. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Example 4.23
Let \(\iota \colon \mathbb{S}^{n} \hookrightarrow \mathbb{R}^{n+1}\) be the inclusion map. Example 2.13(d) showed \(\iota\) is smooth by computing its coordinate representation in graph coordinates; the same coordinates show its differential is injective at each point, so it is an injective smooth immersion. Since \(\mathbb{S}^{n}\) is compact, \(\iota\) is a smooth embedding by Proposition 4.22.
Formalized. Mathlib/Geometry/Manifold/Instances/Sphere.lean::contMDiff_coe_sphere, mfderiv_coe_sphere_injective; Mathlib/Topology/Constructions.lean::Topology.IsEmbedding.subtypeVal; Mathlib/Topology/MetricSpace/ProperSpace.lean::Metric.isCompact_sphere; Mathlib/Analysis/Normed/Module/FiniteDimension.lean::FiniteDimensional.proper — For the unit sphere in a finite-dimensional real inner-product space, the pinned sphere API proves the inclusion smooth and its manifold derivative injective at every point. Subtype coercion is a topological embedding, and finite-dimensional normed spaces are proper, so the unit sphere is compact. These declarations jointly realize Lee’s sphere-inclusion smooth-embedding example; the assembly compiled at P.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Theorem 4.25
Theorem 4.25 (Local Embedding Theorem). Suppose M and N are smooth manifolds with or without boundary, and F M N is a smooth map. Then F is a smooth immersion if and only if every point in M has a neighborhood \(U \subseteq M\) such that \(F | _ { U } \colon U \to N\) is a smooth embeddi ubstitute for the rank theorem.
Not formalized. none; no complete checked declaration under strict bundle semantics — The local embedding theorem is equivalent to the local normal form for derivative-defined immersions. The checked Mathlib immersion predicate is itself defined using such a normal form, but the finite-dimensional bridge from Lee’s injective derivative is not proved, so using that definition here would be circular/unbridged. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Definition/convention — topological immersion
Theorem 4.25 points to a notion of immersion for arbitrary topological spaces: for topological spaces \(X\) and \(Y\), a continuous map \(F \colon X \to Y\) is a topological immersion if every point of \(X\) has a neighborhood \(U\) such that \(F|_{U}\) is a topological embedding. Every smooth immersion is a topological immersion, but, as with embeddings, a topological immersion that happens to be smooth need not be a smooth immersion.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked named predicate owns Lee’s generic “topological immersion” definition (continuous and locally a topological embedding) together with the smooth-immersion implication. Local-homeomorphism/embedding APIs are adjacent but not this interface. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Definition/convention — source terminology/construction
Submersions One of the most important applications of the rank theorem is to vastly expand our understanding of the properties of submersions. ! N is any continuous map, a section of is a continuous right inverse for , i.e., a continuous map \(\sigma \colon N \to M\) \(\pi \circ \sigma = \operatorname { I d } _ { N } \colon\) \[ \begin{array}{c} M \\ \pi \Big \downarrow \\ N. \end{array} \sigma \]
Not formalized. none; no complete checked declaration under strict bundle semantics — Continuous and Function.RightInverse exactly express the two ingredients of a section, but no checked source-facing section interface for arbitrary continuous maps packages Lee’s definition; strict semantics do not promote raw ingredients as a terminology-only row. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Definition/convention — source terminology/construction
A local section of is a continuous map \(\sigma \colon U \to M\) defined on some open subset \(U \subseteq N\) and satisfying the analogous relation \(\sigma = \operatorname { I d } _ { U }\) . Many of the important properties of smooth submersions follow from the fact that they admit an abundance of smooth } _ { ^ {n - m}}) (_ {0} (x), 0) = (x, 0).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked generic local-section object packages an open domain, continuity, and the right-inverse equation in Lee’s sense. The local-homeomorphism library constructs/uses continuous local sections in special contexts only. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Theorem 4.26
local sections. Theorem 4.26 (Local Section Theorem). Suppose M and N are smooth manifolds and \(\pi \colon M \to N\) is a smooth map. Then is a smooth submersion if and only if every point of M is in the image of a smooth local section satisfy the desired conditions.
Not formalized. none; no complete checked declaration under strict bundle semantics — The local-section characterization of derivative-defined smooth submersions is absent. P’s IsSubmersion is defined directly by local projection normal forms but has no theorem identifying it with Lee’s surjective-derivative predicate or with this exact image-of-local-section characterization. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Definition/convention — topological submersion
If \(\pi \colon X \to Y\) is a continuous map, \(\pi\) is a topological submersion if every point of \(X\) lies in the image of a continuous local section of \(\pi\). Every smooth submersion is a topological submersion.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked generic “topological submersion” predicate is defined by abundance of continuous local sections, and the claimed smooth-submersion implication additionally depends on the missing U028/derivative bridge. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Proposition 4.28
Proposition 4.28 (Properties of Smooth Submersions). Let M and N be smooth manifolds, and suppose \(\pi \colon M \to N\) is a smooth submersion. Then is an open map, and if it is surjective it is a quotient map.
Not formalized. none; no complete checked declaration under strict bundle semantics — Generic topology proves that open surjections are quotient maps, but the checked manifold API does not prove that every Lee-smooth submersion (surjective differential everywhere) is open: the needed derivative-to-local-normal-form theorem is missing. Therefore the two-clause row is not promoted. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Theorem 4.29
(Characteristic Property of Surjective Smooth Submersions). Suppose \(M\) and \(N\) are smooth manifolds and \(\pi \colon M \to N\) is a surjective smooth submersion. For any smooth manifold \(P\) with or without boundary, a map \(F \colon N \to P\) is smooth if and only if \(F \circ \pi\) is smooth.
Not formalized. none; no complete checked declaration under strict bundle semantics — The characteristic smoothness descent theorem along a surjective derivative-defined submersion is not in the checked sources. Ordinary composition proves only the forward direction; the reverse direction is precisely the missing local-section/submersion descent result. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Theorem 4.30
Theorem 4.30 (Passing Smoothly to the Quotient). Suppose M and N are smooth manifolds and \(\pi \colon M \to N\) is a surjective smooth submersion. If P is a smooth manifold with or without boundary and \(F \colon M \to P\) is a smooth map that is constant on the fibers of , then there exists a unique smooth map \({ \widetilde { F } } \colon N \to { \overline { { P } } }\) such that \({ \widetilde { F } } \circ \pi = F\) Proof. Because a surjective smooth submersion admits local sections through every point, this follows from the characteristic property.
Not formalized. none; no complete checked declaration under strict bundle semantics — Set-theoretic quotient factorization from a fiber-constant map is generic, but smoothness of the descended map requires U031/local sections. No checked declaration supplies the complete unique smooth factorization. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Theorem 4.31
uniqueness result. Theorem 4.31 (Uniqueness of Smooth Quotients). Suppose that M; \(N _ { 1 }\) , and \(N _ { 2 }\) are smooth manifolds, and \(\pi _ { 1 } \colon M \to N _ { 1 }\) and \(\pi _ { 2 } \colon M \to N _ { 2 }\) are surjective smooth submersions that are constant on each other’s fibers. Then there exists a unique diffeomorphism \(F \colon N _ { 1 } \to N _ { 2 }\) such that F \(\pi _ { 1 } = \pi _ { 2 }\) Exercise
Not formalized. none; no complete checked declaration under strict bundle semantics — The unique diffeomorphism between two smooth quotient targets is a consequence of two instances of U032 plus inverse uniqueness. Since the required smooth quotient descent is absent, no complete checked owner was found. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Definition/convention — smooth covering map
In the context of smooth manifolds, it is useful to introduce a slightly more restrictive type of covering map. If E and M are connected smooth manifolds with or without boundary, a map \(\pi \colon E \to M\) is called a smooth covering map if is smooth and surjective, and each point in M has a neighborhood U such that each component of \(\pi ^ { - 1 } ( U )\) is mapped diffeomorphically onto U by . In this context we also say that U is evenly covered. The space M is called the base of the covering, and E is called a covering manifold of M . If E is simply connected, it is called the universal covering manifold an open or closed map.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has IsCoveringMap for topological coverings and IsLocalDiffeomorph for smooth local equivalences, but no checked bundled smooth-covering-map predicate matching Lee’s connected/surjective/diffeomorphic-sheet definition (Mathlib topological coverings are explicitly allowed to be nonsurjective). Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Proposition 4.33
Proposition 4.33 (Properties of Smooth Coverings). (a) Every smooth covering map is a local diffeomorphism, a smooth submersion, an open map, and a quotient map. (b) An injective smooth covering map is a diffeomorphism. (c) A topological covering map is a smooth covering map if and only if it is a local diffeomorphism.
Not formalized. none; no complete checked declaration under strict bundle semantics — Topological covering maps are local homeomorphisms and local diffeomorphisms have open-map/homeomorphism APIs, but there is no bundled smooth-covering interface and no checked local-diffeomorphism-to-Lee-submersion bridge. The complete three-part properties theorem is therefore unmatched. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Example 4.35
(Smooth Covering Maps). The map ε : ℝ → mathbb S ^1 defined in Example 2.13(b) is a topological covering map and a local diffeomorphism (see also Example 4.11), so it is a smooth covering map; similarly \(\varepsilon^{n} \colon \mathbb{R}^{n} \to \mathbb{T}^{n}\) of Example 2.13(c) is a smooth covering map.
Not formalized. none; no complete checked declaration under strict bundle semantics — Circle.isCoveringMap_exp proves the circle exponential is a topological covering, isLocalHomeomorph_circleExp gives its local-homeomorphism property, and contMDiff_circleExp proves smoothness. No checked theorem upgrades this specific map to IsLocalDiffeomorph, and the canonical row is truncated after those opening claims, so no full-row route is promoted. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Proposition 4.36
(Local Section Theorem for Smooth Covering Maps). Suppose \(E\) and \(M\) are smooth manifolds with or without boundary and \(\pi \colon E \to M\) is a smooth covering map. Given any evenly covered open subset \(U \subseteq M\), any \(q \in U\), and any \(p\) in the fiber of \(\pi\) over \(q\), there is a unique smooth local section \(\sigma \colon U \to E\) with \(\sigma(q) = p\).
Not formalized. none; no complete checked declaration under strict bundle semantics — The topology library provides local inverses/sections for local homeomorphisms, but no checked theorem gives Lee’s unique smooth section over an arbitrary evenly covered open set through a specified fiber point. The smoothness upgrade is not packaged. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Proposition 4.40
Proposition 4.40 (Covering Spaces of Smooth Manifolds). Suppose M is a connected smooth n-manifold, and \(\pi \colon E \to M\) is a topological covering map. Then E is a topological n-manifold, and has a unique smooth structure such that is a smooth covering 2852fa14845aa31e7c3642f7b38d1276917718c1b81900.jpg) Proof.
Not formalized. none; no complete checked declaration under strict bundle semantics — IsLocalHomeomorph.chartedSpace transports a charted-space structure along a surjective local homeomorphism, and project-local quotient work uses this in a special discrete-subgroup case. No checked theorem supplies the general unique smooth structure on an arbitrary topological covering of a smooth manifold. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Proposition 4.41
Proposition 4.41 (Covering Spaces of Smooth Manifolds with Boundary). Suppose M is a connected smooth n-manifold with boundary, and \(\pi \colon E \to M\) is a topological covering map. Then E is a topological n-manifold with boundary such that \(\partial E = \pi ^ { - 1 } ( \partial M )\) , and it has a unique smooth structure such that is a smooth coverin 852852fa14845aa31e7c3642f7b38d1276917718c1b81900.jpg) Proof.
Not formalized. none; no complete checked declaration under strict bundle semantics — The checked covering/manifold APIs do not construct the general boundary manifold structure on the covering space, prove ∂E = π⁻¹(∂M), and establish uniqueness of the smooth structure as one theorem. Partial interior/boundary and covering ingredients do not own the bundle. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Corollary 4.43
Corollary 4.43 (Existence of a Universal Covering Manifold). If M is a connected smooth manifold, there exists a simply connected smooth manifold M , called the universal covering manifold of M , and a smooth covering \(\widetilde { M } \to M\) The universal covering manifold is unique in the following sense: if \({ \widetilde { M } } ^ { \prime }\) is any other simply connected smooth manifold that admits a smooth covering ^ { } $ M; then there exists a diffeomorphism ˚ $
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked general universal-cover existence/uniqueness theorem for connected smooth manifolds was found; topology searches exposed covering-space infrastructure but no universal-cover construction with the stated simply-connected smooth uniqueness. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.
Proposition 4.46
Proposition 4.46. Suppose E and M are nonempty connected smooth manifolds with or without boundary. \(I f \pi \colon E \to M\) is a proper local diffeomorphism, then is a smooth covering smooth map \({ \widetilde { F } } \colon N \to { \overline { { P } } }\) such that \({ \widetilde { F } } \circ \pi = F\) Proof.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned topology proves that a closed local homeomorphism is a covering map and proper maps are closed; local diffeomorphisms are local homeomorphisms/open maps. However Lee’s conclusion is a surjective smooth covering map between connected manifolds, an interface not bundled in the checked sources, so assembling these topological ingredients would still require the missing smooth-covering bridge. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unbridged equivalent notions, isolated examples/ingredients, and reconstruction of the substantive source theorem.