FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013)
FC08 — Lee, Introduction to Smooth Manifolds.
This chapter contains 23 definitions, 14 propositions, 3 lemmas, 3 corollaries, 2 examples, 2 constructions, 9 conventions and 1 other statements.
Of the 57 statements checked against Lean, 17 are formalized somewhere and 40 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 40 | 70% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 17 | 30% | Mathlib states and proves it. |
| checked in total | 57 |
- Canonical source block: FC08 Lee, Chapter 3,
FC08-C03-U001–FC08-C03-U057, exactly 57 unique contiguous rows retrieved from FC08 — John M. Lee, Introduction to Smooth Manifolds throughagent-memory. - 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), followed by current/open/indexed and external Lean checks for the remaining interfaces. Noproject-existing,package-import, orreference-portC03 owner survived strict bundle checking. - Every promoted Mathlib path exists at exact
P./tmp/fc08-c03-witness.leancompiled through the project toolchain and checks the nontrivial U011 assembly:fdifferentialof the identity is the identity onPointDerivation, and for a smooth diffeomorphism the derivation differentials of the map and its inverse are mutual inverses. The same witness checks thePointDerivationreal-module instance and the smooth-function stalk/evaluation interfaces used in the germ audit. The witness is audit evidence only, not project source. - C03 has 17 pinned
mathlibrows and 40 datedunmatchedrows. Positive rows are: U001, U002, U003, U004, U007, U008, U009, U010, U011, U043, U044, U047, U048, U051, U052, U053, U054. - The decisive C03 interface boundary is explicit in pinned
Mathlib/Geometry/Manifold/DerivationBundle.lean:PointDerivationformalizes Lee’s algebraic tangent-space definition andfdifferentialformalizes the differential by precomposition, but the file only documents that this model coincides with the usual tangent space for finite-dimensionalC^∞real manifolds; it does not provide a checkedPointDerivation ≃ TangentSpaceequivalence. Targeted searches atPand currentHfound no such bridge. Consequently U005–U006 and U012–U042 are not inferred from the otherwise extensive chart/model-spaceTangentSpace,mfderiv,TangentBundle, andtangentMapAPIs. - U002–U004 and U007–U011 are promoted entirely inside the derivation model.
PointDerivationis genericDerivationon smooth functions with evaluation at the point as the scalar action;fdifferential_applyis literally Lee’s precomposition formula. For U011, chain, identity, and diffeomorphism-inverse clauses were compiled at the pin rather than inferred from the separate standard tangent-space derivative API. - U001 is independent of the later derivation identification: Mathlib’s standard-model
TangentSpaceis definitionally the model vector space and its constant-fibreTangentBundletotal space canonically identifies with base × fibre, matching Lee’s preliminary geometric tangent-vector model up to suppression of the fixed base coordinate. - U043–U044 are mapped to the stalk of the smooth real-function sheaf.
exists_germ_eq,germ_eq, andgerm_res_applygive exactly the representative/restriction/equality-on-a-neighborhood semantics of smooth germs. U045 remains unmatched because the pin does not package these stalks with the complete scalar-algebra/module structure needed to instantiate Lee’s ℝ-linear point-derivation space on germs; genericDerivationplus a stalk is only adjacent infrastructure without that assembly. - U047–U048 and U051–U054 are direct generic category-theory interfaces. U050 is not promoted from
CategoryTheory.Pointedalone because Lee’s row deliberately ranges over pointed sets, topological spaces, and smooth manifolds; the checked sources do not package the full pointed-smooth-manifold category. U055–U057 similarly remain unmatched because the specific smooth-manifold categories/functors are not bundled interfaces even though their constituent pointwise maps and functorial laws exist. - Current upstream
H=5315eef9e4ffb98e0f89f278b765c50a149f66cawas checked without changing the pinned worktree. Exact greps for aPointDerivation/TangentSpacebridge, a tangent functor, velocity realization, coordinate-vector tangent APIs, and a pointed smooth-manifold category found no current-only owner. The project and pinned Mathlib worktrees remained unmodified by the audit. N=2026-09-07denotes a dated unmatched result after the prescribed search layers. Strict whole-row semantics apply uniformly: no proper subset, unbridged equivalent model, isolated example, or reconstruction of the missing theorem is promoted.
Convention/notation — geometric tangent space to
Here is a preliminary definition of tangent vectors in Euclidean space. Given a point a ∈ ℝ ^n , let us define the geometric tangent space to ℝ ^n at ^a , denoted by ℝ _a ^n , to be the set a × ℝ ^n = ( a , v ) : v ∈ ℝ ^n . A geometric tangent vector in ℝ ^n is an element of ℝ _a ^n for some a ∈ ℝ ^n As a matter of notation, we abbreviate ( a , v ) as v _a (or sometimes ∣ v ∣ _a if it is clearer, for example if v itself has a subscript). We think of v _a as the vector v with its initial point at a (Fig. 3.1).The set ℝ _a ^n is a real vector space under the natural operations \[ v_{a} + w_{a} = (v+w)_{a}, \qquad c(v_{a}) = (cv)_{a}, \] and the vectors \(e_{i}|_{a}\), \(i = 1,\dots,n\), are a basis for \(\mathbb{R}^{n}_{a}\).
Formalized. Mathlib/Geometry/Manifold/IsManifold/Basic.lean::TangentSpace, TangentBundle; Mathlib/Data/Bundle.lean::Bundle.TotalSpace.toProd — TangentSpace for the standard vector-space model is definitionally the model vector space, while TangentBundle is its total-space bundle and Bundle.TotalSpace.toProd identifies a constant-fibre total space with base × fibre. This is Lee’s geometric tangent-vector model up to the canonical identification that suppresses the fixed base point in the fibre.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition/convention — derivation at a
With this construction in mind, we make the following definition. If a is a point of R, a map w \(C ^ { \infty } \left( \mathbb { R } ^ { n } \right) \to \mathbb { R }\) is called a derivation at a if it is linear over R and satisfies the following product rule: \[ w (f g) = f (a) w g + g (a) w f.\tag{3.3} \] Let \(T _ { a } \mathbb { R } ^ { n }\)
Formalized. Mathlib/Geometry/Manifold/DerivationBundle.lean::PointDerivation, PointedContMDiffMap.eval; Mathlib/RingTheory/Derivation/Basic.lean::Derivation, Derivation.leibniz — PointDerivation I a is exactly a derivation from the algebra of smooth scalar-valued functions to the scalar field with the module action induced by evaluation at a; generic Derivation.leibniz is precisely Lee’s product rule.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition/convention — source terminology/construction
Let T _a ℝ ^n denote the set of all derivations of C ^∞ ( ℝ ^n ) at a . . Clearly, T _a ℝ ^n is a vector space under the operations \[ (w_{1}+w_{2})f = w_{1}f + w_{2}f, \qquad (cw)f = c(wf). \] It is finite-dimensional, and naturally isomorphic to the geometric tangent space \(\mathbb{R}^{n}_{a}\).
Formalized. Mathlib/Geometry/Manifold/DerivationBundle.lean::PointDerivation; Mathlib/RingTheory/Derivation/Basic.lean::Derivation.instModule — PointDerivation I a is the type of all point derivations, and the generic derivation module instance makes it a vector space over the scalar field, exactly Lee’s T_a ℝ^n construction.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Lemma 3.1
(Properties of Derivations). Suppose \(a \in \mathbb{R}^{n}\), \(w \in T_{a}\mathbb{R}^{n}\), and \(f, g \in C^{\infty}(\mathbb{R}^{n})\). (a) If \(f\) is a constant function, then \(wf = 0\). (b) If \(f(a) = g(a) = 0\), then \(w(fg) = 0\).
Formalized. Mathlib/Geometry/Manifold/DerivationBundle.lean::PointDerivation, PointedContMDiffMap.smul_def; Mathlib/RingTheory/Derivation/Basic.lean::Derivation.map_algebraMap, Derivation.leibniz — Derivation.map_algebraMap kills scalar constants. If both values at the base point vanish, Derivation.leibniz together with the evaluation scalar action makes both product-rule terms zero, giving the two clauses of Lee’s lemma.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition 3.2
Proposition 3.2. Let \(a \in \mathbb { R } ^ { n }\) . (a) For each geometric tangent vector \(v _ { a } \in \mathbb { R } _ { a } ^ { n }\) , the map \(D _ { v } | _ { a } \colon C ^ { \infty } ( \mathbb { R } ^ { n } ) \to \mathbb { R }\) defined by (3.1) is a derivation at a. (b) The map \(v _ { a } \mapsto D _ { v } | _ { a }\) is an isomorphism from \(\mathbb { R } _ { a } ^ { n }\)
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib has both Lee’s algebraic PointDerivation model and its chart/model-space TangentSpace model, but no checked finite-dimensional real-manifold equivalence between them. The derivation bundle documentation explicitly notes coincidence only informally, so the directional-vector-to-derivation isomorphism is not promoted. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Corollary 3.3
For any \(a \in \mathbb{R}^{n}\), the \(n\) derivations \(\left.\frac{\partial}{\partial x^{1}}\right|_{a}, \dots, \left.\frac{\partial}{\partial x^{n}}\right|_{a}\), defined by \(\left.\frac{\partial}{\partial x^{i}}\right|_{a} f = \frac{\partial f}{\partial x^{i}}(a)\), form a basis for \(T_{a}\mathbb{R}^{n}\), which therefore has dimension \(n\).
Not formalized. none; no complete checked declaration under strict bundle semantics — Coordinate partial derivatives and finite-dimensional tangent spaces exist in the standard differential API, but no checked theorem identifies that standard tangent space with the chapter’s PointDerivation space; hence the claimed derivation basis/dimension cannot be credited under strict bridge semantics. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Definition/convention — derivation at p
Now we are in a position to define tangent vectors on manifolds and manifolds with boundary. The definition is the same in both cases. Let M be a smooth manifold with or without boundary, and let \(p\) be a point of M . A linear map v \(C ^ { \infty } ( M ) \to \mathbb { R }\) is called a derivation at p if it satisfies \[ v (f g) = f (p) v g + g (p) v f \quad \text { for all } f, g \in C ^ {\infty} (M).\tag{3.4} \]
Formalized. Mathlib/Geometry/Manifold/DerivationBundle.lean::PointDerivation, PointedContMDiffMap.eval; Mathlib/RingTheory/Derivation/Basic.lean::Derivation — For an arbitrary smooth manifold, PointDerivation I p is exactly Lee’s definition: an ℝ-linear derivation on globally smooth scalar functions, with the target-module action given by evaluation at p.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition/convention — tangent space to M at p
The set of all derivations of \(C ^ { \infty } ( M )\) at \(p ,\) , denoted by \(T _ { p } M ,\) is a vector space called the tangent space to M at p. An element of \(T _ { p } M\) is called a tangent vector at \(\pmb { p } .\) The following lemma is the analogue of Lemma 3.1 for manifolds.
Formalized. Mathlib/Geometry/Manifold/DerivationBundle.lean::PointDerivation; Mathlib/RingTheory/Derivation/Basic.lean::Derivation.instModule — PointDerivation I p is the set/type of all derivations at p, and the derivation module instance supplies its scalar-vector-space structure, exactly Lee’s tangent-space definition in this chapter.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Lemma 3.4
Lemma 3.4 (Properties of Tangent Vectors on Manifolds). Suppose M is \(a\) smooth manifold with or without boundary, \(p \in M , v \in T _ { p } M\) ; and \(f , g \in C ^ { \infty } ( M )\) . (a) If f is a constant function, then \(v f = 0 .\) (b) \(I f f ( p ) = g ( p ) = 0 , t h e n \ v ( f g ) = 0 .\)
Formalized. Mathlib/Geometry/Manifold/DerivationBundle.lean::PointDerivation, PointedContMDiffMap.smul_def; Mathlib/RingTheory/Derivation/Basic.lean::Derivation.map_algebraMap, Derivation.leibniz — This is the manifold specialization of the generic derivation facts used for U004: constants are killed and the Leibniz rule gives zero on a product when both factors vanish at the base point.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Construction/definition — differential of F at p (Fig
If M and N are smooth manifolds with or without boundary and F : M → N is a smooth map, for each p ∈ M we define a map d F _p : T _p M → T _F (p) N, called the differential of F at p (Fig. 3.3), as follows. Given v ∈ T _p M ; we let d F _p ( v ) be the derivation at F ( p ) that acts on f ∈ C ^∞ ( N ) by the rule \[ dF_{p}(v)(f) = v(f \circ F), \qquad dF_{p} \colon T_{p}M \to T_{F(p)}N. \]
Formalized. Mathlib/Geometry/Manifold/DerivationBundle.lean::fdifferential, fdifferential_apply — fdifferential f p is a scalar-linear map between PointDerivation spaces, and fdifferential_apply states exactly d f_p(v)(g)=v(g ∘ f).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition 3.6
Proposition 3.6 (Properties of Differentials). Let M; N , and P be smooth manifolds with or without boundary, let \(F \colon M \to N\) and \(G \colon N \to P\) be smooth maps, and let \(p \in M\) (a) d \(F _ { p } \colon T _ { p } M \to T _ { F ( p ) } N\) is linear. (b) \(d ( G \circ F ) _ { p } = d G _ { F ( p ) } \circ d F _ { p } \colon T _ { p } M \to T _ { G \circ F ( p ) } P .\) (c) \(d ( \mathrm { I d } _ { M } ) _ { p } = \mathrm { I d } _ { T _ { p } M } \colon T _ { p } M \to T _ { p } M .\) (d) If F is a diffeomorphism, then d \(F _ { p } \colon T _ { p } M \to T _ { F ( p ) } N\) is an isomorphism, and \(\begin{array} { r } { ( d F _ { p } ) ^ { - 1 } = d \bigl ( F ^ { - 1 } \bigr ) _ { F ( p ) } . } \end{array}\) Exercise 3.7. Prove Proposition 3.6.
Formalized. Mathlib/Geometry/Manifold/DerivationBundle.lean::fdifferential, fdifferential_comp; Mathlib/Geometry/Manifold/ContMDiffMap.lean::ContMDiffMap.id, ContMDiffMap.comp; Mathlib/Geometry/Manifold/Diffeomorph.lean::Diffeomorph.toContMDiffMap — fdifferential is linear and fdifferential_comp is the chain rule. At the identity its action is definitionally the identity derivation; applying the chain rule to a diffeomorphism and its inverse proves the two differentials are mutual inverses. All four clauses were compiled together in the C03 pinned audit witness.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition 3.8
Proposition 3.8. Let M be a smooth manifold with or without boundary, \(p \in M\) and \(v \in T _ { p }\) M . If f; \(g \in C ^ { \infty } ( M )\) agree on some neighborhood of p, then \(v f = v g\)
Not formalized. none; no complete checked declaration under strict bundle semantics — The smooth-function API is local and the smooth sheaf has germs, but no checked theorem states that a global PointDerivation depends only on the germ of a smooth function at its base point. Proving this requires the substantive locality argument. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Proposition 3.9
Proposition 3.9 (The Tangent Space to an Open Submanifold). Let M be a smooth manifold with or without boundary, let \(U \subseteq M\) be an open subset, and let \(U \hookrightarrow\) M be the inclusion map. For every \(p \in U\) , the differential $d _ { p } T _ { p } U $ \(T _ { p } M\) is an isomorphi erm in the last sum above is a product of two smooth functions of x that vanish at \(x = a \mathrm { : }\) one is \(\left( x ^ { i } - a ^ { i } \right)\) , and the other is \(\left( x ^ { j } - a ^ { j } \right)\) times the integral.
Not formalized. none; no complete checked declaration under strict bundle semantics — The standard tangent-space API gives canonical differentials for open charts/local diffeomorphisms, but no checked theorem gives the open-submanifold inclusion isomorphism for PointDerivation, Lee’s tangent-space model in this chapter. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Comparison/convention — source terminology/construction
Given an open subset \(U \subseteq M .\) the isomorphism \(d \iota _ { p }\) between \(T _ { p } U\) and \(T _ { p }\) M is canonically defined, independently of any choices. From now on we identify \(T _ { p } U\) with \(T _ { p } M\) for any point \(p \in U\) . This identification just amounts to the observation that \(d \iota _ { p } ( v )\) is the same derivation as v, thought of as acting on functions on the bigger manifold M instead of functions on \(U\) . Since the action of a derivation on a function depends only on the values of the function in an arbitrarily small neighborhood, this is a harmless identification. In particular, this means that any tangent vector \(v \in T _ { p } M\) can be unambiguously applied to functions defined only in a neighborhood of \(p\) , not necessarily on all of M .
Not formalized. none; no complete checked declaration under strict bundle semantics — This identification depends on U013 together with locality of point derivations. The checked APIs do not bridge PointDerivation to local smooth germs/open-submanifold tangent spaces, so the convention is not formally justified as a complete route. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Proposition 3.10
Proposition 3.10 (Dimension of the Tangent Space). If M is an n-dimensiona smooth manifold, then for each \(p \in M .\) ; the tangent space \(T _ { p } M\) is an n-dimensional vector space.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib’s standard TangentSpace is the model vector space and thus has the expected finite dimension, but no checked finite-dimensional equivalence identifies it with Lee’s derivation-defined PointDerivation; the chapter theorem is therefore unmatched. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Lemma 3.11
Let \(\iota \colon \mathbb{H}^{n} \hookrightarrow \mathbb{R}^{n}\) denote the inclusion map. For any \(a \in \partial\mathbb{H}^{n}\), the differential \(d\iota_{a} \colon T_{a}\mathbb{H}^{n} \to T_{a}\mathbb{R}^{n}\) is an isomorphism.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib’s model-with-corners tangent-space machinery handles half-spaces and inclusions, but the source statement is about the derivation-defined tangent spaces and no checked bridge to PointDerivation exists. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Proposition 3.12
and its image in \(T _ { a } \mathbb { R } ^ { n }\) Proposition 3.12 (Dimension of Tangent Spaces on a Manifold with Boundary). Suppose M is an n-dimensional smooth manifold with boundary. For each \(p \in M\) \(T _ { p } M\) is an n-dimensional vector sp this proposition, we can identify the tangent space to an open submanifold with the tangent space to the whole manifold.
Not formalized. none; no complete checked declaration under strict bundle semantics — As for U015, finite-dimensionality is immediate for Mathlib’s standard model-space tangent fibre but is not connected by a checked theorem to Lee’s PointDerivation tangent space on manifolds with boundary. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Construction/definition — map D
Suppose V is a finite-dimensional vector space and \(a \in V\) . Just as we did earlier in the case of \(\mathbb { R } ^ { n }\) , for any vector \(v \in V\) , we define a map \(D _ { v } | _ { a } \colon C ^ { \infty } ( V ) \to { \mathbb { R } }\) by \[ D _ {v} | _ {a} f = \left. \frac {d}{d t} \right| _ {t = 0} f (a + t v).\tag{3.5} \]
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib has Fréchet/manifold derivatives and NormedSpace.fromTangentSpace, but no checked construction identifies Lee’s directional derivative functional with a PointDerivation in the finite-dimensional vector-space case. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Proposition 3.13
Proposition 3.13 (The Tangent Space to a Vector Space). Suppose V is a finitedimensional vector space with its standard smooth manifold structure. For each point \(a \in V\) , the map \(v \mapsto D _ { v } | _ { a }\) defined by (3.5) is a canonical isomorphism from V to \(T _ { a } V .\) , such that for any linear map \(L \colon V \to W\) , the following diagram commutes: \[ \begin{array}{c} V \xrightarrow {\cong} T _ {a} V \\ L \Big \downarrow \qquad \qquad \qquad \qquad \Big \downarrow d L _ {a} \\ W \xrightarrow {\cong} T _ {L a} W. \end{array}\tag{3.6} \]
Not formalized. none; no complete checked declaration under strict bundle semantics — NormedSpace.fromTangentSpace canonically identifies Mathlib’s standard tangent fibre with the ambient normed space, but the theorem here identifies the ambient space with Lee’s derivation-defined tangent space and asserts naturality for linear maps. The missing PointDerivation ≃ TangentSpace bridge blocks the row. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Proposition 3.14
product manifold. Proposition 3.14 (The Tangent Space to a Product Manifold). Let \(M _ { 1 } , \dots , M _ { k }\) be smooth manifolds, and for each j M _ { k } M _ { j }$ be the projection onto the \(M _ { j }\) factor. For any point $ ) M _ { 1 } M _ { k }$ , the map \[ \alpha \colon T _ {p} (M _ {1} \times \dots \times M _ {k}) \rightarrow T _ {p _ {1}} M _ {1} \oplus \dots \oplus T _ {p _ {k}} M _ {k} \] defined by \[ \alpha (v) = \left(d (\pi_ {1}) _ {p} (v), \dots , d (\pi_ {k}) _ {p} (v)\right)\tag{3.7} \] is an isomorphism. The same is true if one of the spaces $
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib has exact product-tangent equivalences and derivatives of projections for its standard tangent spaces, but no checked bridge transfers that theorem to the derivation-defined tangent spaces used by Lee in C03. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Convention/notation — coordinate vectors at p associated
By Corollary 3.3, the derivations \(\partial / \partial x ^ { 1 } | _ { \varphi ( p ) } , \ldots , \partial / \partial x ^ { n } | _ { \varphi ( p ) }\) form a basis for \(T _ { \varphi ( p ) } \mathbb { R } ^ { n }\) . Therefore, the preimages of these vectors under the isomorphism \(d \varphi _ { p }\) form a basis for \(T _ { p } M \ ( \mathrm { F i g . } \ 3 . 5 )\) . In keeping with our standard practice of treating coordinate maps as identifications whenever possible, we use the notation \(\partial / \partial x ^ { i } | _ { p }\) for these vectors, characterized by either of the following expressions: \[ \left. \frac {\partial}{\partial x ^ {i}} \right| _ {p} = (d \varphi_ {p}) ^ {- 1} \left(\left. \frac {\partial}{\partial x ^ {i}} \right| _ {\varphi (p)}\right) = d (\varphi^ {- 1}) _ {\varphi (p)} \left(\left. \frac {\partial}{\partial x ^ {i}} \right| _ {\varphi (p)}\right).\tag{3.8} \] Unwinding the definitions, we see that \(\partial / \partial x ^ { i } | _ { p }\) acts on a function \(f \in C ^ { \infty } ( U )\) by \[ \left. \frac {\partial}{\partial x ^ {i}} \right| _ {p} f = \left. \frac {\partial}{\partial x ^ {i}} \right| _ {\varphi (p)} \big (f \circ \varphi^ {- 1} \big) = \frac {\partial \widehat {f}}{\partial x ^ {i}} (\widehat {p}), \] where \(\hat { f } = f \circ \varphi ^ { - 1 }\) is the coordinate representation of \(f\) , and \(\widehat { p } = \left( p ^ { 1 } , \ldots , p ^ { n } \right) =\) \(\varphi ( p )\) is the coordinate representation of \(p\) . In other words, \(\partial / \partial x ^ { i } | _ { p }\) is just the derivation that takes the i th partial derivative of (the coordinate representation of) f at (the coordinate representation of) p. The vectors \(\partial / \partial x ^ { i } \rvert _ { p }\) are called the coordinate vectors at p associated with the given coordinate system. In the special case of standard coordinates on \(\mathbb { R } ^ { n }\) , the vectors \(\partial / \partial x ^ { i } | _ { p }\) are literally the partial derivative operators. When M is a smooth manifold with boundary and \(p\) is an interior point, the discussion above applies verbatim. For \(p \in \partial M\) ; the only change that needs to be made is to substitute \(\mathbb { H } ^ { n }\) for \(\mathbb { R } ^ { n }\) , with the understanding that the notation \(\partial / \partial x ^ { i } | _ { \varphi ( p ) }\) can be used interchangeably to denote either an element of \(T _ { \varphi ( p ) } \mathbb { R } ^ { n }\) or an element of \(T _ { \varphi ( p ) } \mathbb { H } ^ { n }\) , in keeping with our convention of considering the isomorphism \(d\iota_{p}\) as an identification.
Not formalized. none; no complete checked declaration under strict bundle semantics — Chart derivatives and inverse-chart tangent equivalences exist for Mathlib’s standard TangentSpace; the coordinate vectors here are derivations and their action on local smooth functions is part of the missing bridge/locality theory, so the complete row is not owned. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Convention/notation — smooth manifold
When M is a smooth manifold with boundary and \(p\) is an interior point, the discussion above applies verbatim. For \(p \in \partial M\) ; the only change that needs to be made is to substitute \(\mathbb { H } ^ { n }\) for \(\mathbb { R } ^ { n }\) , with the understanding that the notation \(\partial / \partial x ^ { i } | _ { \varphi ( p ) }\) can be used interchangeably to denote either an element of \(T _ { \varphi ( p ) } \mathbb { R } ^ { n }\) or an element of \(T _ { \varphi ( p ) } \mathbb { H } ^ { n }\) , in keeping with our convention of considering the isomorphism \(d \iota _ { \varphi ( p ) } \colon T _ { \varphi ( p ) } \mathbb { H } ^ { n } \to T _ { \varphi ( p ) } \mathbb { R } ^ { n }\) as an identification. The nth coordinate vector \(\partial / \partial x ^ { n } | _ { p }\) should be interpreted ws.
Not formalized. none; no complete checked declaration under strict bundle semantics — Models with corners formalize boundary tangent spaces, but the one-sided coordinate-derivation convention in Lee’s derivation model is not packaged or bridged to Mathlib’s standard tangent fibre. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Proposition 3.15
Let \(M\) be a smooth \(n\)-manifold with or without boundary and let \(p \in M\). Then \(T_{p}M\) is an \(n\)-dimensional vector space, and for any smooth chart \((U,(x^{i}))\) containing \(p\) the coordinate vectors \(\left.\partial/\partial x^{1}\right|_{p}, \dots, \left.\partial/\partial x^{n}\right|_{p}\) form a basis for \(T_{p}M\).
Not formalized. none; no complete checked declaration under strict bundle semantics — The standard tangent fibre has the model dimension and chart equivalences, but no checked theorem supplies Lee’s coordinate-derivation basis for PointDerivation. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Convention/notation — coordinate basis for
Under the summation convention, with an upper index in a denominator counting as a lower index, the ordered basis \(\left(\left.\partial/\partial x^{i}\right|_{p}\right)\) is called a coordinate basis for \(T_{p}M\), and the numbers \((v^{1},\dots,v^{n})\) are the components of \(v\) with respect to it. The components are recovered from the action of \(v\) on the coordinate functions: for each \(j\), \[ v(x^{j}) = \left(v^{i}\left.\frac{\partial}{\partial x^{i}}\right|_{p}\right)(x^{j}) = v^{i}\frac{\partial x^{j}}{\partial x^{i}}(p) = v^{j}. \]
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked coordinate-derivation basis/components API proves the formula v^j = v(x^j) for Lee’s PointDerivation tangent vectors. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Definition/convention — tangent map
In the differential geometry literature the differential is sometimes called the tangent map, the total derivative, or simply the derivative of \(F\); because it pushes tangent vectors forward from the domain manifold to the codomain, it is also called the (pointwise) pushforward. Different authors denote it by symbols such as \[ F'(p), \quad DF, \quad DF(p), \quad F_{*}, \quad TF, \quad T_{p}F. \] This book writes \(dF_{p}\) for the differential of a smooth map between manifolds, reserving \(DF(p)\) for the total derivative of a map between finite-dimensional vector spaces, identified for Euclidean spaces with the Jacobian matrix.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib uses mfderiv and tangentMap terminology for the standard tangent-space differential, while Lee’s row is a terminology convention for the derivation differential. No separate mathematical theorem is owned by this naming row. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Convention/notation — source terminology/construction
We will stick with the notation \(d F _ { p }\) for the differential of a smooth map between manifolds, and reserve \(D F ( p )\) for the total derivative of a map between finitedimensional vector spaces, which in the case of Euclidean spaces we identify with the Jacobian matrix of \(F\)
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib distinguishes fderiv/mfderiv and has Jacobian infrastructure, but this is Lee-specific notation policy rather than a mathematical interface requiring a route. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Definition/convention — source terminology/construction
Suppose \(( U , \varphi )\) and \(( V , \psi )\) are two smooth charts on \(M ,\) and \(p \in U \cap V\) . Let us denote the coordinate functions of \(\varphi\) by \(\left( x ^ { i } \right)\) and those of by \(\left( \widetilde { x } ^ { i } \right)\) . Any tangent vector at \(p\) can be represented with respect to either basis \(\left( \partial / \partial x ^ { i } | _ { p } \right)\) or \(\left( \partial / \partial \widetilde { x } ^ { i } | _ { p } \right)\) . How are the two representations related? In this situation, it is customary to write the transition map \(\circ \varphi ^ { - 1 } \colon \varphi ( U \cap V ) \to\) \(\psi ( U \cap V )\) in the following shorthand notation:
Not formalized. none; no complete checked declaration under strict bundle semantics — This row is setup prose for change of coordinate bases; no standalone theorem or construction beyond the unbridged coordinate-vector apparatus is asserted. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Convention/notation — source terminology/construction
Here we are indulging in a typical abuse of notation: in the expression tilde(x) ^i ( x ) , we think of tilde(x) ^i as a coordinate function (whose domain is an open subset of M , ; identified with an open subset of ℝ ^n or ℍ ^n ) ; ; but we think of x as representing a point (in this case, in φ ( U ∩ V ) ) . By (3.9), the differential d ( ψ ∘ φ ^- 1 ) _φ ( p ) can be written \[ d(\psi \circ \varphi^{-1})_{\varphi(p)}\left(\frac{\partial}{\partial x^{i}}\bigg|_{\varphi(p)}\right) = \frac{\partial \widetilde{x}^{j}}{\partial x^{i}}(\varphi(p))\, \frac{\partial}{\partial \widetilde{x}^{j}}\bigg|_{\psi(p)}. \]
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has chart transition derivatives for standard tangent spaces, but the displayed coordinate-basis transition formula for derivation tangent vectors is not packaged and depends on the missing bridge. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Example 3.16
The transition map between polar and standard coordinates on suitable open subsets of the plane is \((x,y) = (r\cos\theta,\ r\sin\theta)\). Let \(p \in \mathbb{R}^{2}\) have polar representation \((r,\theta) = (2,\pi/2)\) and let \(v \in T_{p}\mathbb{R}^{2}\) have polar representation \(v = 3\left.\frac{\partial}{\partial r}\right|_{p} - \left.\frac{\partial}{\partial\theta}\right|_{p}\). Since \(\left.\frac{\partial}{\partial\theta}\right|_{p} = -2\sin\!\left(\tfrac{\pi}{2}\right)\left.\frac{\partial}{\partial x}\right|_{p} + 2\cos\!\left(\tfrac{\pi}{2}\right)\left.\frac{\partial}{\partial y}\right|_{p} = -2\left.\frac{\partial}{\partial x}\right|_{p}\), the standard-coordinate representation is \(v = 3\left.\frac{\partial}{\partial y}\right|_{p} + 2\left.\frac{\partial}{\partial x}\right|_{p}\). Each coordinate vector \(\left.\partial/\partial x^{i}\right|_{p}\) depends on the whole coordinate system, not on the single function \(x^{i}\): it differentiates with respect to \(x^{i}\) while the other coordinates are held constant, so changing them can change its direction.
Not formalized. none; no complete checked declaration under strict bundle semantics — Differentiation of polar-coordinate transition maps is available from generic calculus, but no checked declaration packages Lee’s complete numerical polar-coordinate tangent-vector example and its coordinate-basis interpretation. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Definition/convention — tangent bundle of M
Tangent Bundle Often it is useful to consider the set of all tangent vectors at all points of a manifold. Given a smooth manifold M with or without boundary, we define the tangent bundle of M , denoted by TM; to be the disjoint union of the tangent spaces at all points of M : \[ T M = \coprod_ {p \in M} T _ {p} M. \]
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib defines TangentBundle as the bundle of its standard model-space tangent fibres. Lee’s TM in C03 is the disjoint union of derivation-defined tangent spaces; no checked equivalence of these bundle models exists. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Proposition 3.18
Proposition 3.18. For any smooth n-manifold M; the tangent bundle TM has a natural topology and smooth structure that make it into a 2n-dimensional smooth manifold. With respect to this structure, the projection TM M is smooth.
Not formalized. none; no complete checked declaration under strict bundle semantics — Bundle.TotalSpace.isManifold and Bundle.contMDiff_proj give exactly the manifold/smooth-projection theorem for Mathlib’s standard tangent vector bundle, but the source bundle is assembled from Lee’s PointDerivation fibres and the required bundle-level bridge is absent. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Definition/convention — natural coordinates
The coordinates \((x^{i}, v^{i})\) given by (3.13) are called natural coordinates on \(TM\).
Not formalized. none; no complete checked declaration under strict bundle semantics — Tangent-bundle trivializations provide the standard fibre coordinates in Mathlib, but no checked theorem identifies them with Lee’s coordinate derivations/components on the derivation bundle. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Proposition 3.20
If \(M\) is a smooth \(n\)-manifold with or without boundary that can be covered by a single smooth chart, then \(TM\) is diffeomorphic to \(M \times \mathbb{R}^{n}\).
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has tangent-bundle local trivializations and a model-space tangent-bundle diffeomorphism, but no checked theorem gives this global single-chart product diffeomorphism for Lee’s derivation bundle, nor a bridge to the standard tangent bundle. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Convention/notation — global differential
By putting together the differentials of F at all points of M; we obtain a globally defined map between tangent bundles, called the global differential or global tangent map and denoted by \(d F \colon T M \to T N\) This is just the map whose restriction to each tangent space \(T _ { p } M \subseteq T M\) is d \(F _ { p }\) . When we apply the differential of F to a specific vector \(v \in T _ { p } M _ { ☉ }\) ; we can write either d \(F _ { p } ( v )\) or \(d F ( v )\) , depending on how much emphasis we wish to give to the point \(p\) . The former notation is more informative, while the second is more concise.
Not formalized. none; no complete checked declaration under strict bundle semantics — tangentMap bundles the differential on Mathlib’s standard tangent bundle, whereas fdifferential is pointwise on PointDerivation. No checked global total-space map is provided for the derivation bundle used by Lee here. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Proposition 3.21
Proposition 3.21. If \(F \colon M \to N\) is a smooth map, then its global differentia dF TM TN is a smooth \(( x , y )\) denote the standard coordinates on \(\mathbb { R } ^ { 2 }\) .
Not formalized. none; no complete checked declaration under strict bundle semantics — ContMDiff.contMDiff_tangentMap proves smoothness of the standard tangent map, but the source global differential is built from derivation-defined tangent spaces; without the bundle bridge this is an unbridged analogue. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Corollary 3.22
Corollary 3.22 (Properties of the Global Differential). Suppose \(F \colon M \to N\) and \(G \colon N \to P\) are smooth maps. (a) \(d ( G \circ F ) = d G \circ d F .\) (b) \(d ( \mathrm { I d } _ { M } ) = \mathrm { I d } _ { T M } .\) (c) If F is a diffeomorphism, then d \(F \colon T M \to T N\) is also a diffeomorphism, and \(( d F ) ^ { - 1 } = d \big ( F ^ { - 1 } \big )\)
Not formalized. none; no complete checked declaration under strict bundle semantics — The standard tangent-map API proves identity/composition and diffeomorphism functoriality, and fdifferential_comp proves the pointwise derivation chain rule, but no checked global derivation-bundle map packages all clauses of this row. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Convention/notation — dF^{-1} for a diffeomorphism
F ^ { - 1 } )$ Because of part (c) of this corollary, when F is a diffeomorphism we can use the notation \(d F ^ { - 1 }\) unambiguously to mean either \(( d F ) ^ { - 1 }\) or $d ( F ^ { - 1
Not formalized. none; no complete checked declaration under strict bundle semantics — This is notation for the inverse global differential of a diffeomorphism and depends on the unmatched derivation-bundle global differential construction. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Definition/convention — curve in M to be a continuous map
If M is a manifold with or without boundary, we define a curve in M to be a continuous map \(\gamma \colon J \to M\) ; where \(J \subseteq \mathbb { R }\) is an interval. (Most of the time, we will be interested in curves whose domains are open intervals, but for some purposes it is useful to allow J to have one or two endpoints; the definitions all make sense with minor modifications in that case, either by considering J as a manifold with boundary or by interpreting derivatives as one-sided derivatives.) Note that in this book the term curve always refers to a map from an interval into M (a parametrized curve), not just a set of points.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib represents parametrized maps and interval subtypes, but no checked first-class Curve interface matches Lee’s broad continuous-interval convention including endpoint interpretation; this row is primarily source terminology. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Definition/convention — velocity of at t (Fig
Now let M be a smooth manifold, still with or without boundary. Our definition of tangent spaces leads to a natural interpretation of velocity vectors: given a smooth curve J → M and t _0 ∈ J , we define the velocity of at t (Fig. 3.9), denoted by γ ^prime ( t _0 ) , to be the vector \[ \gamma'(t_{0}) = d\gamma\left(\frac{d}{dt}\bigg|_{t_{0}}\right) \in T_{\gamma(t_{0})}M, \] where \(d/dt|_{t_{0}}\) is the standard coordinate basis vector of \(T_{t_{0}}\mathbb{R}\).
Not formalized. none; no complete checked declaration under strict bundle semantics — Manifold derivatives can evaluate a parametrized smooth map, but no checked velocity-vector construction into Lee’s derivation-defined tangent space is packaged. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Proposition 3.23
Proposition 3.23. Suppose M is a smooth manifold with or without boundary and \(p \in M\) Every \(v \in T _ { p } M\) is the velocity of some smooth curve in M .
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked pinned/current theorem states that every tangent vector is the velocity of a smooth curve in the required derivation tangent-space model. The standard tangent API also has no direct existence theorem found by the audit. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Proposition 3.24
Proposition 3.24 (The Velocity of a Composite Curve). Let \(F \colon M \to N\) be a smooth map, and let \(\gamma \colon J \to M\) be a smooth curve. For any \(t _ { 0 } \in J\) , the velocity at \(t = t _ { 0 }\) of the composite curve \(F \circ \gamma \colon J \to N\) is given by \[ (F \circ \gamma) ^ {\prime} (t _ {0}) = d F (\gamma^ {\prime} (t _ {0})). \]
Not formalized. none; no complete checked declaration under strict bundle semantics — The manifold chain rule gives the analogous formula for standard mfderiv, but no checked velocity interface into PointDerivation realizes Lee’s composite-curve statement. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Corollary 3.25
(Computing the Differential Using a Velocity Vector). Suppose \(F \colon M \to N\) is a smooth map, \(p \in M\) and \(v \in T_{p}M\). Then \(dF_{p}(v) = (F \circ \gamma)'(0)\) for any smooth curve \(\gamma \colon J \to M\) with \(0 \in J\), \(\gamma(0) = p\) and \(\gamma'(0) = v\).
Not formalized. none; no complete checked declaration under strict bundle semantics — This corollary depends on U039–U041 and the realization of every derivation tangent vector by a curve; those interfaces are not present as a complete checked route. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Definition/convention — germ of f at p
A smooth function element on M is an ordered pair ( f , U ) , where U is an open subset of M and f : U → ℝ is a smooth function. Given a point p ∈ M ; let us define an equivalence relation on the set of all smooth function elements whose domains contain p by setting ( f , U ) ∼ ( g , V ) ~ i f ~ f equiv g on some neighborhood of p . . The equivalence class of a function element ( f , U ) is called the germ of f at p . . The set of all germs of smooth functions at p is denoted by C _p ^∞ ( M ) It is a real vector space and an associative algebra under the operations \[ c\,[(f,U)] = [(cf,U)], \qquad [(f,U)] + [(g,V)] = [(f+g, U \cap V)], \qquad [(f,U)]\,[(g,V)] = [(fg, U \cap V)]. \]
Formalized. Mathlib/Geometry/Manifold/Sheaf/Smooth.lean::smoothSheafCommRing; Mathlib/Topology/Sheaves/Stalks.lean::TopCat.Presheaf.exists_germ_eq, TopCat.Presheaf.germ_eq — The stalk at p of the sheaf of smooth real-valued functions is exactly the algebra of smooth germs. exists_germ_eq represents every stalk element by a section on a neighborhood, and germ_eq identifies two representatives precisely after restricting to a sufficiently small common neighborhood; the stalk carries the pointwise commutative-ring operations.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Convention/notation — source terminology/construction
(The zero element of this algebra is the equivalence class of the zero function on \(M . )\) Let us denote the germ at \(p\) of the function element \(( f , U )\) simply by \([ f ] _ { p }\) ; there is no need to include the domain \(U\) in the notation, because the same germ is represented by the restriction of \(f\) to any neighborhood of \(p\) . To say that two germs \([ f ] _ { p }\) and \([ g ] _ { p }\) are equal is simply to say that \(f \equiv g\) on some neighborhood of \(p _ { : }\) , however small.
Formalized. Mathlib/Topology/Sheaves/Stalks.lean::TopCat.Presheaf.germ_eq, TopCat.Presheaf.germ_res_apply; Mathlib/Geometry/Manifold/Sheaf/Smooth.lean::smoothSheafCommRing — germ_res_apply makes restriction independent at the stalk, while germ_eq says equality of two germs is witnessed on a common open neighborhood. Together these are exactly Lee’s [f]_p restriction/equality convention.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition/convention — source terminology/construction
A derivation of \(C^{\infty}_{p}(M)\) is a linear map \(v \colon C^{\infty}_{p}(M) \to \mathbb{R}\) satisfying the product rule analogous to (3.4): \[ v[fg]_{p} = f(p)\,v[g]_{p} + g(p)\,v[f]_{p}. \]
Not formalized. none; no complete checked declaration under strict bundle semantics — The smooth-function stalk and its evaluation map are formalized, and generic Derivation is formalized, but the pin does not package the required real-algebra/module structures turning a smooth stalk at p into Lee’s first-class space of ℝ-linear point derivations. The ingredients are not promoted without that exact assembly. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Definition/convention — equivalence relation
Suppose \(p\) is a point of M . We wish to define an equivalence relation on the set of all smooth curves of the form \(\gamma \colon J \to M\) ; where J is an interval containing 0 and \(\gamma ( 0 ) = p\) . Given two such curves \(\gamma _ { 1 } \colon J _ { 1 } \to M\) and \(\gamma _ { 2 } \colon J _ { 2 } \to M .\) ; let us say that \(\gamma _ { 1 } \sim \gamma _ { 2 }\) if \(( f \circ \gamma _ { 1 } ) ^ { \prime } ( 0 ) = ( f \circ \gamma _ { 2 } ) ^ { \prime } ( 0 )\) for every smooth real-valued function \(f\) defined in a neighborhood of \(p\) . Let \(\mathfrak { V } _ { p } M\) denote the set of equivalence classes. The tangent space to M at \(p\) is often defined to be the set \(\mathfrak{V}_{p}M\) of such equivalence classes.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked quotient/equivalence-class-of-curves construction identifies tangent vectors by equality of all local smooth-function derivatives, nor a theorem identifies that quotient with PointDerivation. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Definition/convention — objects of C
A category C consists of the following things: a class Ob.C/, whose elements are called objects of , a class Hom.C/, whose elements are called morphisms of , for each morphism \(f \in { \mathrm { H o m } } ( \mathsf { C } )\) , two objects X; \(Y \in \mathrm { O b } ( \mathsf { C } )\) called the source and target of f , respectively, for each triple \(X , Y , Z \in \mathrm { O b } ( { \mathsf { C } } )\) , a mapping called composition: \[ \operatorname{Hom} _ {\mathbb {C}} (X, Y) \times \operatorname{Hom} _ {\mathbb {C}} (Y, Z) \to \operatorname{Hom} _ {\mathbb {C}} (X, Z), \] written \(( f , g ) \mapsto g \circ f\) , where \({ \mathrm { H o m } } _ { \mathsf { C } } ( X , Y )\) denotes the class of all morphisms with source X and target Y . The morphisms are required to satisfy the following axioms: (i) ASSOCIATIVITY: .f g/ h f .g h/. (ii) EXISTENCE OF IDENTITIES: For each object \(X \in \mathrm { O b } ( \mathsf C )\) , there exists an identity morphism \(\operatorname { I d } _ { X } \in \operatorname { H o m } _ { \mathbb { C } } ( X , X )\) , such that IdY \(\circ f = f = f \circ \operatorname { I d } _ { X }\) for all \(f \in { \mathrm { H o m } } _ { \mathsf { C } } ( X , Y ) .\) A morphism \(f \in { \mathrm { H o m } } _ { \mathsf { C } } ( X , Y )\) is called an isomorphism in if there exists a morphism \(g \in { \mathrm { H o m } } _ { \mathsf { C } } ( Y , X )\) such that \(f \circ g = \operatorname { I d } _ { Y }\)
Formalized. Mathlib/CategoryTheory/Category/Basic.lean::CategoryStruct, Category — CategoryStruct packages hom-types, identities, and composition; Category adds left/right identity and associativity laws. This is exactly Lee’s category data and axioms, represented universe-polymorphically.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition/convention — isomorphism in C
\(f \in { \mathrm { H o m } } _ { \mathsf { C } } ( X , Y ) .\) A morphism \(f \in { \mathrm { H o m } } _ { \mathsf { C } } ( X , Y )\) is called an isomorphism in if there exists a morphism \(g \in { \mathrm { H o m } } _ { \mathsf { C } } ( Y , X )\) such that \(f \circ g = \operatorname { I d } _ { Y }\) and \(g \circ f = \operatorname { I d } _ { X }\)
Formalized. Mathlib/CategoryTheory/Iso.lean::CategoryTheory.Iso — Iso X Y bundles forward and inverse morphisms with the two inverse identities, exactly Lee’s categorical isomorphism.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Example 3.26
(Categories). In most of the categories that one meets “in nature,” the objects are sets with some extra structure, the morphisms are maps that preserve that structure, and the composition laws and identity morphisms are the obvious ones. Some of the categories of this type that appear in this book (implicitly or explicitly) are listed below. In each case, we describe the category by giving its objects and its morphisms.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib contains many of the individual concrete categories alluded to in Lee’s example, but this row is explanatory prose/listing rather than one mathematical interface, and no single checked object owns the complete example list under whole-row semantics. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Definition/convention — pointed set and pointed map
There are also important categories whose objects are sets with distinguished base points, in addition to (possibly) other structures. A pointed set is an ordered pair .X; p/, where X is a set and p is an element of X. Other pointed objects such as pointed topological spaces or pointed smooth manifolds are defined similarly. If \(( X , p )\) and \(( X ^ { \prime } , p ^ { \prime } )\) are pointed sets (or topological spaces, etc.), a map \(F \colon X \to\) X is said to be a pointed map if \(F ( p ) = p ^ { \prime } ;\) in this case, we write \(F \colon ( X , p ) \to\) \(( X ^ { \prime } , p ^ { \prime } )\) . Here are some important examples of categories of pointed objects. ●
Not formalized. none; no complete checked declaration under strict bundle semantics — CategoryTheory.Pointed exactly packages pointed sets and basepoint-preserving maps, and pointed topological infrastructure exists separately, but no checked pointed-smooth-manifold category packages the whole multi-context row as stated. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Definition/convention — small and locally small categories
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. For example, in the category Set, Ob.Set/ is the class of all sets; any attempt to treat it as a set in its own right leads to the well-known Russell paradox of set theory. (See [LeeTM, Appendix A] or almost any book on set theory for more.) Even though the classes of objects and morphisms might not constitute sets, we still use notations such as \(X \in \mathrm { O b } ( \mathsf C )\) and \(f \in { \mathrm { H o m } } ( \mathsf { C } )\) to indicate that X is an object and f is a morphism in C. A category in which both Ob.C/ and Hom.C/ are sets is called a small category, and one in which each class of morphisms \({ \mathrm { H o m } } _ { \mathsf { C } } ( X , Y )\) is a set is called locally small. All the categories listed abov say that two germs \([ f ] _ { p }\) and \([ g ] _ { p }\) are equal is simply to say that \(f \equiv g\) on some neighborhood of \(p _ { : }\) , however small.
Formalized. Mathlib/CategoryTheory/Category/Basic.lean::SmallCategory; Mathlib/CategoryTheory/EssentiallySmall.lean::CategoryTheory.LocallySmall — SmallCategory makes both objects and homs live in one small universe, while LocallySmall asserts smallness of every hom-type. These are the universe-polymorphic formalizations of Lee’s small and locally small categories.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition/convention — covariant functor
If \(\mathsf{C}\) and \(\mathsf{D}\) are categories, a covariant functor from \(\mathsf{C}\) to \(\mathsf{D}\) assigns to each object \(X \in \operatorname{Ob}(\mathsf{C})\) an object \(F(X) \in \operatorname{Ob}(\mathsf{D})\), and to each morphism \(f \in \operatorname{Hom}_{\mathsf{C}}(X,Y)\) a morphism \(F(f) \in \operatorname{Hom}_{\mathsf{D}}(F(X),F(Y))\), preserving identities and composition: \[ F(\operatorname{Id}_{X}) = \operatorname{Id}_{F(X)}, \qquad F(g \circ h) = F(g) \circ F(h). \]
Formalized. Mathlib/CategoryTheory/Functor/Basic.lean::CategoryTheory.Functor — Functor C D consists of object and morphism maps with preservation of identity and composition, exactly Lee’s covariant-functor definition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition/convention — contravariant functor
\[ We also need to consider functors that reverse morphisms: a contravariant functor from to is a rule $\mathcal { F }$ that assigns to each object $X \in { \mathrm { O b } } ( \mathsf C )$ an object ${ \mathcal { F } } ( X ) \in { \mathrm { O b } } ( \mathsf { D } )$ , and to each morphism $f \in { \mathrm { H o m } } _ { \mathsf { C } } ( X , Y )$ a morphism $\mathcal { F } ( f ) \in$ $\mathrm { H o m } _ { \mathsf { D } } ( { \mathcal F } ( Y ) , { \mathcal F } ( X ) )$ , such that \] ( _ {X}) = _ { (X)}; alytic manifolds.
Formalized. Mathlib/CategoryTheory/Functor/Basic.lean::CategoryTheory.Functor; Mathlib/CategoryTheory/Opposites.lean::CategoryTheory.Functor.op — A contravariant functor from C to D is represented canonically as a covariant functor Cᵒᵖ ⥤ D; Mathlib’s opposite-category/functor API reverses morphisms and composition exactly as in Lee’s definition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition/convention — covariant functor
One trivial example of a covariant functor is the identity functor from any category to itself: it takes each object and each morphism to itself. Another example is the forgetful functor: if C is a category whose objects are sets with some additional structure and whose morphisms are maps preserving that structure (as are all the categories listed in the first part of Example 3.26 except Set itself), the forgetful functor \(\mathcal { F } \colon \mathsf { C } \to\) Set assigns to each object its underlying set, and to each morphism the same map thought of as a m
Formalized. Mathlib/CategoryTheory/Functor/Basic.lean::CategoryTheory.Functor.id; Mathlib/CategoryTheory/ConcreteCategory/Forget.lean::CategoryTheory.forget — Functor.id is the identity functor. For every concrete category, CategoryTheory.forget sends each structured object to its underlying type and each morphism to its underlying function, exactly Lee’s two examples.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition/convention — source terminology/construction
More interesting functors arise when we associate “invariants” to classes of mathematical objects. For example, the fundamental group is a covariant functor from \(\mathsf { T o p } _ { * }\) to Grp. The results of Problem 2-10 show that there is a contravariant functor from Diff to VecR defined by assigning to each smooth manifold space \(C ^ { \infty } ( M )\) , and to each smooth map \(F \colon M \to N\) the } ( N ) C ^ { } ( M )$ defined by $
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib has the fundamental groupoid functor and generic smooth-function composition, but no checked route packages both Lee examples: the pointed-space fundamental-group functor to groups and the contravariant smooth-function functor from the category of smooth manifolds. Whole-row semantics reject the partial matches. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Definition/convention — functor
by \(F ^ { * } ( f ) = f \circ F\) The discussion in this chapter has given us some other important examples of functors. First, the tangent space functor is a covariant functor from the category Diff of pointed smooth manifolds to the category VecR of real vector spaces. To each pointed smooth manifold \(( M , p )\) it assigns the tangent space \(T _ { p } M _ { \mathrm { \ell } }\) ; and to each pointed smooth map \(F \colon ( M , p ) ( N , F ( p ) )\) it assigns the differential d \(F _ { p }\) The fact that this is a functor is the content of parts (b) and (c) of Proposi
Not formalized. none; no complete checked declaration under strict bundle semantics — fdifferential has the required pointwise identity/composition laws, but Mathlib does not package the category of pointed smooth manifolds and the resulting tangent-space functor to real vector spaces; the source functor is therefore not an existing checked interface. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.
Definition/convention — tangent functor
Proposition 3.6. Similarly, we can think of the assignments \(M \mapsto T M\) and \(F \mapsto d F\) (sending each smooth manifold to its tangent bundle and each smooth map to its global differential) as a covariant functor from Diff to itself, called the tangent functor.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has TangentBundle, tangentMap, and their functorial laws, but no checked category of smooth manifolds with a bundled tangent endofunctor, and the standard tangent bundle is moreover unbridged to Lee’s derivation bundle in this chapter. Strict bundle semantics reject a proper subset, an unbridged equivalent model, terminology-only analogy, or reconstruction of the substantive source theorem.