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

FC08 — Lee, Introduction to Smooth Manifolds.

This chapter contains 18 definitions, 2 theorems, 6 propositions, 1 lemma, 3 corollaries, 11 examples, 3 constructions and 3 conventions.

Of the 47 statements checked against Lean, 3 are formalized somewhere and 44 are not.

Status	Statements	Share	What it means
not formalized	44	94%	A documented search found no Lean statement of it anywhere.
in Mathlib	3	6%	Mathlib states and proves it.
checked in total	47

Which versions of Lean and Mathlib were searched

Canonical source block: FC08 Lee, Chapter 13, FC08-C13-U001–FC08-C13-U047, exactly 47 unique contiguous rows retrieved from FC08 — John M. Lee, Introduction to Smooth Manifolds through agent-memory.
Search order: project at A=3b2239e161592472b34e02ad3b7da308f9ce7280, pinned Mathlib P=db584cd6d46c92f209a44c0f1c829460d327499d (Apache-2.0, Lean 4.33.0), current upstream H=5315eef9e4ffb98e0f89f278b765c50a149f66ca (Apache-2.0, Lean 4.34.0-rc2), then targeted indexed/external Lean searches. No project-existing, package-import, or reference-port owner survived strict whole-row checking.
C13 has 3 pinned mathlib rows and 44 dated unmatched rows. Positive rows are: U037, U038, U046.
The controlling boundary is inherited from C03 and used consistently in C08/C11/C12. Lee’s tangent spaces in FC08 are the point-derivation model. Mathlib’s mature Riemannian manifold files explicitly build on TangentSpace I x; exact P/H searches still find no checked PointDerivation ≃ TangentSpace. Therefore the otherwise strong standard-tangent Riemannian metric, path-length, distance, orthonormal-frame, pullback, musical, and gradient APIs are adjacency evidence only, not routes for U001–U036 or U039–U045.
Submanifold and normal-bundle rows U022–U029 also inherit C05’s missing general immersed/embedded submanifold layer. Generic Riemannian vector-bundle infrastructure does not repair the absent source tangent/submanifold objects.
U037 is independent of Riemannian tangent semantics: TopologicalSpace.MetrizableSpace is exactly Lee’s topological definition. U038 is directly proved by Manifold.metrizableSpace, so metrizability survives even though Lee derives it from Riemannian distance.
U046 is likewise tangent-independent algebra. LinearMap.BilinForm.Nondegenerate and toDual supply the nondegenerate bilinear form and induced V ≃ₗ V*. For symmetric real forms, QuadraticMap.associated_left_inverse transports to quadratic-form language, QuadraticForm.equivalent_one_neg_one_weighted_sum_squared gives Sylvester diagonalization, and sigPos/sigNeg with their equivalence theorems give the basis-independent signature counts. /tmp/fc08-c13-witness.lean compiled the nondegenerate symmetric-form-to-±1 diagonalization bridge at exact P.
U047 remains unmatched: neither P nor H contains a manifold-level pseudo-Riemannian/Lorentz metric structure with smoothness and constant signature. The algebraic signature package alone is only a proper subset.
Targeted external/indexed searches did not surface a compatible Lean owner for the missing point-derivation Riemannian bridge or Lorentz/pseudo-Riemannian manifold layer.
N=2026-09-07 marks dated unmatched decisions. Strict whole-row semantics apply uniformly.

Definition/convention — Riemannian metric

FC08-C13-U001 · Ch. 13, § Riemannian Manifolds; source L9788 · not formalized

Transferring these ideas to manifolds, we obtain one of the most important applications of tensors to differential geometry. Let M be a smooth manifold with or without boundary. A Riemannian metric on M is a smooth symmetric covariant 2-tensor field on M that is positive definite at each point. A Riemannian manifold is a pair $( M , g )$ , where M is a smooth manifold and $g$ is a Riemannian metric on M . One sometimes simply says “M is a Riemannian manifold” if M is understood to be endowed with a specific Riemannian metric. A Riemannian manifold with boundary is defined similarly.

Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has substantial Riemannian-manifold, path-length, and distance infrastructure, but it is formulated on the standard TangentSpace. FC08 C03 fixed Lee’s tangent spaces to the point-derivation model, and exact P/H searches still find no PointDerivation ≃ TangentSpace bridge. This source row therefore cannot be identified with the standard-tangent theorem under strict semantics. Strict whole-row semantics reject proper subsets, unproved converse directions, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.

Definition/convention — Riemannian metric

FC08-C13-U002 · Ch. 13, § Riemannian Manifolds; source L9792 · not formalized

Note that a Riemannian metric is not the same thing as a metric in the sense of metric spaces, although the two concepts are related, as we will see below. Because of this ambiguity, we usually use the term “distance function” for a metric in the metric space sense, and reserve “metric” for a Riemannian metric. In any event, which type of metric is being considered should always be clear from the context.

Convention/notation — source terminology/construction

FC08-C13-U003 · Ch. 13, § Riemannian Manifolds; source L9794 · not formalized

If $g$ is a Riemannian metric on $M$, then for each $p \in M$ the 2-tensor $g_{p}$ is an inner product on $T_{p}M$; accordingly $\langle v,w \rangle_{g}$ denotes $g_{p}(v,w)$ for $v, w \in T_{p}M$.

Example 13.1

FC08-C13-U004 · Ch. 13, § Riemannian Manifolds; source L9808 · not formalized

Proposition 12.15(b) }). \end{array} \[ Example 13.1 (The Euclidean Metric). The simplest example of a Riemannian metric is the Euclidean metric $\overline { { g } }$ on $\mathbb { R } ^ { n }$ , given in standard coordinates by \] = _ {i j} d x ^ {i} d x ^ {j}, \[ where $\delta _ { i j }$ is the Kronecker delta. It is common to abbreviate the symmetric product of a tensor ˛ with itself by $\alpha ^ { 2 }$ , so the Euclidean metric can also be written \] = (d x ^ {1}) ^ {2} + + (d x ^ {n}) ^ {2}. \[ Applied to vectors v; $w \in T _ { p } \mathbb { R } ^ { n }$ , this yields \] _ {p} (v, w) = _ {i j} v ^ {i} w ^ {j} = _ {i = 1} ^ {n} v ^ {i} w ^ {i} = v w. \[ In other words, $\overline { { g } }$ is the 2-tensor field whose value at each point is the Euclidean dot product. (As you may recall, we warned in Chapter 1 that expressions involving the Euclidean dot product are likely to violate our index conventions and therefore to require explicit summation signs. This can usually be avoided by writing the metric coefficients $\delta _ { i j }$ explicitly, as in $\delta _ { i j } v ^ { i } w ^ { j } . )$ Example 13.2 (Product Metrics). If $( M , g )$ and $( \widetilde M , \widetilde g )$ are Riemannian manifolds, we can define a Riemannian metric $\widehat g = g \oplus \widetilde g$ on the product manifold $M \times \widetilde M$ , called the product metric, as follows: \]

Example 13.2

FC08-C13-U005 · Ch. 13, § Riemannian Manifolds; source L9828 · not formalized

(Product Metrics). If $(M,g)$ and $(\widetilde{M},\widetilde{g})$ are Riemannian manifolds, the product metric $\widehat{g} = g \oplus \widetilde{g}$ on $M \times \widetilde{M}$ is \[ \widehat{g}\big((v,\widetilde{v}),(w,\widetilde{w})\big) = g(v,w) + \widetilde{g}(\widetilde{v},\widetilde{w}) \tag{13.1} \] for $(v,\widetilde{v}), (w,\widetilde{w}) \in T_{p}M \oplus T_{q}\widetilde{M} \cong T_{(p,q)}(M \times \widetilde{M})$. In local coordinates $(x^{1},\dots,x^{n},y^{1},\dots,y^{m})$ it is the block diagonal matrix $(\widehat{g}_{ij}) = \begin{pmatrix} g_{ij} & 0 \\ 0 & \widetilde{g}_{ij} \end{pmatrix}$. For example, the Euclidean metric on $\mathbb{R}^{n+m}$ is the product of the Euclidean metrics on $\mathbb{R}^{n}$ and $\mathbb{R}^{m}$.

Proposition 13.3

FC08-C13-U006 · Ch. 13, § Riemannian Manifolds; source L9844 · not formalized

another approach, see Problem 13-18.) Proposition 13.3 (Existence of Riemannian Metrics). Every smooth manifold with or without boundary admits a Riemannian metric. P

Definition/convention — source terminology/construction

FC08-C13-U007 · Ch. 13, § Riemannian Manifolds; source L9864 · not formalized

The length or norm of a tangent vector $v \in T _ { p } M$ is defined to be \[ | v | _ {g} = \langle v, v \rangle_ {g} ^ {1 / 2} = g _ {p} (v, v) ^ {1 / 2}. \]

Definition/convention — source terminology/construction

FC08-C13-U008 · Ch. 13, § Riemannian Manifolds; source L9870 · not formalized

The angle between two nonzero tangent vectors $v, w \in T_{p}M$ is the unique $\theta \in [0,\pi]$ satisfying \[ \cos\theta = \frac{\langle v,w \rangle_{g}}{|v|_{g}\,|w|_{g}}. \] Tangent vectors are orthogonal if $\langle v,w \rangle_{g} = 0$, which means that one of them is zero or the angle between them is $\pi/2$.

Definition/convention — orthogonal

FC08-C13-U009 · Ch. 13, § Riemannian Manifolds; source L9876 · not formalized

Tangent vectors $v , w \in T _ { p } M$ are said to be orthogonal if $\langle v , w \rangle _ { g } = 0$ . This means either one or both vectors are zero, or the angle between them is $\pi / 2$

Definition/convention — source terminology/construction

FC08-C13-U010 · Ch. 13, § Riemannian Manifolds; source L9878 · not formalized

One highly useful tool for the study of Riemannian manifolds is orthonormal frames. Let $( M , g )$ be an n-dimensional Riemannian manifold with or without boundary. Just as we did for the case of R in Chapter 8, we say that a local frame $( E _ { 1 } , \ldots , E _ { n } )$ for M on an open subset $U \subseteq M$ is an orthonormal frame if the vectors $( E _ { 1 } | _ { p } , \ldots , E _ { n } | _ { p } )$ form an orthonormal basis for $T _ { p } M$ at each point $p \in U$ , or equivalently if $\langle \bar { E _ { i } } , \bar { E _ { j } } \rangle _ { g } = \delta _ { i j }$

Example 13.4

FC08-C13-U011 · Ch. 13, § Riemannian Manifolds; source L9880 · not formalized

Example 13.4. The coordinate frame $\left( { \partial } / { \partial x ^ { i } } \right)$ is a global orthonormal frame for $\mathbb { R } ^ { n }$ with the Euclidean

Example 13.5

FC08-C13-U012 · Ch. 13, § Riemannian Manifolds; source L9882 · after FC08-C08-U019, FC08-C09-U063 · not formalized

Example 13.5. The frame $( E _ { 1 } , E _ { 2 } )$ on $\mathbb { R } ^ { 2 } \setminus \{ 0 \}$ defined in Example 8.12 is a local orthonormal frame for $\mathbb { R } ^ { 2 }$ . As we observed in Example 9.45, it is not a coordinate frame in any coord {1}{k !} _ {S _ {k}} (v _ {(1)}, , v _ {(k)}).

Proposition 13.6

FC08-C13-U013 · Ch. 13, § Riemannian Manifolds; source L9886 · not formalized

Proposition 13.6. Suppose $( M , g )$ is a Riemannian manifold with or without boundary, and $( X _ { j } )$ is a smooth local frame for M over an open $U \subseteq M$ . Then there is a smooth orthonormal frame $( E _ { j } )$ over U such that span $\left( E _ { 1 } | _ { p } , \dots , E _ { j } | _ { p } \right) = \operatorname { s p a n } \left( X _ { 1 } | _ { p } , \dots , X _ { j } | _ { p } \right)$

Corollary 13.8

FC08-C13-U014 · Ch. 13, § Riemannian Manifolds; source L9890 · not formalized

Corollary 13.8 (Existence of Local Orthonormal Frames). Let $( M , g )$ be a Riemannian manifold with or without boundary. For each $p \in M$ ; there is a smooth orthonormal frame on a neighborhood of $p$.

Construction/definition — pullback metric determined by F

FC08-C13-U015 · Ch. 13, § Pullback Metrics; source L9898 · not formalized

Suppose M; N are smooth manifolds with or without boundary, $g$ is a Riemannian metric on N , and $F \colon M \to N$ is smooth. The pullback $F ^ { * } g$ is a smooth 2-tensor field on M . If it is positive definite, it is a Riemannian metric on M; called the pullback metric determined by F . The next proposition shows when this is the ca symmetrization operator, it is possible to define a new product that takes a pair of symmetric tensors and yields another symmetric tensor.

Proposition 13.9

FC08-C13-U016 · Ch. 13, § Pullback Metrics; source L9903 · not formalized

Proposition 13.9 (Pullback Metric Criterion). Suppose $F \colon M \to N$ is a smooth map and g is a Riemannian metric on N . Then $F ^ { * } g$ is a Riemannian metric on M $i f$ and only if F is a smooth immersion.

Example 13.11

FC08-C13-U017 · Ch. 13, § Pullback Metrics; source L9909 · after FC08-C04-U022 · not formalized

The smooth map $F \colon \mathbb{R}^{2} \to \mathbb{R}^{3}$, $F(u,v) = (u\cos v,\ u\sin v,\ v)$, is a proper injective smooth immersion, hence an embedding by Proposition 4.22; its image is the helicoid. Substituting into $\overline{g}$ gives the pullback metric \[ F^{*}\overline{g} = (\cos v\,du - u\sin v\,dv)^{2} + (\sin v\,du + u\cos v\,dv)^{2} + dv^{2} = du^{2} + (u^{2}+1)\,dv^{2}. \] By convention $du^{2}$ means the symmetric product $du\,du$, not $d(u^{2})$.

Example 13.12

FC08-C13-U018 · Ch. 13, § Pullback Metrics; source L9925 · not formalized

In polar coordinates the Euclidean metric $\overline{g} = dx^{2} + dy^{2}$ on $\mathbb{R}^{2}$ becomes, on substituting $x = r\cos\theta$ and $y = r\sin\theta$, \[ \overline{g} = (\cos\theta\,dr - r\sin\theta\,d\theta)^{2} + (\sin\theta\,dr + r\cos\theta\,d\theta)^{2} = dr^{2} + r^{2}\,d\theta^{2}. \] For Riemannian manifolds $(M,g)$ and $(\widetilde{M},\widetilde{g})$, a smooth map $F \colon M \to \widetilde{M}$ is a Riemannian isometry if it is a diffeomorphism with $F^{*}\widetilde{g} = g$, and a local isometry if every $p \in M$ has a neighborhood $U$ with $F|_{U}$ an isometry onto an open subset of $\widetilde{M}$ — equivalently, if $F$ is a local diffeomorphism with $F^{*}\widetilde{g} = g$. Manifolds admitting an isometry are isometric, and the study of properties invariant under isometries is Riemannian geometry. One such property is flatness: $(M,g)$ is flat, and $g$ a flat metric, if it is locally isometric to $(\mathbb{R}^{n},\overline{g})$.

Definition/convention — isometric and locally isometric Riemannian manifolds

FC08-C13-U019 · Ch. 13, § Pullback Metrics; source L9933 · not formalized

If there exists a Riemannian isometry between ( M , g ) and ( widetilde M , widetilde g ) , we say that they are isometric as Riemannian manifolds. If each point of M has a neighborhood that is isometric to an open subset of ( tilde(M) , tilde(g) ) , then we say that ( M , g ) is locally isometric to ( tilde(M) , tilde(g) ) . The study of properties of Riemannian manifolds that are invariant under (local or global) isometries is called Riemannian geometry.

Definition/convention — flat Riemannian manifold and flat metric

FC08-C13-U020 · Ch. 13, § Pullback Metrics; source L9935 · not formalized

A Riemannian $n$-manifold $(M,g)$ is a flat Riemannian manifold, and $g$ a flat metric, if $(M,g)$ is locally isometric to $(\mathbb{R}^{n},\overline{g})$.

Theorem 13.14

FC08-C13-U021 · Ch. 13, § Pullback Metrics; source L9941 · not formalized

Theorem 13.14. For a Riemannian manifold $( M , g )$ , the following are equivalent: (a) g is flat. (b) Each point of M is contained in the domain of a smooth coordinate chart in which g has the coordinate representation $g = \delta _ { i j } d x ^ { i } d x ^ { j }$ (c) Each point of M is contained in the domain of a smooth coordinate chart in which the coordinate frame is orthonormal. (d) Each point of M is contained in the domain of a commuting orthonormal frame.

Construction/definition — induced metric

FC08-C13-U022 · Ch. 13, § Riemannian Submanifolds; source L9965 · not formalized

Submanifolds Pullback metrics are especially important for submanifolds. If $( M , g )$ is a Riemannian manifold with or without boundary, every submanifold $S \subseteq M$ (immersed or embedded, with or without boundary) automatically inherits a pullback metric $\iota ^ { * } g$ where S M$ is inclusion. In this setting, the pullback metric is also called the induced metric on S. By definition, this means for v; $ $d \iota _ { p } \colon T _ { p } S \to T _ { p } M$ is our usual identification of $T _ { p } S$ as a subspace of $T _ { p } M$ Thus $\iota ^ { * } g$ is just the restriction of $g$ to pairs of vectors tangent to S . With this metric, S is called a Riemannian submanifold } (M) = (T ^ {k} T ^ {*} M).

Not formalized. none; no complete checked declaration under strict bundle semantics — This row requires Lee’s Riemannian tangent geometry together with an immersed/embedded submanifold or normal-bundle layer. C05 has no checked general submanifold object, and the C03 point-derivation tangent model remains unbridged from Mathlib’s standard TangentSpace; the mature standard-tangent Riemannian/submanifold ingredients therefore cannot own the source row. Strict whole-row semantics reject proper subsets, unproved converse directions, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.

Example 13.16

FC08-C13-U023 · Ch. 13, § Riemannian Submanifolds; source L9973 · not formalized

The metric $\mathring{g} = \iota^{*}\overline{g}$ induced on $\mathbb{S}^{n}$ by the inclusion $\iota \colon \mathbb{S}^{n} \hookrightarrow \mathbb{R}^{n+1}$ is called the round metric, or standard metric, on the sphere.

Example 13.17

FC08-C13-U024 · Ch. 13, § Riemannian Submanifolds; source L9977 · not formalized

Example 13.17 (Induced Metrics in Graph Coordinates). Let $U \subseteq \mathbb { R } ^ { n }$ be an open subset, and let $S \subseteq \mathbb { R } ^ { n + 1 }$ be the graph of a smooth function $f \colon U \to \mathbb { R }$ The map $X \colon U \to \mathbb { R } ^ { n + 1 }$ given by $X { \big ( } u ^ { 1 } , \ldots , u ^ { n } { \big ) } = { \big ( } u ^ { 1 } , \ldots , u ^ { n } , f ( u ) { \big ) }$ is a smooth global parametrization of S and the induced metric on S is given in graph coordinates by \[ X ^ {*} \bar {g} = X ^ {*} \left(\left(d x ^ {1}\right) ^ {2} + \dots + \left(d x ^ {n + 1}\right) ^ {2}\right) = \left(d u ^ {1}\right) ^ {2} + \dots + \left(d u ^ {n}\right) ^ {2} + d f ^ {2}. \] For example, the upper hemisphere of $\mathbb { S } ^ { 2 }$ is parametrized by the map $X \colon \mathbb { B } ^ { 2 } \to \mathbb { R } ^ { 3 }$ given by \[ X (u, v) = \left(u, v, \sqrt {1 - u ^ {2} - v ^ {2}}\right). \] In these coordinates, the round metric can be written \[ \begin{array}{c} \stackrel {\circ} {g} = X ^ {*} \overline {{g}} = d u ^ {2} + d v ^ {2} + \left(\frac {u d u + v d v}{\sqrt {1 - u ^ {2} - v ^ {2}}}\right) ^ {2} \\ = \frac {(1 - v ^ {2}) d u ^ {2} + (1 - u ^ {2}) d v ^ {2} + 2 u v d u d v}{1 - u ^ {2} - v ^ {2}}. \end{array} \]

Example 13.18

FC08-C13-U025 · Ch. 13, § Riemannian Submanifolds; source L9995 · after FC08-C05-U026 · not formalized

Example 13.18 (Induced Metrics on Surfaces of Revolution). Let C be an embedded 1-dimensional submanifold of the half-plane $\{ ( r , z ) : r > 0 \}$ , and let $S _ { C }$ be the surface of revolution generated by C as described in Example 5.17. To compute the induced metric on $S _ { C }$ , choose any smooth local parametrization $\gamma ( t ) =$ $\bigl ( a ( t ) , b ( t ) \bigr )$ for $C$ , and note that the map $X ( t , \theta ) = { \big ( } a ( t ) \cos \theta , a ( t ) \sin \theta , b ( t ) { \big ) }$ yields a smooth local parametrization of $S _ { C }$ , provided that $( t , \theta )$ is restricted to a sufficiently small open subset of the plane. Thus we can compute \[ \begin{array}{r l} X ^ {*} \overline {{g}} & = d (a (t) \cos \theta) ^ {2} + d (a (t) \sin \theta) ^ {2} + d (b (t)) ^ {2} \\ & = (a ^ {\prime} (t) \cos \theta d t - a (t) \sin \theta d \theta) ^ {2} \\ & \quad + (a ^ {\prime} (t) \sin \theta d t + a (t) \cos \theta d \theta) ^ {2} + (b ^ {\prime} (t) d t) ^ {2} \\ & = (a ^ {\prime} (t) ^ {2} + b ^ {\prime} (t) ^ {2}) d t ^ {2} + a (t) ^ {2} d \theta^ {2}. \end{array} \] In particular, $\mathrm { i f } \gamma$ is a unit-speed curve, meaning that $| \gamma ^ { \prime } ( t ) | ^ { 2 } = a ^ { \prime } ( t ) ^ { 2 } + b ^ { \prime } ( t ) ^ { 2 } = 1$ this reduces to the simple formula $d t ^ { 2 } + a ( t ) ^ { 2 } d \theta ^ { 2 }$ Here are some familiar examples of surfaces of revolution. (a) The embedded torus described in Example 5.17 is the surface of revolution generated by the circle $( r - 2 ) ^ { 2 } + z ^ { 2 } = 1$ . Using the unit-speed parametrization $\gamma ( t ) = ( 2 + \cos t , \sin t )$ for the circle, we obtain the formula $d t ^ { 2 } + ( 2 + \cos t ) ^ { 2 } d \theta ^ { 2 }$ for the induced metric. (b) The unit sphere (minus the north and south poles) is a surface of revolution whose generating curve is the semicircle parametrized by $\gamma ( t ) = ( \sin t , \cos t )$ for $0 < t < \pi$ . The induced metric is $d t ^ { 2 } + \sin ^ { 2 } t d \theta ^ { 2 }$ (c) The unit cylinder $x ^ { 2 } + y ^ { 2 } = 1$ is a surface of revolution whose generating curve is the vertical line parametrized by $\gamma ( t ) = ( 1 , t )$ for $t \in \mathbb { R }$ . The induced metric write $X _ { i } = X _ { i } ^ { j } \partial / \partial x ^ { j }$ , where the component functions $X _ { i } ^ { j }$ all vanish at p.

Proposition 13.19

FC08-C13-U026 · Ch. 13, § Riemannian Submanifolds; source L10017 · not formalized

Proposition 13.19 (Flatness Criterion for Surfaces of Revolution). Let $C \subseteq H$ be a connected embedded 1-dimensional submanifold of the half-plane $H = \{ ( r , z )$ $r > 0 \}$ , and let $S _ { C }$ be the surface of revolution generated by C . The induced metric on $S _ { C }$ is flat if and only $i f C$ is part of a straight line.

Corollary 13.20

FC08-C13-U027 · Ch. 13, § Riemannian Submanifolds; source L10063 · not formalized

The round metric on $\mathbb{S}^{2}$ is not flat.

Construction/definition — source terminology/construction

FC08-C13-U028 · Ch. 13, § The Normal Bundle; source L10067 · after FC08-C10-U051 · not formalized

Suppose $( M , g )$ is an n-dimensional Riemannian manifold with or without boundary, and $S \subseteq M$ is a k-dimensional Riemannian submanifold (also with or without boundary). Just as we did for submanifolds of R, for any $p \in S$ we say that a vector $v \in T _ { p } M$ is normal to S if v is orthogonal to every vector in $T _ { p } S$ with respect to the inner product $\langle \cdot , \cdot \rangle _ { g }$ . The normal space to S at $\pmb { p }$ is the subspace $N _ { p } S \subseteq T _ { p } M$ consisting of all vectors that are normal to S at $p$ , and the normal bundle of S is the subset $N S \subseteq T M$ consisting of the union of all the normal spaces at points of S . The projection $\pi _ { N S } \colon N S \to S$ is defined as the restriction to NS of $\pi \colon T M \to M$ The following proposition is proved in the same way as Corol

Proposition 13.21

FC08-C13-U029 · Ch. 13, § The Normal Bundle; source L10069 · not formalized

Corollary 10.36. Proposition 13.21 (The Normal Bundle to a Riemannian Submanifold). Let $( M , g )$ be a Riemannian n-manifold with or without boundary. For any immersed k-dimensional submanifold $S \subseteq M$ with or without boundary, the normal bundle NS is a smooth rank-.n k/ subbundle of $T M \vert _ { S }$ . For each $p \in S$ , there is a smooth frame for NS on a neighborhood of p that is orthonormal with respect to $g$ .

Definition/convention — lengths of curves

FC08-C13-U030 · Ch. 13, § The Riemannian Distance Function; source L10075 · not formalized

One of the most important tools that a Riemannian metric gives us is the ability to define lengths of curves. Suppose $( M , g )$ is a Riemannian manifold with or without boundary. If $\gamma \colon [ a , b ] \to M$ is a piecewise smooth curve segment, the length of is \[ \mathrm{L} _ {g} (\gamma) = \int_ {a} ^ {b} \left| \gamma^ {\prime} (t) \right| _ {g} d t. \]

Proposition 13.25

FC08-C13-U031 · Ch. 13, § The Riemannian Distance Function; source L10095 · not formalized

Proposition 13.25 (Parameter Independence of Length). Let $( M , g )$ be a $R i e \mathrm { - }$ mannian manifold with or without boundary, and let $\gamma \colon [ a , b ] \to M$ be a piecewise smooth curve segment. $H \widetilde { \gamma }$ is a reparametrization of _ { : }$ , then $ _ { g }

Definition/convention — distances between points

FC08-C13-U032 · Ch. 13, § The Riemannian Distance Function; source L10109 · after FC08-C11-U046 · not formalized

Using curve segments as “measuring tapes,” we can define distances between points on a Riemannian manifold. Suppose $( M , g )$ is a connected Riemannian manifold. (The theory is most straightforward when $\partial M = \emptyset$ , so we assume that for the rest of this section.) For any $p , q \in M$ ; the (Riemannian) distance from p to $\pmb q$ , denoted by $d _ { g } ( p , q )$ , is defined to be the infimum of $\mathrm { L } _ { g } ( \gamma )$ over all piecewise smooth curve segments $\gamma$ from $p$ to $q$ . Because any pair of points in $M$ can be joined by a piecewise smooth curve segment (Proposition 11.33), this is well defined.

Example 13.26

FC08-C13-U033 · Ch. 13, § The Riemannian Distance Function; source L10111 · not formalized

Example 13.26. In $( \mathbb { R } ^ { n } , { \overline { { g } } } )$ , Problem 13-10 shows that any straight line segment is the shortest piecewise smooth curve segment between its endpoints. Therefore, the distance function $d _ { \bar { g } }$ is equal to the usual Euclidean distance: \[ d _ {\overline {{g}}} (x, y) = | x - y |. \]

Lemma 13.28

FC08-C13-U034 · Ch. 13, § The Riemannian Distance Function; source L10121 · not formalized

Let $g$ be a Riemannian metric on an open subset $U \subseteq \mathbb{R}^{n}$. For any compact $K \subseteq U$ there are positive constants $c, C$ such that for all $x \in K$ and all $v \in T_{x}\mathbb{R}^{n}$ \[ c\,|v|_{\overline{g}} \leq |v|_{g} \leq C\,|v|_{\overline{g}}. \tag{13.4} \]

Theorem 13.29

FC08-C13-U035 · Ch. 13, § The Riemannian Distance Function; source L10141 · not formalized

Theorem 13.29 (Riemannian Manifolds as Metric Spaces). Let $( M , g )$ be a connected Riemannian manifold. With the Riemannian distance function, M is a metric space whose metric topology is the same as the original manifold topology.

Definition/convention — complete

FC08-C13-U036 · Ch. 13, § The Riemannian Distance Function; source L10181 · not formalized

As a consequence of this theorem, all of the terminology of metric spaces can be carried over to connected Riemannian manifolds. Thus, a connected Riemannian manifold $( M , g )$ is said to be complete, and $g$ is said to be a complete Riemannian metric, if $( M , d _ { g } )$ is a complete metric space (i.e., if every Cauchy sequence in M converges to a point in $M )$ ; and a subset $B \subseteq M$ bounded there exists a constant K such that $d _ { g } ( x , y ) \leq K$ for all $x , y \in B$ . Problems 13-17 and 13-18 outline two different proofs that every connected smooth manifold admits a complete Riemannian metric.

Definition/convention — metrizable

FC08-C13-U037 · Ch. 13, § The Riemannian Distance Function; source L10183 · in Mathlib

Recall that a topological space is said to be metrizable if it admits a distance function whose metric topology is the same as the given topology.

Formalized. Mathlib/Topology/Metrizable/Basic.lean::TopologicalSpace.MetrizableSpace — MetrizableSpace X is Mathlib’s predicate that the given topology on X is induced by some metric-space structure, exactly Lee’s definition of a metrizable topological space.

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

Corollary 13.30

FC08-C13-U038 · Ch. 13, § The Riemannian Distance Function; source L10185 · in Mathlib

Corollary 13.30. Every smooth manifold with or without boundary is metrizable.

Formalized. Mathlib/Geometry/Manifold/Metrizable.lean::Manifold.metrizableSpace — Manifold.metrizableSpace proves that a finite-dimensional real σ-compact Hausdorff topological manifold is metrizable. These are the standing manifold hypotheses in Mathlib’s manifold setup used for FC08, so this is Lee’s Corollary 13.30.

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

Definition/convention — bundle homomorphism hat(g)

FC08-C13-U039 · Ch. 13, § The Tangent–Cotangent Isomorphism; source L10197 · not formalized

Another convenient feature of every Riemannian metric is that it provides a natural isomorphism between the tangent and cotangent bundles. Given a Riemannian metric $g$ on a smooth manifold M with or without boundary, we define a bundle homomorphism ${ \widehat { g } } \colon T M \to T ^ { * } M$ as follows. For each $p \in M$ and each $v \in T _ { p } M$ we let $\widehat g ( v ) \in T _ { p } ^ { * } M$ be the covector defined by \[ \widehat {g} (v) (w) = g _ {p} (v, w) \quad \text { for all } w \in T _ {p} M. \]

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has finite-dimensional inner-product duality and standard-tangent Riemannian structures, but Lee’s musical maps and gradient are bundle constructions on the source-defined point-derivation tangent/cotangent bundles. C03/C11 provide no checked tangent equivalence or cotangent-bundle bridge, so these rows remain unmatched. Strict whole-row semantics reject proper subsets, unproved converse directions, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.

Definition/convention — source terminology/construction

FC08-C13-U040 · Ch. 13, § The Tangent–Cotangent Isomorphism; source L10233 · not formalized

The components of the covector field $\widehat{g}(X)$ are written \[ \widehat{g}(X) = X_{j}\,dx^{j}, \qquad \text{where } X_{j} = g_{ij}X^{i}. \]

Convention/notation — tone

FC08-C13-U041 · Ch. 13, § The Tangent–Cotangent Isomorphism; source L10239 · not formalized

One says that $\widehat{g}(X)$ is obtained from $X$ by lowering an index, and writes $X^{\flat}$ for $\widehat{g}(X)$, after the musical symbol for lowering a tone.

Definition/convention — source terminology/construction

FC08-C13-U042 · Ch. 13, § The Tangent–Cotangent Isomorphism; source L10241 · not formalized

The matrix of the inverse map $\widehat{g}^{-1} \colon T_{p}^{*}M \to T_{p}M$ is the inverse of $(g_{ij})$, which is invertible at each point because $(g_{ij})$ is the matrix of the isomorphism $\widehat{g}$. Writing $(g^{ij})$ for the matrix-valued function whose value at $p$ is the inverse of $(g_{ij}(p))$, \[ g^{ij}g_{jk} = g_{kj}g^{ji} = \delta^{i}_{k}, \] and $(g^{ij})$ is symmetric, so a covector field $\omega$ has $\widehat{g}^{-1}(\omega) = \omega^{i}\,\partial/\partial x^{i}$ with $\omega^{i} = g^{ij}\omega_{j}$.

Convention/notation — musical isomorphisms

FC08-C13-U043 · Ch. 13, § The Tangent–Cotangent Isomorphism; source L10253 · not formalized

\[ We use the notation $\omega ^ { \sharp } ( ^ { \ast } \omega \cdot \ s h a r p ^ { \ast } )$ for $\widehat g ^ { - 1 } ( \omega )$ , and say that $\omega ^ { \sharp }$ is obtained from ! by raising an index. Because the symbols [ and ] are borrowed from musical notation, these two inverse isomorphisms are frequently called the musical isomorphisms. A handy mnemonic device for keeping the flat and sharp operations straight is to remember that the value of $\omega ^ { \sharp }$ at each point is a vector, which we visualize as a (sharp) arrow; while the value of $X ^ { \flat }$ is a covector, which we visualize by means of its (flat) level sets. The most important use of the sharp operation is to reinstate the gradient as a vector field on Riemannian manifolds. For any smooth real-valued function $f$ on a Riemannian manifold $( M , g )$ with or without boundary, we define a vector field called the gradient of f by \]

Definition/convention — gradient of f by grad f

FC08-C13-U044 · Ch. 13, § The Tangent–Cotangent Isomorphism; source L10255 · not formalized

The most important use of the sharp operation is to reinstate the gradient as a vector field on Riemannian manifolds. For any smooth real-valued function $f$ on a Riemannian manifold $( M , g )$ with or without boundary, we define a vector field called the gradient of f by \[ \operatorname{grad} f = (d f) ^ {\sharp} = \widehat {g} ^ {- 1} (d f). \]

Example 13.31

FC08-C13-U045 · Ch. 13, § The Tangent–Cotangent Isomorphism; source L10293 · after FC08-C13-U018 · not formalized

Example 13.31. Let us compute the gradient of a function $f \in C ^ { \infty } \left( \mathbb { R } ^ { 2 } \right)$ with respect to the Euclidean metric in polar coordinates. From Example 13.12 we see that the matrix of $\overline { { g } }$ in polar coordinates is $\binom { 1 } { 0 } \binom { 0 } { r ^ { 2 } }$ , so its inverse matrix is $\binom { 1 } { 0 } _ { 1 / r ^ { 2 } }$ Inserting this into the formula for the gradient, we obtain \[ \mathrm{grad} f = \frac {\partial f}{\partial r} \frac {\partial}{\partial r} + \frac {1}{r ^ {2}} \frac {\partial f}{\partial \theta} \frac {\partial}{\partial \theta}.\tag{//} \] Problem 13-21 shows that the gradient of a function $f$ on a Riemannian manifold has the same geometric interpretation as it has in Euclidean space: its direction is the direction in which $f$ is increasing fastest, and is orthogonal to the level sets of $f$ ; and its length is the maximum directional derivative }) ^ {2}.

Definition/convention — signature of g

FC08-C13-U046 · Ch. 13, § Pseudo-Riemannian Metrics; source L10303 · in Mathlib

An important generalization of Riemannian metrics is obtained by relaxing the positivity requirement. A symmetric 2-tensor $g$ on a vector space V is said to be nondegenerate if the linear map $\widehat { g } \colon V \to V ^ { * }$ defined by $\widehat g ( v ) ( w ) = g ( v , w )$ is an isomorphism, or equivalently if for every nonzero $v \in V$ there exists $w \in V$ such that $g ( v , w ) \neq 0$ . Just as any inner product can be transformed to the Euclidean one by switching to an orthonormal basis, every nondegenerate symmetric 2-tensor can be transformed by a change of basis to one whose matrix is diagonal with all entries equal to $\pm 1$ (the proof is an adaptation of the Gram–Schmidt algorithm). The numbers r and s of positive and negative diagonal entries, respectively, are independent of the choice of basis $\mathrm { ( a }$ fact known as Sylvester’s law of inertia; see [FIS03] for a proof). Thus the ordered pair $( r , s )$ , called the signature of $\pmb { g }$ , is an invariant of $g$.

Formalized. Mathlib/LinearAlgebra/BilinearForm/Properties.lean::LinearMap.BilinForm.Nondegenerate, LinearMap.BilinForm.toDual; Mathlib/LinearAlgebra/QuadraticForm/Basic.lean::QuadraticMap.associated_left_inverse; Mathlib/LinearAlgebra/QuadraticForm/Real.lean::QuadraticForm.equivalent_one_neg_one_weighted_sum_squared; Mathlib/LinearAlgebra/QuadraticForm/Signature.lean::QuadraticForm.sigPos, QuadraticForm.sigNeg, QuadraticForm.sigPos_of_equiv_weightedSumSquares, QuadraticForm.sigNeg_of_equiv_weightedSumSquares — For a finite-dimensional real symmetric bilinear form, Nondegenerate is the separating condition and toDual is the induced linear equivalence V ≃ₗ V*. Symmetry identifies the associated quadratic form with the original bilinear form; Sylvester’s theorem diagonalizes every nondegenerate real form with weights ±1, and sigPos/sigNeg are invariant under equivalence and count the positive/negative weights. /tmp/fc08-c13-witness.lean compiles this bridge at P.

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

Definition/convention — Lorentz metrics

FC08-C13-U047 · Ch. 13, § Pseudo-Riemannian Metrics; source L10305 · not formalized

A pseudo-Riemannian metric on a smooth manifold M is a smooth symmetric 2-tensor field whose value is nondegenerate at each point, with the same signature everywhere on M . Pseudo-Riemannian metrics with signature $( n - 1 , 1 )$ (or $( 1 , n - 1 )$ , depending on the convention used) are called Lorentz metrics; they play a central role in physics, where they are used to model gravitation in Einstein’s general theory of relativity.

Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no manifold-level pseudo-Riemannian/Lorentz metric structure with constant signature; exact searches for PseudoRiemannian/LorentzMetric are empty. The algebraic signature theory from U046 is insufficient to supply the smooth tensor-field bundle required here. Strict whole-row semantics reject proper subsets, unproved converse directions, unbridged tangent models, and reconstruction of substantive source theorems from generic ingredients.