FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013)

FC08 — Lee, Introduction to Smooth Manifolds.

This chapter contains 20 definitions, 1 theorem, 7 propositions, 6 lemmas, 3 corollaries, 11 examples, 2 constructions and 5 conventions.

Of the 55 statements checked against Lean, 18 are formalized somewhere and 37 are not.

Status	Statements	Share	What it means
not formalized	37	67%	A documented search found no Lean statement of it anywhere.
in Mathlib	18	33%	Mathlib states and proves it.
checked in total	55

Which versions of Lean and Mathlib were searched

Canonical source block: FC08 Lee, Chapter 10, FC08-C10-U001–FC08-C10-U055, exactly 55 unique contiguous rows retrieved from FC08 — John M. Lee, Introduction to Smooth Manifolds through agent-memory.
Search order followed the Sweep-II plan: project source first at A=3b2239e161592472b34e02ad3b7da308f9ce7280, pinned Mathlib P=db584cd6d46c92f209a44c0f1c829460d327499d (Apache-2.0, Lean 4.33.0), current upstream Mathlib H=5315eef9e4ffb98e0f89f278b765c50a149f66ca (Apache-2.0, Lean 4.34.0-rc2), then targeted indexed/external Lean searches. No project-existing, package-import, or reference-port C10 owner survived strict whole-row checking.
C10 has 18 pinned mathlib rows and 37 dated unmatched rows. Positive rows are: U001, U002, U004, U006, U009, U010, U012, U014, U015, U016, U017, U020, U021, U025, U026, U027, U031, U052.
Mathlib’s basic bundle representation is equivalent to Lee’s after passing between a dependent family E : B → Type* and its sigma-type Bundle.TotalSpace F E. FiberBundle supplies local product trivializations, VectorBundle supplies fiberwise linearity, and ContMDiffVectorBundle supplies smooth transition functions. At the smooth level Mathlib proves the total space is a manifold, the projection is smooth, and atlas trivializations are smooth in both directions. These facts justify U001/U002 without reconstructing a new bundle formalism.
The transition-function and Whitney-sum rows have direct owners. Trivialization.coordChangeL is invertible on overlaps and satisfies the exact change-of-trivialization formula; contMDiffOn_coordChangeL supplies smoothness. Bundle.Prod is the fiberwise direct sum and coordChangeL_prod gives the product/block transition map. Thus U009/U010/U012 are promoted at P.
The section rows use the dependent-fiber presentation directly. A rough section is a dependent function s : ∀ p, E p; its total-space lift lies over the identity definitionally. FiberBundle.continuousAt_section/continuousWithinAt_section characterize continuous sections, while ContMDiffSection bundles smooth global sections. /tmp/fc08-c10-witness.lean compiled the projection identity and the continuity equivalence at P. U014–U017 and U020–U021 are promoted accordingly; U018 remains unmatched because no dependent-section support API was found.
The local-frame API is strong but intentionally asymmetric. Trivialization.localFrame and isLocalFrameOn_localFrame_baseSet directly own the frame induced by a trivialization and give U025–U027; IsLocalFrameOn.coeff owns U031. However LocalFrame.lean explicitly states that a fully frame-intrinsic converse for smoothness is still future work, and no arbitrary-frame-to-trivialization construction was found at P or H. Therefore U023/U024/U028–U030/U032 are not inferred from the one-way infrastructure.
U011 is deliberately unmatched despite VectorPrebundle/VectorBundleCore: those constructors produce the topology and smooth vector-bundle structure from compatible coordinate-change data, but no checked theorem supplies Lee’s full uniqueness of both topology and smooth structure. Strict whole-row semantics exclude the construction-only subset.
U008/U013/U019/U033/U039 and tangent-dependent portions of later examples inherit the promoted C03 boundary: Mathlib’s mature tangent bundle uses standard TangentSpace, while Lee’s tangent vectors in this source were introduced as point derivations; no checked PointDerivation ≃ TangentSpace bridge exists at P or H. Submanifold-dependent portions also inherit C05’s absence of a general embedded/immersed submanifold package.
The largest C10 gap is bundle maps/subbundles. Exact searches at P and H found no BundleHom/VectorBundleHom structure, no bundle-isomorphism structure of Lee’s form, and no Subbundle/VectorSubbundle abstraction. Consequently U034–U051 remain unmatched rather than being reconstructed from total-space maps, fiberwise linear maps, kernels/ranges, and Riemannian ingredients.
General smooth fiber bundles are also not bundled at P/H. FiberBundle exactly owns U052, but there is no checked general ContMDiffFiberBundle/smooth-fiber-bundle predicate for arbitrary model fibers; smooth vector bundles are only a special case. U053–U055 therefore remain unmatched where their whole statements require the missing smooth/general or explicit Möbius components.
Targeted indexed searches did not surface a compatible external Lean owner for the missing bundle-homomorphism, subbundle, arbitrary-frame converse, or general smooth-fiber-bundle rows. External results were used only as secondary evidence; route decisions are grounded in the exact checked revisions above.
N=2026-09-07 marks dated unmatched decisions after the prescribed search layers. Strict whole-row semantics apply uniformly.

Construction/definition — local trivialization of E

FC08-C10-U001 · Ch. 10, § Vector Bundles; source L7195 · in Mathlib

Let $M$ be a topological space. A real vector bundle of rank $k$ over $M$ is a topological space $E$ with a surjective continuous map $\pi \colon E \to M$ such that: (i) each fiber $E_{p} = \pi^{-1}(p)$ carries the structure of a $k$-dimensional real vector space; (ii) each $p \in M$ has a neighborhood $U$ and a homeomorphism $\Phi \colon \pi^{-1}(U) \to U \times \mathbb{R}^{k}$, a local trivialization of $E$ over $U$, with $\pi_{U} \circ \Phi = \pi$, where $\pi_{U} \colon U \times \mathbb{R}^{k} \to U$ is the projection, and with $\Phi|_{E_{q}}$ a vector space isomorphism from $E_{q}$ to $\{q\} \times \mathbb{R}^{k} \cong \mathbb{R}^{k}$ for each $q \in U$.

Formalized. Mathlib/Topology/FiberBundle/Basic.lean::FiberBundle, Bundle.Trivialization; Mathlib/Topology/VectorBundle/Basic.lean::VectorBundle, Bundle.Trivialization.linearEquivAt — A FiberBundle F E supplies local trivializations of the sigma-type total space over the base, and VectorBundle ℝ F E requires those trivializations to be fiberwise linear. Specializing the fixed model fiber F to a k-dimensional real normed space gives Lee’s rank-k vector-bundle definition; linearEquivAt is the fiber isomorphism.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Definition/convention — smooth vector bundle

FC08-C10-U002 · Ch. 10, § Vector Bundles; source L7208 · in Mathlib

If M and E are smooth manifolds with or without boundary, π is a smooth map, and the local trivializations can be chosen to be diffeomorphisms, then E is called a smooth vector bundle. In this case, we call any local trivialization that is a diffeomorphism onto its image a smooth local trivialization.

Formalized. Mathlib/Geometry/Manifold/VectorBundle/Basic.lean::ContMDiffVectorBundle, Bundle.TotalSpace.isManifold, contMDiff_proj, Bundle.Trivialization.contMDiffOn, Bundle.Trivialization.contMDiffOn_symm — ContMDiffVectorBundle ∞ F E I requires smooth transition maps. Mathlib then makes the total space a smooth manifold, proves the projection smooth, and proves each atlas trivialization and its inverse smooth on their domains. This is Lee’s smooth-vector-bundle condition in the dependent-fiber presentation.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Convention/notation — a (real) line bundle

FC08-C10-U003 · Ch. 10, § Vector Bundles; source L7210 · not formalized

A rank-1 vector bundle is often called a (real) line bundle. Complex vector bundles are defined similarly, with “real vector space” replaced by “complex vector space” and $\mathbb { R } ^ { k }$ replaced by $\mathbb { C } ^ { k }$ in the definition. We have no need to treat complex vector bundles in this book, so all of our vector bundles are understood without further comment e number of specialized techniques that have been developed to solve partial differential equations is staggering.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib vector bundles are generic over the scalar field and can certainly be specialized to rank-one real bundles or complex bundles, but no checked interface owns Lee’s combined source convention “line bundle / complex analogue / all subsequent unqualified bundles are real.” The generic class is adjacent rather than a whole-row formalization. Strict whole-row semantics reject proper subsets, unproved converse directions, missing uniqueness clauses, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.

Convention/notation — total space of the bundle

FC08-C10-U004 · Ch. 10, § Vector Bundles; source L7212 · in Mathlib

The space E is called the total space of the bundle, M is called its base, and is its projection. Depending on what we wish to emphasize, we sometimes omit some of the ingredients from the notation, and write “E is a vector bundle over M;” ${ \mathrm { o r } } \ ^ { \cdots } E \to M$ is a vector bundle,” or $^ { * } \pi \colon E \to M$ is a vecto o ordinary differential equations by means of the theory of flows, and thus can be solved using only ODEs and a little differential-geometric insight but no specialized PDE theory.

Formalized. Mathlib/Data/Bundle.lean::Bundle.TotalSpace, Bundle.TotalSpace.proj, Bundle.TotalSpace.mk' — Bundle.TotalSpace F E is Mathlib’s total space, the base is the index type B, and Bundle.TotalSpace.proj is the canonical projection. This exactly realizes Lee’s terminology/notation row.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Definition/convention — global trivialization of E )

FC08-C10-U005 · Ch. 10, § Vector Bundles; source L7216 · not formalized

If there exists a local trivialization of E over all of M (called a global trivialization of E ), then E is said to be a trivial bundle. In this case, E itself is homeomorphic to the product space $M \times \mathbb { R } ^ { k }$ . If $E \to M$ is a smooth bundle that admits a smooth global trivialization, then we say that E is smoothly trivial. In this case E is diffeomorphic to $M \times \mathbb { R } ^ { k }$ , not just homeomorphic. For brevity, when we say that a smooth bundle is trivial, we always understand this to mean smoothly trivial, not just trivial in the topological sense.

Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib has IsHomeomorphicTrivialFiberBundle for the topological product condition and the canonical Bundle.Trivial construction, but no corresponding general smooth-triviality predicate/equivalence for an arbitrary smooth bundle. Lee’s row includes both topological triviality and smooth triviality/diffeomorphism, so the available topological half is insufficient. Strict whole-row semantics reject proper subsets, unproved converse directions, missing uniqueness clauses, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.

Example 10.2

FC08-C10-U006 · Ch. 10, § Vector Bundles; source L7221 · in Mathlib

Example 10.2 (Product Bundles). One particularly simple example of a rankk vector bundle over any space M is the product space $E = M \times \mathbb { R } ^ { k }$ with $\pi = \pi _ { 1 } \colon M \times \mathbb { R } ^ { k } \to M$ as its projection. Any such bundle, called a product bundle, is trivial (with the identity map as a global trivialization). If M is a smooth manifold with or without boundary, then $M \times \mathbb { R } ^ { k }$ is smoothly solved by any smooth function u that depends on y alone—so in order to get a unique solution one generally stipulates that the solution should satisfy some extra conditions.

Formalized. Mathlib/Topology/FiberBundle/Constructions.lean::Bundle.Trivial.homeomorphProd, Bundle.Trivial.trivialization; Mathlib/Topology/VectorBundle/Constructions.lean::Bundle.Trivial.vectorBundle; Mathlib/Geometry/Manifold/VectorBundle/Basic.lean::Bundle.Trivial.contMDiffVectorBundle — Bundle.Trivial B F is the product bundle, with total space homeomorphic to B × F and a global trivialization. It carries the vector-bundle and C^n vector-bundle instances, giving the smooth product-bundle example on a smooth base.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Example 10.3

FC08-C10-U007 · Ch. 10, § Vector Bundles; source L7225 · not formalized

Example 10.3 (The Möbius Bundle). Define an equivalence relation on $\mathbb { R } ^ { 2 }$ by declaring that $( x , y ) ( x ^ { } , y ^ { } ) $ if and only if $( x ^ { \prime } , y ^ { \prime } ) = \left( x + n , ( - 1 ) ^ { n } y \right)$ for some $n \in \mathbb { Z }$ . Let $E = \mathbb { R } ^ { 2 } / { \sim }$ denote the quotient space, and let $\dot { q } \colon \mathbb { R } ^ { 2 } \to E$ be the quotient map. To visualize $E$ , let S denote the strip $[ 0 , 1 ] \times \mathbb { R } \subseteq \mathbb { R } ^ { 2 }$

Not formalized. none; no complete checked declaration under strict bundle semantics — No checked P/H or project declaration packages Lee’s Möbius-bundle quotient construction with its vector-bundle structure. Generic quotient and bundle constructors would require reconstructing this explicit example. Strict whole-row semantics reject proper subsets, unproved converse directions, missing uniqueness clauses, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.

Proposition 10.4

FC08-C10-U008 · Ch. 10, § Vector Bundles; source L7239 · after FC08-C03-U031 · not formalized

Problem 21-9 suggests a more powerful approach.) The most important examples of vector bundles are tangent bundles. Proposition 10.4 (The Tangent Bundle as a Vector Bundle). Let M be a smooth n-manifold with or without boundary, and let TM be its tangent bundle. With its standard projection map, its natural vector space structure on each fiber, and the topology and smooth structure constructed in Proposition 3.18, TM is a smooth vector bundle of rank n over M . P

Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib proves that its standard TangentSpace tangent bundle is a smooth vector bundle, but FC08 C03 established that Lee’s tangent vectors in this source are the point-derivation model and no checked PointDerivation ≃ TangentSpace bridge exists at P or H. The standard-tangent result therefore cannot own Lee’s tangent-bundle row. Strict whole-row semantics reject proper subsets, unproved converse directions, missing uniqueness clauses, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.

Lemma 10.5

FC08-C10-U009 · Ch. 10, § Vector Bundles; source L7257 · in Mathlib

Lemma 10.5. Let E M be a smooth vector bundle of rank k over M . Suppose ˚ $\pi ^ { - 1 } ( U ) \to U \times \mathbb { R } ^ { k }$ and $\psi \colon \pi ^ { - 1 } ( V ) \to V \times \mathbb { R } ^ { k }$ are two smooth local trivializations of E with $U \cap V \neq \emptyset$ . There exists a smooth map $\tau \colon U \cap V \to \mathbf { G L } ( k , \mathbb { R } )$ 1 such that the composition $\dot { \phi \circ \psi ^ { - 1 } } \colon ( U \cap V ) \times \mathbb { R } ^ { k } \to ( U \cap V ) \times \mathbb { R } ^ { k }$ has the form \[ \varPhi \circ \Psi^ {- 1} (p, v) = \bigl (p, \tau (p) v \bigr), \] where $\tau ( p )$ v denotes the usual action hat {u} (t, p) = e ^ {- B (t, p)} ((p) + _ {0} ^ {t} (, p) e ^ {B (, p)} d ), \ B (, p) = _ {0} ^ {} (, p) d .

Formalized. Mathlib/Topology/VectorBundle/Basic.lean::Bundle.Trivialization.coordChangeL, Bundle.Trivialization.coe_coordChangeL, Bundle.Trivialization.apply_symm_apply_eq_coordChangeL; Mathlib/Geometry/Manifold/VectorBundle/Basic.lean::Bundle.Trivialization.contMDiffOn_coordChangeL — On the overlap of two bundle trivializations, coordChangeL is the fiberwise linear equivalence obtained by composing one trivialization with the inverse of the other; apply_symm_apply_eq_coordChangeL gives Lee’s (p,v) ↦ (p,τ(p)v) formula. For a smooth vector bundle contMDiffOn_coordChangeL proves smooth dependence on the base. In finite-dimensional real coordinates this is exactly the GL(k,ℝ) transition map.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Definition/convention — transition function

FC08-C10-U010 · Ch. 10, § Vector Bundles; source L7277 · in Mathlib

The smooth map $\tau \colon U \cap V \to \mathrm{GL}(k,\mathbb{R})$ given by this lemma is called the transition function between the local trivializations $\Phi$ and $\Psi$ — one of the few places in smooth manifold theory where "function" is used with a codomain other than $\mathbb{R}$ or $\mathbb{R}^{k}$. For example, if $\Phi$ and $\Psi$ are the local trivializations of $TM$ associated with two smooth charts, then (3.12) shows the transition function between them is the Jacobian matrix of the coordinate transition map.

Formalized. Mathlib/Topology/VectorBundle/Basic.lean::Bundle.Trivialization.coordChangeL, Bundle.Trivialization.symm_coordChangeL; Mathlib/Geometry/Manifold/VectorBundle/Basic.lean::Bundle.Trivialization.contMDiffOn_coordChangeL — coordChangeL is precisely the transition function between two linear trivializations; on overlaps it is invertible with inverse the reversed coordinate change, and is smooth for a smooth vector bundle. The codomain GL(k,ℝ) is represented as an invertible continuous linear endomorphism of the fixed k-dimensional model fiber.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Lemma 10.6

FC08-C10-U011 · Ch. 10, § Vector Bundles; source L7281 · not formalized

Lemma 10.6 (Vector Bundle Chart Lemma). Let M be a smooth manifold with or without boundary, and suppose that for each $p \in M$ we are given a real vector space $E _ { p }$ of some fixed dimension k. Let $\begin{array} { r } { E = \coprod _ { p \in M } E _ { p } } \end{array}$ , and let $E \to M$ be the map that takes each element of $E _ { p }$ to the point p. Suppose furthermore that we are given the following data: (i) an open cover $\{ U _ { \alpha } \} _ { \alpha \in A }$ of M (ii) for each $\alpha \in A$ , a bijective map $\phi _ { \alpha } \colon \pi ^ { - 1 } ( U _ { \alpha } ) \to U _ { \alpha } \times \mathbb { R } ^ { k }$ whose restriction to each $E _ { p }$ is a vector space isomorphism from $E _ { p }$ to $\{ p \} \times \mathbb { R } ^ { k } \cong \mathbb { R } ^ { k }$ (iii) for each $\alpha , \beta \in A$ with $U _ { \alpha } \cap U _ { \beta } \neq \emptyset$ , a smooth map $\tau _ { \alpha \beta } \colon U _ { \alpha } \cap U _ { \beta } \to$ GL.k; R/ such that the map $\varPhi _ { \alpha } \circ \varPhi _ { \beta } ^ { - 1 }$ from $( U _ { \alpha } \cap U _ { \beta } ) \times \mathbb { R } ^ { k }$ to itself has the form \[ \Phi_ {\alpha} \circ \Phi_ {\beta} ^ {- 1} (p, v) = \left(p, \tau_ {\alpha \beta} (p) v\right)\tag{10.3} \] Then E has a unique topology and smooth structure making it into a smooth manifold with or without boundary and a smooth rank-k vector bundle over M; with as projection and $\{ ( U _ { \alpha } , \Phi _ { \alpha } ) \}$ as smooth local trivializations. Proof. For each point $p \in M$ ; choose some $U _ { \alpha }$ containing $p ;$ choose a smooth chart $( V _ { p } , \varphi _ { p } )$ for M such that $p \in V _ { p } \subseteq U _ { \alpha } ;$ ; and let ${ \widehat { V } } _ { p } = \varphi _ { p } ( V _ { p } ) \subseteq \mathbb { R } ^ { n }$ or $\mathbb { H } ^ { n }$ (where n is the dimension of $M )$ . Define a map $\widetilde { \varphi } _ { p } \colon \pi ^ { - 1 } ( V _ { p } ) \to \widehat { V } _ { p } \times \mathbb { R } ^ { k } \mathrm { ~ b y ~ } \widetilde { \varphi } _ { p } = ( \varphi _ { p } \times \mathrm { I d } _ { \mathbb { R } ^ { k } } ) \circ$ $\varPhi _ { \alpha }$ \[ \pi^ {- 1} (V _ {p}) \xrightarrow {\varPhi_ {\alpha}} V _ {p} \times \mathbb {R} ^ {k} \xrightarrow {\varphi_ {p} \times \mathrm{Id} _ {\mathbb {R} ^ {k}}} \widehat {V} _ {p} \times \mathbb {R} ^ {k}. \]

Not formalized. none; no complete checked declaration under strict bundle semantics — VectorPrebundle/VectorBundleCore provide the construction of a topology and smooth vector-bundle structure from compatible transition data, but targeted P/H searches found no theorem proving Lee’s full uniqueness clause for the topology and smooth structure. The construction is a proper subset of Proposition 10.6 under whole-row semantics. Strict whole-row semantics reject proper subsets, unproved converse directions, missing uniqueness clauses, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.

Example 10.7

FC08-C10-U012 · Ch. 10, § Vector Bundles; source L7327 · in Mathlib

(Whitney Sums). Given smooth vector bundles $E' \to M$ and $E'' \to M$ of ranks $k'$ and $k''$, the Whitney sum has fiber $E'_{p} \oplus E''_{p}$ at each $p \in M$; its total space is $E' \oplus E'' = \coprod_{p \in M}(E'_{p} \oplus E''_{p})$ with the obvious projection, and since the fibers depend smoothly on $p$ the chart lemma makes it a smooth vector bundle over $M$. Its transition functions have the form $\widetilde{\Phi} \circ \Phi^{-1}(p,(v',v'')) = (p,\ \tau(p)(v',v''))$, where $\tau(p) = \tau'(p) \oplus \tau''(p) \in \mathrm{GL}(k'+k'',\mathbb{R})$ is the block diagonal matrix $\begin{pmatrix} \tau'(p) & 0 \\ 0 & \tau''(p) \end{pmatrix}$.

Formalized. Mathlib/Topology/VectorBundle/Constructions.lean::Bundle.Prod.prod, VectorBundle.prod, Bundle.Trivialization.coordChangeL_prod; Mathlib/Geometry/Manifold/VectorBundle/Basic.lean::Bundle.Prod.contMDiffVectorBundle — Mathlib’s bundle product E₁ ×ᵇ E₂ is the fiberwise direct sum. Product trivializations and coordChangeL_prod give the block/product transition map, and the resulting bundle has both topological and smooth vector-bundle instances. This is Lee’s Whitney-sum construction.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Example 10.8

FC08-C10-U013 · Ch. 10, § Vector Bundles; source L7347 · not formalized

(Restriction of a Vector Bundle). Suppose $\pi \colon E \to M$ is a rank-$k$ vector bundle and $S \subseteq M$ is any subset. The restriction of $E$ to $S$ is $E|_{S} = \bigcup_{p \in S} E_{p}$, with the projection $E|_{S} \to S$ obtained by restricting $\pi$. If $E$ is smooth and $S$ is an immersed or embedded submanifold, the chart lemma shows $E|_{S}$ is a smooth vector bundle; in particular, for a smooth submanifold $S \subseteq M$ the restricted bundle $TM|_{S}$ is called the ambient tangent bundle over $S$.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has pullback/restriction vector bundles along a map, including smooth pullbacks, but Lee’s row specifically quantifies over immersed/embedded submanifolds and names the restricted tangent bundle as the ambient tangent bundle. C05 has no general submanifold package, and C03’s tangent model remains unbridged; the complete row cannot be stated in the checked interface. Strict whole-row semantics reject proper subsets, unproved converse directions, missing uniqueness clauses, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.

Definition/convention — cross section) is a section of the map π

FC08-C10-U014 · Ch. 10, § Local and Global Sections of Vector Bundles; source L7351 · in Mathlib

Let $\pi \colon E \to M$ be a vector bundle. A section of $E$, sometimes called a cross section, is a section of the map $\pi$: a continuous map $\sigma \colon M \to E$ with $\pi \circ \sigma = \operatorname{Id}_{M}$, so that $\sigma(p) \in E_{p}$ for each $p \in M$.

Formalized. Mathlib/Data/Bundle.lean::Bundle.TotalSpace.mk'; Mathlib/Topology/FiberBundle/Basic.lean::FiberBundle.continuousAt_section — A dependent function s : ∀ p, E p is exactly fiber-valued section data; its total-space lift p ↦ TotalSpace.mk' F p (s p) satisfies projection-to-identity definitionally. FiberBundle.continuousAt_section is the continuity criterion for this lift. The C10 witness compiles the projection identity and continuity equivalence.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Definition/convention — global section

FC08-C10-U015 · Ch. 10, § Local and Global Sections of Vector Bundles; source L7353 · in Mathlib

More generally, a local section of E is a continuous map $\sigma \colon U \to E$ defined on some open subset $U \subseteq M$ and satisfying $\pi \circ \sigma = \operatorname { I d } _ { U }$ (see Fig. 10.3). To emphasize the distinction, a section defined on all of M is sometimes called a global section. Note that a local section of E over $U \subseteq M$ is the same as a global section of the restricted bundle $E | _ { U }$ . If M is a smooth manifold with or without boundary and E is a smooth vector bundle, a smooth (local or global) section of E is one that is a smooth map from its domain into $E$.

Formalized. Mathlib/Topology/FiberBundle/Basic.lean::FiberBundle.continuousWithinAt_section, FiberBundle.continuousAt_section; Mathlib/Geometry/Manifold/VectorBundle/Basic.lean::Bundle.Trivialization.contMDiffWithinAt_section, Bundle.Trivialization.contMDiffOn_section_iff; Mathlib/Geometry/Manifold/VectorBundle/ContMDiffSection.lean::ContMDiffSection; Mathlib/Geometry/Manifold/VectorBundle/Pullback.lean::ContMDiffVectorBundle.pullback — Local sections are represented by dependent fiber-valued maps on an open set (equivalently on the pullback/restricted bundle), with the checked continuity/smoothness predicates; ContMDiffSection bundles global smooth sections. These interfaces jointly realize Lee’s local/global and smooth-section definitions without changing the bundle semantics.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Definition/convention — rough (local

FC08-C10-U016 · Ch. 10, § Local and Global Sections of Vector Bundles; source L7355 · in Mathlib

section of E is one that is a smooth map from its domain to $E$ Just as with vector fields, for some purposes it is useful also to consider maps that would be sections except that they might not be continuous. Thus, we define a rough (local or global) section of $E$ over a set $U \subseteq M$ to be a map $\sigma \colon U \to E$ (not necessarily continuous) such that $\pi \circ \sigma = \operatorname { I d } _ { U } . \ A$ “section” without further qualification always means a con stics.

Formalized. Mathlib/Data/Bundle.lean::Bundle.TotalSpace.mk' — Lee’s rough section is exactly a dependent function s : ∀ p, E p; its lift p ↦ ⟨p,s p⟩ lies over the identity definitionally, with no continuity field. /tmp/fc08-c10-witness.lean compiles this exact encoding.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Definition/convention — source terminology/construction

FC08-C10-U017 · Ch. 10, § Local and Global Sections of Vector Bundles; source L7360 · in Mathlib

The zero section of $E$ is the global section $\zeta \colon M \to E$ defined by \[ \zeta(p) = 0 \in E_{p} \quad \text{for each } p \in M. \]

Formalized. Mathlib/Topology/VectorBundle/Basic.lean::Bundle.zeroSection, Bundle.continuous_zeroSection; Mathlib/Geometry/Manifold/VectorBundle/Basic.lean::contMDiff_zeroSection — Bundle.zeroSection is the pointwise zero section, and Mathlib proves it continuous and C^n for a vector bundle. This exactly matches Lee’s zero-section construction.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Definition/convention — source terminology/construction

FC08-C10-U018 · Ch. 10, § Local and Global Sections of Vector Bundles; source L7366 · not formalized

As in the case of vector fields, the support of a section is the closure of the set $\{ p \in M : \sigma ( p ) \neq 0 \}$

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has generic support/tsupport for fixed-codomain functions, but no checked support operation for a dependent section s : ∀ p, E p whose values lie in varying fibers. The set {p | s p ≠ 0} can be written manually, but there is no section-support interface to own Lee’s definition. Strict whole-row semantics reject proper subsets, unproved converse directions, missing uniqueness clauses, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.

Example 10.10

FC08-C10-U019 · Ch. 10, § Local and Global Sections of Vector Bundles; source L7370 · not formalized

Example 10.10 (Sections of Vector Bundles). Suppose M is a smooth manifold with or without boundary. (a) Sections of TM are vector fields on M . (b) Given an immersed submanifold $S \subseteq M$ with or without boundary, a section of the ambient tangent bundle $T M | _ { S } S$ is called a vector field along S . It is a continuous map $X \colon S \to T M$ such that $X _ { p } \in T _ { p } M$ for each $p \in S$ . This is different from a vector field on S, which satisfies $X _ { p } \in T _ { p } S$ at each point. (c) If $E = M \times \mathbb { R } ^ { k }$ is a product bundle, there is a natural one-to-one correspondence between sections of E and continuous functions from M to $\mathbb { R } ^ { k }$ : a continuous function $F \colon M \to \mathbb { R } ^ { k }$ determines a section $\widetilde { F } \colon M \to M \times \mathbb { R } ^ { k }$ by $\widetilde { F } ( x ) = \left( x , F ( x ) \right)$ , and vice versa. If M is a smooth manifold with or without boundary, then the section $\widetilde { F }$ is smooth if and only if F is. (d) The correspondence in the preceding paragraph yields a natural identification between the space $C ^ { \infty } ( M )$ / and the space of smooth sections of the trivial line bundle $M \times \mathbb { R } \to M$ If $E \to M$ is a smooth vector bundle, the set of all smooth global sections is a vector space under pointwise addition and scalar multiplication.

Not formalized. none; no complete checked declaration under strict bundle semantics — The product-bundle/function correspondence is available, but this four-part example bundle also identifies tangent-bundle sections with vector fields and ambient-tangent sections along a submanifold. Those parts hit the C03 tangent-model and C05 submanifold blockers, so the whole example is unmatched. Strict whole-row semantics reject proper subsets, unproved converse directions, missing uniqueness clauses, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.

Definition/convention — source terminology/construction

FC08-C10-U020 · Ch. 10, § Local and Global Sections of Vector Bundles; source L7380 · in Mathlib

sections of the trivial line bundle $M \times \mathbb { R } \to M$ If $E \to M$ is a smooth vector bundle, the set of all smooth global sections of E is a vector space under pointwise addition and scalar multiplication: \[ (c _ {1} \sigma_ {1} + c _ {2} \sigma_ {2}) (p) = c _ {1} \sigma_ {1} (p) + c _ {2} \sigma_ {2} (p). \]

Formalized. Mathlib/Geometry/Manifold/VectorBundle/ContMDiffSection.lean::ContMDiffSection, ContMDiffSection.instAddCommGroup, ContMDiffSection.instSMul, ContMDiffSection.instModule — ContMDiffSection I F ∞ V is the space of smooth global sections. Its pointwise operations form an additive commutative group and a module over the base field, exactly Lee’s real vector-space structure after specializing 𝕜=ℝ.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Convention/notation — Gamma(E), the space of smooth sections

FC08-C10-U021 · Ch. 10, § Local and Global Sections of Vector Bundles; source L7386 · in Mathlib

This vector space is usually denoted by $\Gamma ( E )$ . (For particular vector bundles, we will often introduce specialized notations for their spaces of sections, such as the notation ${ \mathfrak { X } } ( M )$ introduced in Chapter 8 for the space of smooth sections of $TM$.)

Formalized. Mathlib/Geometry/Manifold/VectorBundle/ContMDiffSection.lean::ContMDiffSection — ContMDiffSection I F ∞ V is Mathlib’s bundled type for the space Lee denotes Γ(E) of smooth global sections. The notation differs, but the represented object is the same.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Lemma 10.12

FC08-C10-U022 · Ch. 10, § Local and Global Sections of Vector Bundles; source L7400 · not formalized

Lemma 10.12 (Extension Lemma for Vector Bundles). Let $\pi \colon E \to M$ be a smooth vector bundle over a smooth manifold M with or without boundary. Suppose A is a closed subset of M; and $A E$ is a section of $E | _ { A }$ that is smooth in the sense that extends to a smooth local section of E in a neighborhood of each point. For each open subset $U \subseteq M$ containing A, there exists a global smooth section $\widetilde { \sigma } \in \Gamma ( E )$ such that $\widetilde { \sigma } | _ { A } = \sigma$ and supp ${ \tilde { \sigma } } \subseteq U$ Exercise 10.13. Prove the preceding lemma. Exercise 10.14. Let $\pi \colon E \to M$ be a smooth vector bundle. Show that each element of E is in the image of a smooth global section.

Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib has partitions of unity, smooth-section operations, and local extension of an individual fiber vector, but no checked theorem matching Lee’s closed-set section extension with prescribed values on the closed set and support contained in an arbitrary neighborhood. The same gap was encountered for vector fields in C08. Strict whole-row semantics reject proper subsets, unproved converse directions, missing uniqueness clauses, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.

Definition/convention — global frame

FC08-C10-U023 · Ch. 10, § Local and Global Frames; source L7408 · not formalized

The concept of local frames that we introduced in Chapter 8 extends readily to vector bundles. Let $E \to M$ be a vector bundle. If $U \subseteq M$ is an open subset, a $k \mathrm { - }$ tuple of local sections $( \sigma _ { 1 } , \ldots , \sigma _ { k } )$ of E over U is said to be linearly independent if their values $\big ( \sigma _ { 1 } ( p ) , \ldots , \sigma _ { k } ( p ) \big )$ form a linearly independent k-tuple in $E _ { p }$ for each $p \in U$ . Similarly, they are said to span E if their values span $E _ { p }$ for each $p \in U$ . A local frame for E over U is an ordered k-tuple $( \sigma _ { 1 } , \ldots , \sigma _ { k } )$ of linearly independent local sections over U that span $E ;$ ; thus $\big ( \sigma _ { 1 } ( p ) , \ldots , \sigma _ { k } ( p ) \big )$ is a basis for the fiber $E _ { p }$ for each $p \in U$ . It is called a global frame if $U = M$ . If $E \to M$ is a smooth vector bundle, a local or global frame is a smooth frame if each $\sigma _ { i }$ is a smooth section. We often denote a frame $( \sigma _ { 1 } , \ldots , \sigma _ { k } )$

Not formalized. none; no complete checked declaration under strict bundle semantics — IsLocalFrameOn is a direct predicate for smooth local frames, but Lee’s row first defines linearly independent/spanning local frames from merely continuous local sections and then separately defines smooth frames. No broader bundled frame predicate exists at P/H, so IsLocalFrameOn is a proper subset of the source definition bundle. Strict whole-row semantics reject proper subsets, unproved converse directions, missing uniqueness clauses, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.

Proposition 10.15

FC08-C10-U024 · Ch. 10, § Local and Global Frames; source L7414 · after FC08-C10-U022 · not formalized

If $( \sigma _ { 1 } , \hdots , \sigma _ { m } )$ is a linearly independent m-tuple of smooth local sections of E over an open subset $U \subseteq M$ ; with $1 \leq m < k$ , then for each $p \in U$ there exist smooth sections $\sigma _ { m + 1 } , \ldots , \sigma _ { k }$ defined on some neighborhood V of p such that $( \sigma _ { 1 } , \ldots , \sigma _ { k } )$ is a smooth local frame for E over $U \cap V$ (b) $I f \left( v _ { 1 } , \ldots , v _ { m } \right)$ is a linearly independent m-tuple of elements of $E _ { p }$ for some $p \in M$ ; with $1 \leq m \leq k$ , then there exists a smooth local frame $( \sigma _ { i } )$ for E over some neighborhood of p such that $\sigma _ { i } ( p ) = v _ { i } f o r i = 1 , \ldots , m$ (c) If $A \subseteq M$ is a closed subset and $( \tau _ { 1 } , \dots , \tau _ { k } )$ is a linearly independent k-tuple of sections of $E | _ { A }$ that are smooth in the sense described in Lemma 10.12, then there exists a smooth local frame $( \sigma _ { 1 } , \ldots , \sigma _ { k } )$ for E over some neighborhood of A such that $\sigma _ { i } | _ { A } = \tau _ { i } f o r i = 1 , \dots , k$ Exercise 10.16. Prove the preceding proposition. Local frames for a vector bundle are intimately connected with local trivializations, as the next two examples show. Example 10.17 (A Global Frame for a Product Bundle). If $E = M \times \mathbb { R } ^ { k } \to M$ is a product bundle, the standard basis $( e _ { 1 } , \ldots , e _ { k } )$ for $\mathbb { R } ^ { k }$ yields a global frame for $E$.

Not formalized. none; no complete checked declaration under strict bundle semantics — Targeted P/H searches found no completion theorem extending an arbitrary linearly independent tuple of smooth local sections/fiber vectors/closed-set frame data to a local frame. Local trivializations produce frames, but do not prove Lee’s three-part completion proposition from the stated input. Strict whole-row semantics reject proper subsets, unproved converse directions, missing uniqueness clauses, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.

Example 10.17

FC08-C10-U025 · Ch. 10, § Local and Global Frames; source L7426 · in Mathlib

Example 10.17 (A Global Frame for a Product Bundle). If $E = M \times \mathbb { R } ^ { k } \to M$ is a product bundle, the standard basis $( e _ { 1 } , \ldots , e _ { k } )$ for $\mathbb { R } ^ { k }$ yields a global frame $( \widetilde { e } _ { i } )$ for E, defined by $\tilde { e } _ { i } ( p ) = ( p , e _ { i } )$ . If M is a smooth manifold with or without boundary, then this global frame is smooth.

Formalized. Mathlib/Topology/FiberBundle/Constructions.lean::Bundle.Trivial.trivialization; Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean::Bundle.Trivialization.localFrame, Bundle.Trivialization.isLocalFrameOn_localFrame_baseSet — Applying localFrame to the canonical global trivialization of Bundle.Trivial M F and a basis of F gives a smooth frame on all of M. /tmp/fc08-c10-witness.lean compiles the global-frame statement, which specializes to the standard basis of ℝ^k in Lee’s example.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Example 10.18

FC08-C10-U026 · Ch. 10, § Local and Global Frames; source L7428 · in Mathlib

Example 10.18 (Local Frames Associated with Local Trivializations). Suppose $\pi \colon E \to M$ is a smooth vector bundle. If $\phi \colon \pi ^ { - 1 } ( U ) \to U \times \mathbb { R } ^ { k }$ is a smooth local trivialization of $E$ , we can use the same idea as in the preceding example to construct a local frame for E over $U$ . Define maps $\sigma _ { 1 } , \dots , \sigma _ { k } \colon U \to E$ by $\sigma _ { i } ( p ) = \phi ^ { - 1 } ( p , e _ { i } ) = \phi ^ { - 1 } \circ \widetilde { e } _ { i } ( p )$ Then $\sigma _ { i }$ is smooth, being a composition of smooth maps, and $(\sigma_{i})$ is a local frame for $E$ over $U$.

Formalized. Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean::Bundle.Trivialization.localFrame, Bundle.Trivialization.contMDiffOn_localFrame_baseSet, Bundle.Trivialization.isLocalFrameOn_localFrame_baseSet — e.localFrame b is defined by applying the inverse trivialization to basis vectors in the model fiber; Mathlib proves each resulting section smooth and the family a basis in every fiber on e.baseSet. This is Lee’s local-frame construction from a smooth trivialization.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Convention/notation — frame associated with a local trivialization

FC08-C10-U027 · Ch. 10, § Local and Global Frames; source L7438 · in Mathlib

Each $\sigma_{i}$ is a section, and $(\sigma_{i}(p))$ is a basis for $E_{p}$: the trivialization $\Phi$ restricts to an isomorphism $E_{p} \to \{p\} \times \mathbb{R}^{k}$ with $\Phi(\sigma_{i}(p)) = (p, e_{i})$, so it carries $(\sigma_{i}(p))$ to the standard basis of $\{p\} \times \mathbb{R}^{k} \cong \mathbb{R}^{k}$. This local frame $(\sigma_{i})$ is said to be associated with $\Phi$.

Formalized. Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean::Bundle.Trivialization.basisAt, Bundle.Trivialization.localFrame, Bundle.Trivialization.localFrame_apply_of_mem_baseSet, Bundle.Trivialization.isLocalFrameOn_localFrame_baseSet — The basisAt/localFrame API records exactly that the frame induced by a trivialization is the inverse image of the chosen model-fiber basis and forms a basis in every fiber. This is Lee’s “frame associated with a local trivialization.”

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Proposition 10.19

FC08-C10-U028 · Ch. 10, § Local and Global Frames; source L7440 · after FC08-C10-U026 · not formalized

i } )$ is associated with $\pmb { \phi }$ Proposition 10.19. Every smooth local frame for a smooth vector bundle is associated with a smooth local trivialization as in Example 10.18. Proof. Suppose $

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib constructs a smooth local frame from a trivialization, but the converse construction of a compatible smooth trivialization from an arbitrary smooth local frame is absent at P/H. LocalFrame.lean is one-way on this point. Strict whole-row semantics reject proper subsets, unproved converse directions, missing uniqueness clauses, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.

Corollary 10.20

FC08-C10-U029 · Ch. 10, § Local and Global Frames; source L7478 · not formalized

Corollary 10.20. A smooth vector bundle is smoothly trivial if and only if it admits a smooth global frame.

Not formalized. none; no complete checked declaration under strict bundle semantics — The forward direction is available for the canonical trivial bundle, but without the missing arbitrary-frame-to-trivialization construction there is no checked iff saying a smooth vector bundle is smoothly trivial exactly when it has a smooth global frame. Strict whole-row semantics reject proper subsets, unproved converse directions, missing uniqueness clauses, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.

Corollary 10.21

FC08-C10-U030 · Ch. 10, § Local and Global Frames; source L7484 · not formalized

Corollary 10.21. Let $\pi \colon E \to M$ be a smooth vector bundle of rank k, let $( V , \varphi )$ be a smooth chart on M with coordinate functions $\left( x ^ { i } \right)$ , and suppose there exists a smooth local frame $( \sigma _ { i } )$ for E over V . Define $\widetilde \varphi \colon \pi ^ { - 1 } ( V ) \to \varphi ( V ) \times \mathbb R ^ { k }$ by \[ \widetilde {\varphi} \big (v ^ {i} \sigma_ {i} (p) \big) = \big (x ^ {1} (p), \ldots , x ^ {n} (p), v ^ {1}, \ldots , v ^ {k} \big). \] Then $\left( \pi ^ { - 1 } ( V ) , \widetilde { \varphi } \right)$ is a smooth coordinate chart for $E$ Proof. Just check that $\widetilde { \varphi }$ is equal to the composition $\left( \varphi \times \operatorname { I d } _ { \mathbb { R } ^ { k } } \right) \circ \varPhi$ , where $\varPhi$

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib’s total-space charts come from bundle trivializations, and a trivialization gives a local frame, but the converse from an arbitrary smooth local frame is absent. Hence the coordinate chart asserted by Lee from arbitrary frame data is not a checked theorem. Strict whole-row semantics reject proper subsets, unproved converse directions, missing uniqueness clauses, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.

Definition/convention — component functions of τ

FC08-C10-U031 · Ch. 10, § Local and Global Frames; source L7494 · in Mathlib

Smoothness of sections of a vector bundle can be characterized in terms of local frames, as smoothness of vector fields is in terms of components in a chart. Suppose $(\sigma_{i})$ is a smooth local frame for $E$ over an open subset $U \subseteq M$. If $\tau \colon M \to E$ is a rough section, its value at $p \in U$ is $\tau(p) = \tau^{i}(p)\sigma_{i}(p)$ for uniquely determined numbers $(\tau^{1}(p),\dots,\tau^{k}(p))$, defining $k$ functions $\tau^{i} \colon U \to \mathbb{R}$, the component functions of $\tau$ with respect to that frame.

Formalized. Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean::IsLocalFrameOn.coeff, IsLocalFrameOn.coeff_apply_of_mem, IsLocalFrameOn.coeff_sum_eq — IsLocalFrameOn.coeff gives the unique fiberwise coordinate functionals of an arbitrary section relative to a smooth local frame, and coeff_sum_eq reconstructs the section from them. These are exactly Lee’s component functions.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Proposition 10.22

FC08-C10-U032 · Ch. 10, § Local and Global Frames; source L7496 · not formalized

Proposition 10.22 (Local Frame Criterion for Smoothness). Let $\pi \colon E \to M$ be a smooth vector bundle, and let $\tau \colon M \to E$ be a rough section. $I f \left( \sigma _ { i } \right)$ is a smooth local frame for E over an open subset $U \subseteq M$ ; then is smooth on $U$ if and only if its component functions with respect to $( \sigma _ { i } )$ are smooth. Proof. Let $\phi \colon \pi ^ { - 1 } ( U ) \to U \times \mathbb { R } ^ { k }$ be the local trivialization associated ion of vector bundles, called fiber bundles.

Not formalized. none; no complete checked declaration under strict bundle semantics — IsLocalFrameOn.contMDiffOn_of_coeff proves the coefficient-smoothness ⇒ section-smoothness direction for an arbitrary smooth frame, but the file explicitly states that a fully frame-intrinsic converse is still to be added. The available iff is only for frames induced by a trivialization, so Proposition 10.22 is not fully owned. Strict whole-row semantics reject proper subsets, unproved converse directions, missing uniqueness clauses, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.

Proposition 10.24

FC08-C10-U033 · Ch. 10, § Local and Global Frames; source L7506 · after FC08-C03-U031 · not formalized

Proposition 10.24 (Uniqueness of the Smooth Structure on TM ). Let M be a smooth n-manifold with or without boundary. The topology and smooth structure on TM constructed in Proposition 3.18 are the unique ones with respect to which $\pi \colon T M \to M$ is a smooth vector bundle with the given vector space structure on the fibers, and such that all coordinate vector fields are smooth local sections.

Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem proves Lee’s uniqueness characterization of the topology/smooth structure on the tangent bundle. Moreover, the standard TangentSpace bundle in Mathlib remains unbridged from Lee’s point-derivation tangent model from C03. Strict whole-row semantics reject proper subsets, unproved converse directions, missing uniqueness clauses, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.

Definition/convention — bundle homomorphism

FC08-C10-U034 · Ch. 10, § Bundle Homomorphisms; source L7512 · not formalized

If $\pi \colon E \to M$ and $\pi' \colon E' \to M'$ are vector bundles, a continuous map $F \colon E \to E'$ is a bundle homomorphism if there exists a map $f \colon M \to M'$ with $\pi' \circ F = f \circ \pi$.

Not formalized. none; no complete checked declaration under strict bundle semantics — P/H have bundles of fiberwise continuous linear maps, but targeted searches found no bundled notion of a continuous/smooth bundle homomorphism between total spaces (over varying or fixed bases), no bundle-isomorphism structure, and no inverse-smoothness theorem of Lee’s form. The source row therefore lacks its defining interface. Strict whole-row semantics reject proper subsets, unproved converse directions, missing uniqueness clauses, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.

Proposition 10.25

FC08-C10-U035 · Ch. 10, § Bundle Homomorphisms; source L7520 · not formalized

Proposition 10.25. Suppose $\pi \colon E \to M$ and $\pi ^ { \prime } \colon E \to M ^ { \prime }$ are vector bundles and $F \colon E \to E ^ { \prime }$ is a bundle homomorphism covering $f \colon M \to M ^ { \prime }$ . Then f is continuous and is uniquely determined by F . If the bundles and F are all smooth, then f is smooth 41a338593845667004cf2108c0.jpg) Fig.

Definition/convention — bundle isomorphism

FC08-C10-U036 · Ch. 10, § Bundle Homomorphisms; source L7524 · not formalized

A bijective bundle homomorphism $F \colon E \to E'$ whose inverse is also a bundle homomorphism is a bundle isomorphism; if $F$ is in addition a diffeomorphism, it is a smooth bundle isomorphism. Bundles admitting such a map are said to be (smoothly) isomorphic.

Definition/convention — slightly more restrictive notion of bundle homomorphism

FC08-C10-U037 · Ch. 10, § Bundle Homomorphisms; source L7526 · not formalized

In the special case in which both E and $E ^ { \prime }$ are vector bundles over the same base space M; a slightly more restrictive notion of bundle homomorphism is usually more useful. A bundle homomorphism over M is a bundle homomorphism covering the identity map of M; or in other words, a continuous map $F \colon E \to E ^ { \prime }$ such that $\pi ^ { \prime } \circ F = \pi$ \[ \begin{array}{c} E \xrightarrow {F} E ^ {\prime} \\ \pi \Big \downarrow \quad \Big \downarrow \pi^ {\prime} \\ M, \end{array} \] and whose restriction to each fiber is linear. If there exists a bundle homomorphism $F \colon E \to E ^ { \prime }$ over M that is also a (smooth) bundle isomorphism, then we say that E and $E ^ { \prime }$ are (smoothly) isomorphic over M . The next proposition shows that it is not necessary to check smoothness of the inverse map separately.

Proposition 10.26

FC08-C10-U038 · Ch. 10, § Bundle Homomorphisms; source L7536 · not formalized

Proposition 10.26. Suppose E and $E ^ { \prime }$ are smooth vector bundles over a smooth manifold M with or without boundary, and F $E E ^ { \prime }$ is a bijective smooth bundle homomorphism over M . Then F is a smooth bundle isomorphism.

Example 10.28

FC08-C10-U039 · Ch. 10, § Bundle Homomorphisms; source L7542 · not formalized

Example 10.28 (Bundle Homomorphisms). (a) If $F \colon M \to N$ is a smooth map, the global differential d $F \colon T M \to T N$ is a smooth bundle homomorphism covering F . (b) If $E \to M$ is a smooth vector bundle and $S \subseteq M$ is an immersed submanifold with or without boundary, then the inclusion map $E | _ { S } \hookrightarrow E$ is a smooth bundle homomorphism covering the inclusion of S into $M$.

Not formalized. none; no complete checked declaration under strict bundle semantics — The standard-tangent API has a global tangent map/differential and pullback-bundle maps, but Mathlib has no checked bundle-homomorphism structure to state the example as Lee does; part (b) also depends on the absent general submanifold package, and part (a) hits the C03 tangent-model boundary. Strict whole-row semantics reject proper subsets, unproved converse directions, missing uniqueness clauses, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.

Definition/convention — source terminology/construction

FC08-C10-U040 · Ch. 10, § Bundle Homomorphisms; source L7548 · not formalized

Suppose $E \to M$ and $E' \to M$ are smooth vector bundles over a smooth manifold $M$ with or without boundary, with spaces of smooth global sections $\Gamma(E)$ and $\Gamma(E')$. A smooth bundle homomorphism $F \colon E \to E'$ over $M$ induces a map $\widetilde{F} \colon \Gamma(E) \to \Gamma(E')$ by \[ \widetilde{F}(\sigma)(p) = (F \circ \sigma)(p) = F(\sigma(p)). \tag{10.5} \]

Not formalized. none; no complete checked declaration under strict bundle semantics — These rows require a smooth bundle-homomorphism-over-M interface and its induced action on smooth sections. P/H have neither such a bundle-map structure nor the full C^∞(M)-module structure on ContMDiffSection used by Lee’s characterization theorem. The pointwise/smooth-section primitives are proper subsets only. Strict whole-row semantics reject proper subsets, unproved converse directions, missing uniqueness clauses, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.

Definition/convention — linear

FC08-C10-U041 · Ch. 10, § Bundle Homomorphisms; source L7556 · not formalized

Because a bundle homomorphism is linear on fibers, the resulting map $\widetilde { F }$ on sections is linear over R. In fact, it satisfies a stronger linearity property. A map $\mathcal { F } \colon \Gamma ( E ) \Gamma ( E ^ { \prime } )$ is said to be linear over $C ^ { \infty } ( M )$ if for any smooth functions $u _ { 1 } , u _ { 2 } \in C ^ { \infty } ( M )$ and smooth sections $\sigma _ { 1 } , \sigma _ { 2 } \in \Gamma ( E )$ \[ \mathcal {F} (u _ {1} \sigma_ {1} + u _ {2} \sigma_ {2}) = u _ {1} \mathcal {F} (\sigma_ {1}) + u _ {2} \mathcal {F} (\sigma_ {2}). \]

Lemma 10.29

FC08-C10-U042 · Ch. 10, § Bundle Homomorphisms; source L7564 · not formalized

Lemma 10.29 (Bundle Homomorphism Characterization Lemma). Let $\pi \colon E \to$ M and $\pi ^ { \prime } \colon E ^ { \prime } \to M$ be smooth vector bundles over a smooth manifold M with or without boundary, and let $\Gamma ( E ) , \Gamma ( E ^ { \prime } )$ denote their spaces of smooth sections. A map $\mathcal { F } \colon \Gamma ( E ) \Gamma ( E ^ { \prime } )$ is linear over $C ^ { \infty } ( M )$ if and only if there is a smooth bundle homomorphism $F \colon E \to E ^ { \prime }$ over M such that $\mathcal { F } ( \sigma ) = F$ for all $\sigma \in \Gamma ( E )$

Example 10.30

FC08-C10-U043 · Ch. 10, § Bundle Homomorphisms; source L7600 · not formalized

Example 10.30 (Bundle Homomorphisms Over Manifolds). (a) If M is a smooth manifold and $f \in C ^ { \infty } ( M )$ , the map from ${ \mathcal { X } } ( M )$ to itself defined by $X \mapsto f X$ is linear over $C ^ { \infty } ( M )$ because $f ( u _ { 1 } X _ { 1 } + u _ { 2 } X _ { 2 } ) =$ $u _ { 1 } f X _ { 1 } + u _ { 2 } f X _ { 2 }$ , and thus defines a smooth bundle homomorphism over M from T M to itself. (b) If Z is a smooth vector field on $\mathbb { R } ^ { 3 }$ , the cross product with Z defines a map from $\mathcal { X } \left( \mathbb { R } ^ { 3 } \right)$ to itself: $X \mapsto X \times Z$ . Since it is linear over $C ^ { \infty } ( \mathbb { R } ^ { 3 } )$ in X , it determines a smooth bundle homomorphism over $\mathbb { R } ^ { 3 }$ from $T \mathbb { R } ^ { 3 } \mathrm { \Delta t o \ } T \mathbb { R } ^ { 3 }$ (c) Given $Z \in { \mathfrak { X } } ( \mathbb { R } ^ { n } )$ , the Euclidean dot product defines a map $X \mapsto X \cdot Z$ from ${ \mathcal { X } } \left( \mathbb { R } ^ { n } \right)$ to $C ^ { \infty } ( \mathbb { R } ^ { n } )$ , which is linear over $C ^ { \infty } ( \mathbb { R } ^ { n } )$ and thus determines a smooth bundle homomorphism from $T\mathbb{R}^{n}$ to the trivial line bundle.

Convention/notation — source terminology/construction

FC08-C10-U044 · Ch. 10, § Bundle Homomorphisms; source L7608 · after FC08-C10-U042 · not formalized

By Lemma 10.29 the notation $\widetilde{F}$ is usually dropped, the same symbol serving for a bundle homomorphism $F \colon E \to E'$ over $M$ and for the linear map $F \colon \Gamma(E) \to \Gamma(E')$ it induces on sections, since the action on sections is just pointwise application. The same convention is already in use elsewhere: for $a \in \mathbb{R}$, the notation $X \mapsto aX$ denotes both multiplication of tangent vectors in each $T_{p}M$ by $a$ and multiplication of vector fields by $a$, and since multiplication by $a$ is a bundle homomorphism from $TM$ to itself there is no ambiguity.

Definition/convention — smooth subbundle

FC08-C10-U045 · Ch. 10, § Subbundles; source L7614 · not formalized

Given a vector bundle $\pi_{E} \colon E \to M$, a subbundle of $E$ is a vector bundle $\pi_{D} \colon D \to M$ in which $D$ is a topological subspace of $E$ and $\pi_{D}$ is the restriction of $\pi_{E}$, such that for each $p \in M$ the subset $D_{p} = D \cap E_{p}$ is a linear subspace of $E_{p}$ with the inherited vector space structure. Requiring $D$ to be a vector bundle over $M$ forces every fiber $D_{p}$ to be nonempty and of the same dimension. If $E \to M$ is smooth, a subbundle is called a smooth subbundle when it is a smooth vector bundle and an embedded submanifold, with or without boundary, in $E$.

Not formalized. none; no complete checked declaration under strict bundle semantics — Targeted project, P, and current-H searches found no Subbundle/VectorSubbundle abstraction and no constant-rank kernel/image bundle theorem. Without a subbundle object and bundle-homomorphism interface, Lee’s definition, local-frame criterion, examples, rank definition, and kernel/image theorem cannot be stated as complete checked rows. Strict whole-row semantics reject proper subsets, unproved converse directions, missing uniqueness clauses, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.

Lemma 10.32

FC08-C10-U046 · Ch. 10, § Subbundles; source L7623 · not formalized

Lemma 10.32 (Local Frame Criterion for Subbundles). Let $\pi \colon E \to M$ be a smooth vector bundle, and suppose that for each $p \in M$ we are given an mdimensional linear subspace $D _ { p } \subseteq E _ { p }$ . Then $\begin{array} { r } { D = \bigcup _ { p \in M } D _ { p } \subseteq E } \end{array}$ is a smooth subbundle of E if and only if the following condition is satisfied: Each point of M has a neighborhood U on which there exist smooth local sections $\sigma _ { 1 } , . . . , \sigma _ { m } \colon U \to E$ with the property that $\sigma _ { 1 } ( q ) , \dots , \sigma _ { m } ( q )$ form a basis for $D _ { q }$ at each $q \in U$

Example 10.33

FC08-C10-U047 · Ch. 10, § Subbundles; source L7647 · not formalized

If M is a smooth manifold and V is a nowhere-vanishing smooth vector field on M; then the set $D \subseteq T M$ whose fiber at each $p \in M$ is the linear span of $V _ { p }$ is a smooth 1-dimensional subbundle of $T M$ (b) Suppose $E \to M$ is any trivial bundle, and let $( E _ { 1 } , \ldots , E _ { k } )$ be a smooth global frame for E. If $0 \leq m \leq k$ , the subset $D \subseteq E$ defined by $D _ { p } =$ span $\left( E _ { 1 } | _ { p } , \ldots , E _ { m } | _ { p } \right)$ for each $p \in M$ is a smooth subbundle of E. (c) Suppose M is a smooth manifold with or without boundary and $S \subseteq M$ is an immersed k-submanifold with or without boundary. Problem 10-14 asks you to prove that TS is a smooth rank-k subbundle of the ambient tangent bundle $T M | _ { S }$ The next theorem shows how to obtain many more subbundles. Suppose $E \to M$ and $E ^ { \prime } \to M$ are vector bundles and $F \colon E \to E ^ { \prime }$ is a bundle homomorphism over M . For each $p \in M$ ; the rank of the linear map $F { \big \vert } _ { E _ { p } }$ is called the rank of F at p. We say that $F$ has constant rank if its rank is the same at every point.

Definition/convention — rank of F at p

FC08-C10-U048 · Ch. 10, § Subbundles; source L7655 · not formalized

The next theorem shows how to obtain many more subbundles. Suppose $E \to M$ and $E ^ { \prime } \to M$ are vector bundles and $F \colon E \to E ^ { \prime }$ is a bundle homomorphism over M . For each $p \in M$ ; the rank of the linear map $F { \big \vert } _ { E _ { p } }$ is called the rank of F at p. We say that F has constant rank if its rank is the same for all $p \in M$

Theorem 10.34

FC08-C10-U049 · Ch. 10, § Subbundles; source L7657 · not formalized

Let $E$ and $E'$ be smooth vector bundles over a smooth manifold $M$ and let $F \colon E \to E'$ be a smooth bundle homomorphism over $M$. Define \[ \operatorname{Ker} F = \bigcup_{p \in M} \operatorname{Ker}\left(F|_{E_{p}}\right), \qquad \operatorname{Im} F = \bigcup_{p \in M} \operatorname{Im}\left(F|_{E_{p}}\right). \] Then $\operatorname{Ker} F$ and $\operatorname{Im} F$ are smooth subbundles of $E$ and $E'$ if and only if $F$ has constant rank.

Lemma 10.35

FC08-C10-U050 · Ch. 10, § Subbundles; source L7671 · not formalized

method for constructing interesting subbundles of the tangent bundle over submanifolds of $\mathbb { R } ^ { n }$ Lemma 10.35 (Orthogonal Complement Bundles). Let M be an immersed submanifold with or without boundary in $\mathbb { R } ^ { n }$ , and D be a smooth rank-k subbundle of $T \mathbb { R } ^ { n } | _ { M }$ . For each $p \in M$ ; let $D _ { p } ^ { \perp }$ denote the orthogonal complement of $D _ { p }$ in $T _ { p } \mathbb { R } ^ { n }$ with respect to the Euclidean dot product, and let $D ^ { \perp } \subseteq T \mathbb { R } ^ { n } | _ { M }$ be the subset \[ D ^ {\perp} = \left\{(p, v) \in T \mathbb {R} ^ {n}: p \in M, v \in D _ {p} ^ {\perp} \right\}. \] Then $D ^ { \perp }$ is a smooth ran $k { \mathord - } ( n - k )$ subbundle of $T \mathbb { R } ^ { n } | _ { M }$ . For each $p \in M$ ; there is a smooth orthonormal frame for $D^{\perp}$ on a neighborhood of $p$.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has inner-product/Riemannian vector-bundle infrastructure, but no checked smooth-subbundle abstraction or orthogonal-complement/normal-bundle construction of Lee’s form. These rows additionally quantify over immersed submanifolds, inheriting C05’s absent general submanifold interface; the planned orthonormal-frame layer is not present at P/H. Strict whole-row semantics reject proper subsets, unproved converse directions, missing uniqueness clauses, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.

Corollary 10.36

FC08-C10-U051 · Ch. 10, § Subbundles; source L7681 · not formalized

(The Normal Bundle to a Submanifold of $\mathbb{R}^{n}$). If $M \subseteq \mathbb{R}^{n}$ is an immersed $m$-dimensional submanifold with or without boundary, its normal bundle $NM$ is a smooth rank-$(n-m)$ subbundle of $T\mathbb{R}^{n}|_{M}$, and each $p \in M$ has a neighborhood carrying a smooth orthonormal frame for $NM$.

Definition/convention — local trivialization of E

FC08-C10-U052 · Ch. 10, § Fiber Bundles; source L7689 · in Mathlib

Let M and $F$ be topological spaces. A fiber bundle over M with model fiber $\pmb { F }$ is a topological space E together with a surjective continuous map $\pi \colon E \to M$ with the property that for each $x \in M$ ; there exist a neighborhood $U$ of $x$ in M and a homeomorphism $\phi \colon \pi ^ { - 1 } ( U ) \to U \times F$ , called a local trivialization of E over $U$ , such that the following diagram commutes: \[ \begin{array}{c} \pi^ {- 1} (U) \xrightarrow {\varPhi} U \times F \\ \big \backslash \quad \big \backslash \quad \big \backslash \quad \big \backslash \\ U. \end{array} \]

Formalized. Mathlib/Topology/FiberBundle/Basic.lean::FiberBundle, FiberBundle.trivializationAt, FiberBundle.continuous_proj; Mathlib/Topology/FiberBundle/Trivialization.lean::Bundle.Trivialization — FiberBundle F E is precisely a topological bundle locally homeomorphic over the base to a product with fixed model fiber F; its atlas consists of Bundle.Trivializations commuting with projection, and the projection is continuous. This is Lee’s topological fiber-bundle definition.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Construction/definition — total space of the bundle

FC08-C10-U053 · Ch. 10, § Fiber Bundles; source L7695 · not formalized

The space E is called the total space of the bundle, M is its base, and $\pi$ is its projection. If E, M; and F are smooth manifolds with or without boundary, is a smooth map, and the local trivializations can be chosen to be diffeomorphisms, then it is called a smooth fiber bundle.

Not formalized. none; no complete checked declaration under strict bundle semantics — The topological FiberBundle part is formalized, but P/H have no general ContMDiffFiberBundle/smooth-fiber-bundle interface for an arbitrary model fiber. Smooth vector bundles are a special case and cannot own Lee’s general smooth fiber-bundle definition. Strict whole-row semantics reject proper subsets, unproved converse directions, missing uniqueness clauses, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.

Definition/convention — smoothly trivial

FC08-C10-U054 · Ch. 10, § Fiber Bundles; source L7697 · not formalized

A trivial fiber bundle is one that admits a local trivialization over the entire base space (a global trivialization). It is said to be smoothly trivial if it is a smooth bundle and the global trivialization is a diffeomorphism.

Not formalized. none; no complete checked declaration under strict bundle semantics — IsHomeomorphicTrivialFiberBundle owns the topological trivial-bundle condition, but there is no general smooth-fiber-bundle/smooth-triviality predicate supplying the diffeomorphic version required by the same row. Strict whole-row semantics reject proper subsets, unproved converse directions, missing uniqueness clauses, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.

Example 10.37

FC08-C10-U055 · Ch. 10, § Fiber Bundles; source L7699 · after FC08-C10-U007 · not formalized

Example 10.37 (Fiber Bundles). (a) Every product space $M \times F$ is a fiber bundle with projection $\pi _ { 1 } \colon M \times F \to M .$ called a product fiber bundle. It has a global trivialization given by the identity map $M \times F M \times F$ , so every product bundle is trivial. (b) Every rank-k vector bundle is a fiber bundle with model fiber $\mathbb { R } ^ { k }$ (c) If $E \to \mathbb { S } ^ { 1 }$ is the Möbius bundle of Example 10.3, then the image of $\mathbb { R } \times [ - 1 , 1 ]$ under the quotient map $q \colon { \mathbb { R } } ^ { 2 } \to E$ is a fiber bundle over $\mathbb { S } ^ { 1 }$ with model fiber Œ 1; 1. It is not a trivial bundle. (Can you prove it?) (d) Every covering map $\pi \colon E \to M$ is a fiber bundle whose model fiber is discrete. To construct local trivializations, let S be a discrete space with the same cardinality as the fibers of . For each evenly covered open subset $U \subseteq M$ ; define a map $\phi \colon \pi ^ { - 1 } ( U ) \to U \times S$ by choosing a bijection between the set of components of $\pi ^ { - 1 } ( U )$ and S, and letting $\phi ( x ) = { \bigl ( } \pi ( x ) , c ( x ) { \bigr ) }$ , where $c ( x )$ is the element of $S$ corresponding to the component containing $x$.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib directly owns product fiber bundles and every vector bundle is built on a FiberBundle, and it has general covering/fiber-bundle ingredients. But Lee’s four-part example also includes the explicit Möbius strip sub-bundle and its nontriviality; no checked declaration packages that example, so the whole bundle is unmatched. Strict whole-row semantics reject proper subsets, unproved converse directions, missing uniqueness clauses, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.