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

FC08 — Lee, Introduction to Smooth Manifolds.

This chapter contains 20 definitions, 4 theorems, 18 propositions, 2 lemmas, 1 corollary, 8 examples, 2 constructions and 1 convention.

Of the 56 statements checked against Lean, 5 are formalized somewhere and 51 are not.

Status	Statements	Share	What it means
not formalized	51	91%	A documented search found no Lean statement of it anywhere.
in Mathlib	5	9%	Mathlib states and proves it.
checked in total	56

Which versions of Lean and Mathlib were searched

Canonical source block: FC08 Lee, Chapter 15, FC08-C15-U001–FC08-C15-U056, exactly 56 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.
C15 has 5 pinned mathlib rows and 51 dated unmatched rows. Positive rows are: U003, U004, U006, U007, U048.
Linear orientation algebra is mature at P. Orientation is a positive ray of top alternating forms; Basis.orientation, orientation_eq_iff_det_pos, and the negation lemmas make it equivalent to Lee’s ordered-basis equivalence classes. The zero-dimensional case is represented by positiveOrientation and Orientation.eq_or_eq_neg_of_isEmpty.
/tmp/fc08-c15-witness.lean compiled at exact P. Its central bridge proves rayOfNeZero ℝ ω hω = e.orientation ↔︎ 0 < ω e, so Mathlib’s ray representation exactly realizes Lee Proposition 15.3; it also verifies that the determinant form of a basis lies in that basis orientation.
U002 is deliberately unmatched because the canonical catalogue row is truncated after the transition-matrix formula and omits the determinant-sign condition. The adjacent Mathlib theorem is not used to repair source text silently.
P and current H have no global smooth-manifold orientation/orientability API. Exact searches find no Orientable/IsOrientable manifold structure, orientation-preserving smooth-map predicate, orientation covering, or smooth manifold volume-form layer. Therefore U008–U047 and U050–U056 remain unmatched even when linear orientation, standard-tangent Riemannian, or generic covering ingredients are present.
Tangent-based manifold rows also inherit the C03 boundary: Lee’s FC08 tangent spaces are point derivations, while Mathlib manifold tangent geometry uses standard TangentSpace; no checked bridge exists at P/H. Hypersurface/submanifold rows additionally inherit C05’s absent general submanifold API.
U048 is independent of manifold orientation. Mathlib’s IsCoveringMap already permits disconnected total spaces and supplies the evenly-covered/continuity part, while Lee additionally requires local path connectedness and surjectivity. The exact conjunction was compiled in the witness. U049 is not inferred: no checked theorem provides Lee’s componentwise restriction result, and proving it would be substantive.
Targeted current GitHub/indexed searches did not surface a compatible external Lean owner for manifold orientability or the orientation-covering theorems.
N=2026-09-07 marks dated unmatched decisions. Strict whole-row semantics apply uniformly.

Definition/convention — orientable

FC08-C15-U001 · Ch. 15; source L11474 · not formalized

As we will see in this chapter, a vector space always has exactly two choices of orientation. In R, there is a standard orientation that we can all agree on; but in other vector spaces, an arbitrary choice has to be made. For manifolds, the situation is much more complicated. On a sphere, it is possible to decide unambiguously which rotational direction is counterclockwise, by looking at the surface from the outside (Fig. 15.1). On the other hand, a Möbius band (Fig. 15.2) has the curious property that a figure moving around on the surface can come back to its starting point transformed into its mirror image, so it is impossible to decide consistently which of the two possible rotational directions on the surface to call “clockwise” and which “counterclockwise,” or which is the “front” side and which is the “back” side. The analogous phenomenon in a 3-manifold would be a right-handed person who takes a long trip and comes back left-handed. Manifolds like the sphere, in which it is possible to choose a consistent orientation, are said to be orientable; those like the Möbius band in which it is not possible are said to be nonorientable.

Not formalized. none; no complete checked declaration under strict bundle semantics — This introductory row mixes the manifold notion of orientability with sphere/Möbius examples. P/H has linear orientations but no manifold-orientation/orientability API owning the full row. Strict whole-row semantics reject proper subsets, missing converse directions, unbridged tangent models, and substantive reconstruction from generic ingredients.

Definition/convention — source terminology/construction

FC08-C15-U002 · Ch. 15, § Orientations of Vector Spaces; source L11492 · not formalized

Let $V$ be a real vector space of dimension $n \geq 1$. Two ordered bases $(E_{1},\dots,E_{n})$ and $(\widetilde{E}_{1},\dots,\widetilde{E}_{n})$ for $V$ are consistently oriented if the transition matrix $(B^{j}_{i})$, defined by \[ E_{i} = B^{j}_{i}\widetilde{E}_{j}, \tag{15.1} \] has positive determinant.

Not formalized. none; no complete checked declaration under strict bundle semantics — The canonical source row is truncated immediately after defining the transition matrix and omits the determinant-sign clause completing Lee’s definition. Module.Basis.orientation_eq_iff_det_pos is the expected adjacent theorem, but the missing source text is not reconstructed. Strict whole-row semantics reject proper subsets, missing converse directions, unbridged tangent models, and substantive reconstruction from generic ingredients.

Convention/notation — oriented vector space

FC08-C15-U003 · Ch. 15, § Orientations of Vector Spaces; source L11502 · in Mathlib

dim $V = n \geq 1$ , we define an orientation for $V$ as an equivalence class of ordered bases. If $( E _ { 1 } , \ldots , E _ { n } )$ is any ordered basis for V , we denote the orientation that it determines by $[ E _ { 1 } , \ldots , E _ { n } ]$ , and the opposite orientation by $- [ E _ { 1 } , \dots , E _ { n } ]$ A vector space together with a choice of orientation is called an oriented vector space. If V is oriented, then any ordered basis $( E _ { 1 } , \ldots , E _ { n } )$ that is in the given orientation is said to be oriented or positively oriented. Any basis that is not in the given orientation is said to be negatively oriented.

Formalized. Mathlib/LinearAlgebra/Orientation.lean::Orientation, Module.Oriented, Module.Basis.orientation, Module.Basis.orientation_eq_iff_det_pos, Module.Basis.orientation_ne_iff_eq_neg — Orientation ℝ V (Fin n) is Mathlib’s equivalent representation of an orientation: Basis.orientation sends an ordered basis to its class; orientation_eq_iff_det_pos proves that two bases give the same class exactly when the change-of-basis determinant is positive; negation is the opposite orientation, and Module.Oriented records a chosen positive orientation.

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

Definition/convention — orientation of V to be simply a choice of one of the numbers

FC08-C15-U004 · Ch. 15, § Orientations of Vector Spaces; source L11504 · in Mathlib

For the special case of a zero-dimensional vector space V , we define an orientation of V to be simply a choice of one of the numbers is smooth.

Formalized. Mathlib/LinearAlgebra/Orientation.lean::IsEmpty.oriented, Orientation.eq_or_eq_neg_of_isEmpty — For an empty index type (the zero-dimensional case), Mathlib supplies a canonical positiveOrientation and proves every orientation is either it or its negation. This is exactly Lee’s choice of +1 or -1.

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

Example 15.2

FC08-C15-U005 · Ch. 15, § Orientations of Vector Spaces; source L11506 · not formalized

The orientation $[e_{1},\dots,e_{n}]$ of $\mathbb{R}^{n}$ determined by the standard basis is the standard orientation. In the usual graphical conventions, an oriented basis for $\mathbb{R}$ points to the right, an oriented basis for $\mathbb{R}^{2}$ is one whose rotation from the first vector to the second is counterclockwise, and an oriented basis for $\mathbb{R}^{3}$ is right-handed; these may be taken as the definitions of those words. The standard orientation of $\mathbb{R}^{0}$ is defined to be $+1$.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib can define the basis orientation of ℝ^n, but this example also packages the geometric right/counterclockwise/right-handed interpretations and the ℝ^0 convention. No checked declaration owns the whole example. Strict whole-row semantics reject proper subsets, missing converse directions, unbridged tangent models, and substantive reconstruction from generic ingredients.

Proposition 15.3

FC08-C15-U006 · Ch. 15, § Orientations of Vector Spaces; source L11510 · in Mathlib

Proposition 15.3. Let V be a vector space of dimension n. Each nonzero element $\omega \in \Lambda ^ { n } ( V ^ { * } )$ determines an orientation $\mathcal { O } _ { \omega }$ of V as follows: $i f n \geq 1$ , then $\mathcal { O } _ { \omega }$ is the set of ordered bases $( E _ { 1 } , \ldots , E _ { n } )$ such that ! $( E _ { 1 } , \ldots , E _ { n } ) > 0$ ; while if ${ \dot { n } } = 0$ , then $\mathcal { O } _ { \omega } \ i s + 1 \ i f \omega > 0 .$ , and 1 if ! < 0. Two nonzero n-covectors determine the same orientation if and only if each is a positive multiple of the other.

Formalized. Mathlib/LinearAlgebra/Orientation.lean::Orientation, Module.Basis.orientation; Mathlib/LinearAlgebra/Ray.lean::rayOfNeZero, ray_eq_iff, SameRay.sameRay_smul_left_iff_of_ne; Mathlib/LinearAlgebra/Determinant.lean::AlternatingMap.eq_smul_basis_det — Mathlib defines an orientation as a positive ray of nonzero top alternating forms. At exact P, /tmp/fc08-c15-witness.lean proves rayOfNeZero ℝ ω hω = e.orientation ↔︎ 0 < ω e, and ray equality is precisely positive scalar proportionality. This is Lee’s Proposition 15.3 including the orientation selected by a nonzero top covector.

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

Definition/convention — source terminology/construction

FC08-C15-U007 · Ch. 15, § Orientations of Vector Spaces; source L11522 · in Mathlib

If $V$ is an oriented $n$-dimensional vector space and $\omega$ is an $n$-covector determining the orientation of $V$, then $\omega$ is called a positively oriented $n$-covector. For example, $e^{1} \wedge \cdots \wedge e^{n}$ is positively oriented for the standard orientation on $\mathbb{R}^{n}$.

Formalized. Mathlib/LinearAlgebra/Orientation.lean::Module.Basis.orientation; Mathlib/LinearAlgebra/Ray.lean::rayOfNeZero — A top covector is positively oriented exactly when its positive ray is the chosen Orientation. The compiled witness also checks rayOfNeZero ℝ e.det e.det_ne_zero = e.orientation, giving the basis determinant form as the canonical positively oriented top form.

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

Definition/convention — pointwise orientation

FC08-C15-U008 · Ch. 15, § Orientations of Manifolds; source L11531 · not formalized

Let M be a smooth manifold with or without boundary. We define a pointwise orientation on M to be a choice of orientation of each tangent space. By itself, this is not a very useful concept, because the orientations of nearby points may have no relation to each other. For example, a pointwise orientation on $\mathbb { R } ^ { n }$ might switch randomly from point to point between the standard orientation and its opposite. In order for orientations to have some relationship with the smooth structure, we need an extra condition to ensure that the orientations of nearby tangent spaces are consistent with each ot smooth chart for the standard smooth structure on $\mathbb { B } ^ { n }$ .

Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no global smooth-manifold orientation or orientability structure. Its linear Orientation API does not provide Lee’s continuous pointwise orientations, oriented frames/charts, orientation forms, orientation-preserving local diffeomorphisms, product/pullback manifold orientations, or Lie-group orientation theorem. In addition, tangent-based clauses inherit the C03 point-derivation-vs-standard-TangentSpace boundary. Strict whole-row semantics reject proper subsets, missing converse directions, unbridged tangent models, and substantive reconstruction from generic ingredients.

Definition/convention — negatively oriented frame

FC08-C15-U009 · Ch. 15, § Orientations of Manifolds; source L11533 · not formalized

Let M be a smooth n-manifold with or without boundary, endowed with a pointwise orientation. If $\left( E _ { i } \right)$ is a local frame for TM; we say that $\left( E _ { i } \right)$ is (positively) oriented if $( E _ { 1 } | _ { p } , \ldots , E _ { n } | _ { p } )$ is a positively oriented basis for $T _ { p } M$ at each point $p \in U$ . A negatively oriented frame is defi ition with F equal to the identity map of $U \cap { \widetilde { U } }$ , but using coordinates $\left( x ^ { i } \right)$ in the domain and $\left( \widetilde { x } ^ { j } \right)$ in the codomain.

Definition/convention — continuous

FC08-C15-U010 · Ch. 15, § Orientations of Manifolds; source L11535 · not formalized

A pointwise orientation is said to be continuous if every point of M is in the domain of an oriented local frame. (Recall that by definition the vector fields that make up a local frame are continuous.) An orientation of M is a continuous pointwise orientation. We say that M is orientable if there exists an orientation for it, and nonorientable if not. An oriented manifold is an ordered pair $( M , { \mathcal { O } } )$ , where M is an smooth manifold and is a choice of orientation for M ; an oriented manifold with boundary is defined similarly. For each $p \in M$ ; the orientation }$ M determined by is denoted by $\mathcal { O } _ { p }$ . When it is not important to name the orientation explicitly, we use the usual shorthand expression “M is an oriented smooth manifold” (or “manifold with boundary”). If M is zero-dimensional, this definition just means that an orientation of M is a choice of $

Definition/convention — orientation of M

FC08-C15-U011 · Ch. 15, § Orientations of Manifolds; source L11537 · not formalized

If M is zero-dimensional, this definition just means that an orientation of M is a choice of $\pm 1$ attached to each of its points. The continuity condition is vacuous in this case, and the notion of oriented frames is not useful. Clearly, every 0-manifold is orientable.

Proposition 15.5

FC08-C15-U012 · Ch. 15, § Orientations of Manifolds; source L11543 · not formalized

Proposition 15.5 (The Orientation Determined by an n-Form). Let M be a smooth n-manifold with or without boundary. Any nonvanishing n-form ! on M determines a unique orientation of M for which ! is positively oriented at each point. Conversely, if M is given an orientation, then there is a smooth nonvanishing n-form on M that is positively oriented at each point.

Definition/convention — orientation form

FC08-C15-U013 · Ch. 15, § Orientations of Manifolds; source L11545 · not formalized

Remark. Because of this proposition, if M is a smooth n-manifold with or without boundary, any nonvanishing n-form on M is called an orientation form. If M is oriented and ω is an orientation form determining the given orientation, we also say that ω is (positively) oriented. It is easy to check that if ω and tilde(ω) are two positively oriented smooth forms on M , ; then tilde(ω) = f ω for some strictly positive smooth realvalued function f . If M is a 0-manifold, a nonvanishing 0-form (i.e., real-valued function) assigns the orientation 1 to points where it is positive and 1 to points where it is negative.

Definition/convention — consistently oriented

FC08-C15-U014 · Ch. 15, § Orientations of Manifolds; source L11557 · not formalized

A smooth chart on an oriented smooth manifold with or without boundary is positively oriented if its coordinate frame $(\partial/\partial x^{i})$ is positively oriented, and negatively oriented if that frame is negatively oriented. A smooth atlas $\{(U_{\alpha},\varphi_{\alpha})\}$ is consistently oriented if for each $\alpha, \beta$ the transition map $\varphi_{\beta} \circ \varphi_{\alpha}^{-1}$ has positive Jacobian determinant everywhere on $\varphi_{\alpha}(U_{\alpha} \cap U_{\beta})$.

Proposition 15.6

FC08-C15-U015 · Ch. 15, § Orientations of Manifolds; source L11559 · not formalized

Proposition 15.6 (The Orientation Determined by a Coordinate Atlas). Let M be a smooth positive-dimensional manifold with or without boundary. Given any consistently oriented smooth atlas for M; there is a unique orientation for M with the property that each chart in the given atlas is positively oriented. Conversely, if M is oriented and either $\partial M = \emptyset$ or dim $M > 1$ , then the collection of all oriented smooth charts is a consistently oriented atlas for M .

Proposition 15.7

FC08-C15-U016 · Ch. 15, § Orientations of Manifolds; source L11565 · not formalized

Proposition 15.7 (Product Orientations). Suppose $M _ { 1 } , \dots , M _ { k }$ are orientable smooth manifolds. There is a unique orientation on $M _ { 1 } \times \cdots \times M _ { k }$ , called the product orientation, with the following property: if for each $i = 1 , \ldots , k , \omega _ { i }$ is an orientation form for the given orientation on $M _ { i }$ , then $\pi _ { 1 } ^ { * } \omega _ { 1 } \wedge \cdots \wedge \pi _ { k } ^ { * } \omega _ { k }$ is an orientation form for the product orientation.

Proposition 15.9

FC08-C15-U017 · Ch. 15, § Orientations of Manifolds; source L11569 · not formalized

Proposition 15.9. Let M be a connected, orientable, smooth manifold with or without boundary. Then M has exactly two orientations. If two orientations of M agree at one point, they are equal.

Proposition 15.11

FC08-C15-U018 · Ch. 15, § Orientations of Manifolds; source L11573 · not formalized

Proposition 15.11 (Orientations of Codimension-0 Submanifolds). Suppose M is an oriented smooth manifold with or without boundary, and $D \subseteq M$ is a smooth codimension-0 submanifold with or without boundary. Then the orientation of M restricts to an orientation of D. If ! is an orientation form for M; then $\iota _ { D } ^ { * } \omega$ is an orientation form for D.

Definition/convention — source terminology/construction

FC08-C15-U019 · Ch. 15, § Orientations of Manifolds; source L11577 · not formalized

Let M and N be oriented smooth manifolds with or without boundary, and suppose $F \colon M \to N$ is a local diffeomorphism. If M and N are positive-dimensional, we say that F is orientation-preserving if for each $p \in M ,$ ; the isomorphism d $F _ { p }$ takes oriented bases of $T _ { p } M$ to oriented bases of $T _ { F ( p ) } N$ , and orientationreversing if it takes oriented bases of $T _ { p } M$ to negatively oriented bases of $T _ { F ( p ) } N$ If M and N are 0-manifolds, then F is orientation-preserving if for every $p \in M$ the points p and $F ( p )$ have the same orientation; and it is orientation-reversing if they have the opposite orientation.

Proposition 15.15

FC08-C15-U020 · Ch. 15, § Orientations of Manifolds; source L11591 · not formalized

Proposition 15.15 (The Pullback Orientation). Suppose M and N are smooth manifolds with or without boundary. If $F \colon M \to N$ is a local diffeomorphism and N is oriented, then M has a unique orientation, called the pullback orientation induced by F , such that F is orientation-preservi rties: (i) d is linear over R.

Construction/definition — source terminology/construction

FC08-C15-U021 · Ch. 15, § Orientations of Manifolds; source L11595 · not formalized

In the situation of the preceding proposition, if denotes the given orientation on N , the pullback orientation on M is denoted b

Proposition 15.17

FC08-C15-U022 · Ch. 15, § Orientations of Manifolds; source L11601 · not formalized

Proposition 15.17. Every parallelizable smooth manifold is orientable. P

Example 15.18

FC08-C15-U023 · Ch. 15, § Orientations of Manifolds; source L11608 · not formalized

vector field along a submanifold Example 15.18. The preceding proposition implies that Euclidean space $\mathbb { R } ^ { n }$ , the n-torus $\mathbb { T } ^ { n }$ , the spheres $\mathrm { S } ^ { 1 } , \mathrm { S } ^ { \bar { 3 } }$ , and $\mathbb { S } ^ { 7 }$ , and products of them are all orientable, because they are all parallelizable. Therefore, any codimension-0 submanifold of one of these manifolds is also orientable. Likewise, every Lie group is orientable beca ome neighborhood of $p$ and supported in $U$ .

Definition/convention — left-invariant orientation

FC08-C15-U024 · Ch. 15, § Orientations of Manifolds; source L11610 · not formalized

In the case of Lie groups, we can say more. If G is a Lie group, an orientation of G is said to be left-invariant if $L _ { g }$ is orientation-preserving ating this at $p$ and using the facts that $\psi ( p ) = 1$ and ${ \boldsymbol { l } } \psi _ { p } = 0$ , we conclude that d!

Proposition 15.19

FC08-C15-U025 · Ch. 15, § Orientations of Manifolds; source L11612 · not formalized

every $g \in G$ Proposition 15.19. Every Lie group has precisely two left-invariant orientations, corresponding to the two orientations of its Lie algebra.

Definition/convention — oriented smooth manifold

FC08-C15-U026 · Ch. 15, § Orientations of Hypersurfaces; source L11618 · not formalized

If M is an oriented smooth manifold and S is a smooth submanifold of M (with or without boundary), S might not inherit an orientation from M; even if S is embedded. Clearly, it is not sufficient to restrict an orientation form from M to S , since the restriction of an n-form to a manifold of lower dimension must necessarily be zero. A useful example to consider is the Möbius band, which is not orientable (see Example 15.38 below), even though it can be embedded together with the observation in the preceding paragraph, it follows that (14.19) holds at $p$ .

Not formalized. none; no complete checked declaration under strict bundle semantics — This row requires manifold orientations together with hypersurface/boundary or Riemannian tangent geometry. P/H has no manifold-orientation layer; hypersurface/submanifold claims also inherit C05’s missing general submanifold object and C03’s unbridged tangent model. Fiberwise orientation/volume-form ingredients are only proper subsets. Strict whole-row semantics reject proper subsets, missing converse directions, unbridged tangent models, and substantive reconstruction from generic ingredients.

Proposition 15.21

FC08-C15-U027 · Ch. 15, § Orientations of Hypersurfaces; source L11624 · not formalized

Proposition 15.21. Suppose M is an oriented smooth n-manifold with or without boundary, S is an immersed hypersurface with or without boundary in M; and N is a vector field along S that is nowhere tangent to S. Then S has a unique orientation such that for each $p \in S , ( E _ { 1 } , \ldots , E _ { n - 1 } )$ is an oriented basis for $T _ { p } S$ if and only if $( N _ { p } , E _ { 1 } , \dots , E _ { n - 1 } )$ is an oriented basis for $T _ { p } M$ . If ! is an orientation form for M; then $\iota _ { S } ^ { * } ( N \lrcorner \omega )$ is an orientation form for S with respect to this orientation, where $\iota _ { S } \colon S \hookrightarrow M$ is inclusi esentation $\psi \stackrel { - } { \circ } F \circ \varphi ^ { - 1 }$ .

Example 15.22

FC08-C15-U028 · Ch. 15, § Orientations of Hypersurfaces; source L11639 · not formalized

Example 15.22. The sphere $\mathbb { S } ^ { n }$ is a hypersurface in $\mathbb { R } ^ { n + 1 }$ , to which the vector field $N = x ^ { i } \partial / \partial x ^ { i }$ is nowhere tangent, so this vector field induces an orientation on $\mathbb { S } ^ { n }$ This shows that all spheres are orientable. We define the standard orientation of $\mathbb { S } ^ { n }$ to be the orientation determined by N . Unless otherwise specified, we always use this orientation. (The standard orientation on $\mathbb { S } ^ { 0 }$ is the one that assigns the orientation 1 to the point $+ 1 \in \mathbb { S } ^ { 0 }$ and $- 1 \mathrm { ~ t o ~ } { - 1 } \in \mathbb { S } ^ { 0 } . )$ Not every hypersurface admits a nowhere tangent vector field. (See Problem 15-6.) However, the following proposition gives a sufficient condition that holds in many cases. Proposition 15.23. Let

Proposition 15.23

FC08-C15-U029 · Ch. 15, § Orientations of Hypersurfaces; source L11645 · not formalized

Let M be an oriented smooth manifold, and suppose S ⊆ M is a regular level set of a smooth function f M → ℝ . Then S is orientable . The proof takes a Riemannian metric on $M$ and the vector field $N = \operatorname{grad} f|_{S}$, which is nowhere tangent to $S$, so Proposition 15.21 applies.

Definition/convention — outward-pointing vector field

FC08-C15-U030 · Ch. 15, § Boundary Orientations; source L11651 · after FC08-C05-U016 · not formalized

If M is a smooth manifold with boundary, then @M is an embedded hypersurface in M (see Theorem 5.11), and Problem 8-4 showed that there is always a smooth outward-pointing vector field along @M . Because an outward-pointing vector field is nowhere tangent to @M; it determines an orientation on @M

Proposition 15.24

FC08-C15-U031 · Ch. 15, § Boundary Orientations; source L11653 · not formalized

Proposition 15.24 (The Induced Orientation on a Boundary). Let M be an oriented smooth n-manifold with boundary, $n \geq 1$ . Then @M is orientable, and all outward-pointing vector fields along @M determine the same orientation on @M .

Definition/convention — induced orientation

FC08-C15-U032 · Ch. 15, § Boundary Orientations; source L11655 · not formalized

Remark. The orientation on @M determined by any outward-pointing vector field is called the induced orientation or the Stokes orientation on @M . (The second term is chosen because of the role this orientation plays in Stokes’s theorem, to be discussed in Chapter 16.)

Example 15.25

FC08-C15-U033 · Ch. 15, § Boundary Orientations; source L11661 · not formalized

they are both negative multiples of $\partial / \partial x ^ { 1 } | _ { p \cdot } )$ ) Example 15.25. This proposition gives a simpler proof that $\mathbb { S } ^ { n }$ is orientable, because it is the boundary of the closed unit ball. The orientation thus induced on $\mathbb { S } ^ { n }$ is the standard one, as you can check.

Example 15.26

FC08-C15-U034 · Ch. 15, § Boundary Orientations; source L11663 · not formalized

Give $\mathbb{H}^{n}$ the standard orientation inherited from $\mathbb{R}^{n}$ and identify $\partial\mathbb{H}^{n}$ with $\mathbb{R}^{n-1}$ by $(x^{1},\dots,x^{n-1},0) \leftrightarrow (x^{1},\dots,x^{n-1})$. The induced orientation satisfies \[ \left[-\partial/\partial x^{n},\ \partial/\partial x^{1},\dots,\partial/\partial x^{n-1}\right] = -\left[\partial/\partial x^{n},\ \partial/\partial x^{1},\dots,\partial/\partial x^{n-1}\right] = (-1)^{n}\left[\partial/\partial x^{1},\dots,\partial/\partial x^{n-1},\ \partial/\partial x^{n}\right]. \] So the induced orientation on $\partial\mathbb{H}^{n}$ agrees with the standard orientation of $\mathbb{R}^{n-1}$ when $n$ is even and is opposite to it when $n$ is odd; the standard coordinates on $\partial\mathbb{H}^{n} \approx \mathbb{R}^{n-1}$ are positively oriented if and only if $n$ is even.

Lemma 15.27

FC08-C15-U035 · Ch. 15, § Boundary Orientations; source L11676 · not formalized

Lemma 15.27. Let M be an oriented smooth n-manifold with boundary. Suppose $U \subseteq \mathbb { R } ^ { n - 1 }$ is open, a; b are real numbers with $a < b$ , and F $( a , b ] \times U \to M$ is a smooth embedding that restricts to an embedding of $\{ b \} \times U$ into @M . Then the parametrization $f \colon U \to \partial M$ given by $f ( x ) = F ( b , x )$ is orientation-preserving for @M if and only if F is orientation-preservin rray}{c} d (u d v) (X, Y) = d u d v (X, Y) = d u (X) d v (Y) - d v (X) d u (Y) \ = X u Y v - X v Y u.

Example 15.28

FC08-C15-U036 · Ch. 15, § Boundary Orientations; source L11705 · after FC08-C15-U035 · not formalized

Example 15.28. Spherical coordinates (Example C.38) yield a smooth local parametrization of $\mathbb { S } ^ { 2 }$ as follows. Let U be the open rectangle $( 0 , \pi ) \times ( 0 , 2 \pi ) \subseteq \mathbb { R } ^ { 2 }$ U ^ { 3 }$ be the following map: \[ X (\varphi , \theta) = (\sin \varphi \cos \theta , \sin \varphi \sin \theta , \cos \varphi) \] (Fig. 15.7).We can check whether X preserves or reverses orientation by using the fact that it is the restriction of the 3-dimensional spherical coordinate parametrization $ 1 ] U ^ { 3 }$ defined by \[ F (\rho , \varphi , \theta) = (\rho \sin \varphi \cos \theta , \rho \sin \varphi \sin \theta , \rho \cos \varphi). \] Because $F ( 1 , \varphi , \theta ) = X ( \varphi , \theta )$ , the hypotheses of Lemma 15.27 are satisfied. By direct computation, the Jacobian determinant of $F$ is $\rho ^ { 2 }$ sin $\varphi }$ , which is positive on $( 0 , 1 ] \times U$ . By virtue of Lemma 15.27, X is orientation-preserving. ## The Riemannian Volume Form Let $

Proposition 15.29

FC08-C15-U037 · Ch. 15, § The Riemannian Volume Form; source L11723 · not formalized

Proposition 15.29. Suppose $( M , g )$ is an oriented Riemannian n-manifold with or without boundary, and $n \geq 1$ . There is a unique smooth orientation form $\omega _ { g } \in$ $\Omega ^ { n } ( M )$ , called the Riemannian volume form, that satisfies \[ \omega_ {g} (E _ {1}, \ldots , E _ {n}) = 1\tag{15.2} \] for every local oriented orthonormal frame $( E _ { i } )$ for M .

Proposition 15.31

FC08-C15-U038 · Ch. 15, § The Riemannian Volume Form; source L11763 · not formalized

Proposition 15.31. Let $( M , g )$ be an oriented Riemannian n-manifold with or without boundary, $n \geq 1$ . In any oriented smooth coordinates $\left( x ^ { i } \right)$ , the Riemannian volume form has the local coordinate expression \[ \omega_ {g} = \sqrt {\det (g _ {i j})} d x ^ {1} \wedge \dots \wedge d x ^ {n}, \] where $g _ { i j }$ are the components of $_ g$ in these coordinates.

Definition/convention — source terminology/construction

FC08-C15-U039 · Ch. 15, § Hypersurfaces in Riemannian Manifolds; source L11799 · after FC08-C15-U027 · not formalized

Hypersurfaces in Riemannian Manifolds Let $( M , g )$ be an oriented Riemannian manifold with or without boundary, and suppose $S \subseteq M$ is an immersed hypersurface with or without boundary. Any unit normal vector field along S is nowhere tangent to $S$ , so it determines an orientation of S by Proposition 15.21. The next proposition gives a simple formula for the volume form of the induced metric on S with respect to this orientation.

Proposition 15.32

FC08-C15-U040 · Ch. 15, § Hypersurfaces in Riemannian Manifolds; source L11801 · not formalized

Proposition 15.32. Let $( M , g )$ be an oriented Riemannian manifold with or without boundary, let $S \subseteq M$ be an immersed hypersurface with or without boundary, and let $\widetilde g$ denote the induced metric on S. Suppose N is a smooth unit normal vector field along S. With respect to the orientation of S determined by N , the volume form of $( S , { \widetilde { g } } )$ is given by \[ \omega_ {\widetilde {g}} = \iota_ {S} ^ {*} (N \lrcorner \omega_ {g}). \] Proof.

Proposition 15.33

FC08-C15-U041 · Ch. 15, § Hypersurfaces in Riemannian Manifolds; source L11820 · not formalized

Proposition 15.33. Suppose M is any Riemannian manifold with boundary. There is a unique smooth outward-pointing unit normal vector field N along @M

Corollary 15.34

FC08-C15-U042 · Ch. 15, § Hypersurfaces in Riemannian Manifolds; source L11828 · not formalized

If $(M,g)$ is an oriented Riemannian manifold with boundary and $\widetilde{g}$ is the induced metric on $\partial M$, then the volume form of $\widetilde{g}$ is \[ \omega_{\widetilde{g}} = \iota_{\partial M}^{*}\left(N \lrcorner\, \omega_{g}\right), \] where $N$ is the outward unit normal vector field along $\partial M$.

Proposition 15.35

FC08-C15-U043 · Ch. 15, § Orientations and Covering Maps; source L11842 · not formalized

Proposition 15.35. If $E \to M$ is a smooth covering map and M is orientable, then E is also orientable.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has topological covering-map infrastructure, but no smooth-manifold orientation-preserving predicate or orientability theorem with which to state the source result. Covering data alone is a proper subset. Strict whole-row semantics reject proper subsets, missing converse directions, unbridged tangent models, and substantive reconstruction from generic ingredients.

Definition/convention — source terminology/construction

FC08-C15-U044 · Ch. 15, § Orientations and Covering Maps; source L11846 · not formalized

The next theorem is more interesting. If G is a Lie group acting smoothly on a smooth manifold $E$ (on the left, say), we say the action is an orientation-preserving action if for each $g \in G$ , the diffeomorphism $x \mapsto g \cdot x$ is orientation-preserving.

Theorem 15.36

FC08-C15-U045 · Ch. 15, § Orientations and Covering Maps; source L11848 · not formalized

Theorem 15.36. Suppose E is a connected, oriented, smooth manifold with $o r$ without boundary, and $\pi \colon E \to M$ is a smooth normal covering map. Then M is orientable if and only if the action of $\operatorname { A u t } _ { \pi } ( E )$ on E is orientat ) + d (V d ) = d (V d ); \[ \] d _ {V} = d (V d ) + d (d (V ) ) = d (V d ).

Example 15.37

FC08-C15-U046 · Ch. 15, § Orientations and Covering Maps; source L11862 · after FC08-C04-U036 · not formalized

(Orientability of Projective Spaces). For $n \geq 1$, consider the smooth covering map $q \colon \mathbb{S}^{n} \to \mathbb{RP}^{n}$ of Example 4.35. Its only nontrivial covering automorphism is the antipodal map $\alpha(x) = -x$, which is orientation-preserving if and only if $n$ is odd; hence $\mathbb{RP}^{n}$ is orientable if and only if $n$ is odd.

Example 15.38

FC08-C15-U047 · Ch. 15, § Orientations and Covering Maps; source L11864 · after FC08-C10-U007, FC08-C15-U045 · not formalized

Example 15.38 (The Möbius Bundle and the Möbius Band). Let E be the total space of the Möbius bundle (Example 10.3). The quotient map $q \colon { \mathbb { R } } ^ { 2 } \to E$ used to define $E$ is a smooth normal covering map, and the covering automorphism group is isomorphic to $\mathbb { Z } ,$ , acting on $\mathbb { R } ^ { 2 }$ by $n \cdot ( x , y ) = \left( x + n , ( - 1 ) ^ { n } y \right)$ . (You can check this directly from the definitions, or you can accept this for now and wait until we have developed more machinery in Chapter 21, where a simpler proof is available; see Problem 21-9.) For n odd, the diffeomorphism $( x , y ) \mapsto n \cdot ( x , y )$ of $\mathbb { R } ^ { 2 }$ pulls back the orientation form dx $\wedge d y$ to $- d x \wedge d y$ , so the action of $\operatorname { A u t } _ { \pi } ( E )$ is not orientation-preserving. Thu

Definition/convention — neighborhood that

FC08-C15-U048 · Ch. 15, § The Orientation Covering; source L11872 · in Mathlib

In order to handle the orientable and nonorientable cases in a uniform way, it is useful to expand our definition of covering maps slightly, by allowing “covering spaces” that are not connected. If N and M are topological spaces, let us say that a map $\pi \colon N \to M$ is a generalized covering map if it satisfies all of the requirements for a covering map except that N might not be connected: this means that N is locally path-connected, is surjective and continuous, and each point $p \in M$ has a neighborhood that is evenly covered by . If in addition N and M are smooth manifolds with or without boundary and is a local diffeomorphism, we say it is a generalized smooth covering map.

Formalized. Mathlib/Topology/Connected/LocallyPathConnected.lean::LocallyPathConnectedSpace; Mathlib/Topology/Covering/Basic.lean::IsEvenlyCovered, IsCoveringMap, IsCoveringMap.continuous; Lean core::Function.Surjective — Mathlib’s IsCoveringMap already allows disconnected total spaces and states that every base point is evenly covered; unlike Lee’s generalized notion it does not require surjectivity. Thus Lee’s definition is exactly the short conjunction LocallyPathConnectedSpace N ∧ Function.Surjective π ∧ IsCoveringMap π. /tmp/fc08-c15-witness.lean compiles this definition and derives continuity from IsCoveringMap.continuous.

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

Lemma 15.39

FC08-C15-U049 · Ch. 15, § The Orientation Covering; source L11874 · not formalized

Lemma 15.39. Suppose N and M are topological spaces and $N M$ is a generalized covering map. If M is connected, then the restriction of to each component of N is a covering map.

Not formalized. none; no complete checked declaration under strict bundle semantics — No checked P/H theorem states that, for Lee’s generalized covering over a connected base, restriction to each connected component of the total space is a connected covering map. Proving surjectivity and the covering property componentwise would be substantive reconstruction. Strict whole-row semantics reject proper subsets, missing converse directions, unbridged tangent models, and substantive reconstruction from generic ingredients.

Definition/convention — source terminology/construction

FC08-C15-U050 · Ch. 15, § The Orientation Covering; source L11880 · not formalized

Let $M$ be a connected smooth positive-dimensional manifold with or without boundary, and let $\widehat{M}$ denote the set of orientations of all tangent spaces to $M$: \[ \widehat{M} = \{(p,\mathcal{O}_{p}) : p \in M \text{ and } \mathcal{O}_{p} \text{ is an orientation of } T_{p}M\}. \]

Not formalized. none; no complete checked declaration under strict bundle semantics — P/H has no orientation-covering construction for manifolds, and no manifold-orientability API from which its smooth structure, two-sheeted covering theorem, uniqueness, or fundamental-group criterion can be stated. Generic covering-space results do not own these rows. Strict whole-row semantics reject proper subsets, missing converse directions, unbridged tangent models, and substantive reconstruction from generic ingredients.

Construction/definition — orientation covering of M

FC08-C15-U051 · Ch. 15, § The Orientation Covering; source L11886 · not formalized

Define the projection $\widehat { \pi } \colon \widehat { M } \to M$ by sending an orientation of $T _ { p } M$ to the point $p$ itself: $\hat { \pi } ( p , \mathcal { O } _ { p } ) = p$ . Since each tangent space has exactly two orientations, each fiber of this map has cardinality 2. The map $\widehat { \pi } \colon \widehat { M } \to M$ is called the orientation covering of M . Proposition 15.40 (Properties of the Orientation Covering). Suppose

Proposition 15.40

FC08-C15-U052 · Ch. 15, § The Orientation Covering; source L11888 · not formalized

(Properties of the Orientation Covering). Suppose $M$ is a connected smooth positive-dimensional manifold with or without boundary and $\widehat{\pi} \colon \widehat{M} \to M$ is its orientation covering. Then $\widehat{M}$ can be given the structure of a smooth oriented manifold with or without boundary such that: (a) $\widehat{\pi}$ is a generalized smooth covering map; (b) a connected open subset $U \subseteq M$ is evenly covered by $\widehat{\pi}$ if and only if $U$ is orientable; (c) if $U \subseteq M$ is evenly covered, every orientation of $U$ is the pullback orientation induced by a local section of $\widehat{\pi}$ over $U$.

Theorem 15.41

FC08-C15-U053 · Ch. 15, § The Orientation Covering; source L11912 · not formalized

(Orientation Covering Theorem). Suppose $M$ is a connected smooth manifold with or without boundary and $\widehat{\pi} \colon \widehat{M} \to M$ is its orientation covering. (a) If $M$ is orientable, $\widehat{M}$ has exactly two components and the restriction of $\widehat{\pi}$ to each is a diffeomorphism onto $M$. (b) If $M$ is nonorientable, $\widehat{M}$ is connected and $\widehat{\pi}$ is a two-sheeted smooth covering map.

Definition/convention — oriented double covering of M

FC08-C15-U054 · Ch. 15, § The Orientation Covering; source L11925 · not formalized

The orientation covering is sometimes called the oriented double covering of M . There are other ways of constructing it besides the one we have given here, but as the next theorem shows, the specific details of the construction do not matter, because they all yield isomorphic covering manifolds.

Theorem 15.42

FC08-C15-U055 · Ch. 15, § The Orientation Covering; source L11927 · not formalized

Theorem 15.42 (Uniqueness of the Orientation Covering). Let M be a nonorientable connected smooth manifold with or without boundary, and let $\widehat { \pi } \colon \widehat { M } \to M$ be its orientation covering. If $\widetilde { M }$ is an oriented smooth manifold with or without boundary that admits a two-sheeted smooth covering map $\widetilde \pi \colon \widetilde { M } \to M$ ; then there exists a unique orientation-preserving diffeomorphism ’ $\widetilde M \to \widehat M$ such that ${ \hat { \pi } } \circ \varphi = { \widetilde { \pi } }$

Theorem 15.43

FC08-C15-U056 · Ch. 15, § The Orientation Covering; source L11933 · not formalized

Theorem 15.43. Let M be a connected smooth manifold with or without boundary, and suppose the fundamental group of M has no subgroup of index 2. Then M is orientable. In particular, if M is simply connected then it is orientable.