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

FC08 — Lee, Introduction to Smooth Manifolds.

This chapter contains 7 definitions, 10 theorems, 7 propositions, 2 lemmas, 3 corollaries, 3 examples, 1 construction and 1 convention.

Of the 34 statements checked against Lean, 2 are formalized somewhere and 32 are not.

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

Which versions of Lean and Mathlib were searched

Canonical block: FC08-C20-U001–FC08-C20-U034, exactly 34 unique contiguous rows.
Search order: project A=3b2239e161592472b34e02ad3b7da308f9ce7280, pinned Mathlib P=db584cd6d46c92f209a44c0f1c829460d327499d (Apache-2.0; Lean 4.33.0), current H=5315eef9e4ffb98e0f89f278b765c50a149f66ca (Apache-2.0; Lean 4.34.0-rc2), then indexed/current/external Lean search.
Result: 2 pinned mathlib rows (U029, U032) and 32 dated unmatched rows.
U029 maps exactly to LieIdeal and its bracket-closure theorem. U032 maps exactly to the Lie algebra homomorphism LieAlgebra.ad : g →ₗ⁅R⁆ End(g) with ad_apply.
P/H contain Lie groups, left-invariant vector fields, manifold Lie brackets, smooth actions, matrix exponentials, and abstract Lie algebra infrastructure, but targeted searches found no Lie-group exponential/one-parameter subgroup object, no closed subgroup theorem, no Lie correspondence/integration of Lie algebra actions, and no group adjoint representation differentiated to ad.
Accordingly the matrix-exponential rows are not promoted through a missing identification with Lee’s Lie-group exponential, and group-level adjoint/normal-subgroup rows are not inferred from the algebraic ad/LieIdeal objects.
N=2026-09-07 marks negative decisions; strict whole-row semantics apply uniformly.

Definition/convention — one-parameter subgroup of G

FC08-C20-U001 · Ch. 20, § One-Parameter Subgroups; source L15479 · not formalized

A one-parameter subgroup of $\pmb { G }$ is defined to be a Lie group homomorphism $\gamma \colon \mathbb { R } \to G$ , with R considered as a Lie group under addition. By this definition, a one-parameter subgroup is not a Lie subgroup of G, but rather a homomorphism into $G$ . (However, the image of a one-parameter subgroup is a Lie subgroup when endowed with a suitable smooth manifold structure; see Pr

Not formalized. none; no complete checked declaration under strict bundle semantics — P/H have Lie groups, left-invariant vector fields, ODE flows, and matrix exponentials, but no Lie-group exponential map or one-parameter-subgroup API, and no closed-subgroup theorem. The source row depends on that missing bridge. Strict whole-row semantics reject proper subsets, unbridged alternate encodings, and reconstruction.

Theorem 20.1

FC08-C20-U002 · Ch. 20, § One-Parameter Subgroups; source L15481 · not formalized

Theorem 20.1 (Characterization of One-Parameter Subgroups). Let G be a Lie group. The one-parameter subgroups $o f G$ are precisely the maximal integral curves of left-invariant vector fields starting at the identity.

Definition/convention — one-parameter subgroup generated by X

FC08-C20-U003 · Ch. 20, § One-Parameter Subgroups; source L15499 · not formalized

Given $X \in \operatorname { L i e } ( G )$ , the one-parameter subgroup determined by X in this way is called the one-parameter subgroup generated by X . Because left-invariant vector fields are uniquely determined by their values at the identity, it follows that each one-parameter subgroup is uniquely determined by its initial velocity in $T _ { e } G$ , and thus there are one-to-one correspondences \[ \{\text { one - parameter subgroups of } G \} \longleftrightarrow \operatorname{Lie} (G) \longleftrightarrow T _ {e} G. \]

Proposition 20.3

FC08-C20-U004 · Ch. 20, § One-Parameter Subgroups; source L15553 · not formalized

Proposition 20.3. Suppose G is a Lie group and $H \subseteq G$ is a Lie subgroup. The one-parameter subgroups of H are precisely those one-parameter subgroups of G whose initial velocities lie in $T _ { e } H$

Example 20.4

FC08-C20-U005 · Ch. 20, § One-Parameter Subgroups; source L15565 · after FC08-C08-U064 · not formalized

If $H$ is a Lie subgroup of $\mathrm{GL}(n,\mathbb{R})$, the one-parameter subgroups of $H$ are exactly the maps $\gamma(t) = e^{tA}$ for $A \in \mathfrak{h}$, where $\mathfrak{h} \subseteq \mathfrak{gl}(n,\mathbb{R})$ is the subalgebra corresponding to $\operatorname{Lie}(H)$ as in Theorem 8.46. Taking $H = \mathrm{O}(n)$ shows that the one-parameter subgroups of $\mathrm{O}(n)$ are the maps $\gamma(t) = e^{tA}$ for skew-symmetric $A$, and in particular that the exponential of a skew-symmetric matrix is orthogonal.

Construction/definition — exponential map of G

FC08-C20-U006 · Ch. 20, § The Exponential Map; source L15571 · not formalized

Given a Lie group $G$ with Lie algebra ${ \mathfrak { g } } ,$ , we define a map exp ${ \mathfrak { g } } \to G$ , called the exponential map of $\pmb { G }$ , as follows: for any $X \in { \mathfrak { g } }$ , we set \[ \exp X = \gamma (1), \] where $\gamma$ is the one-parameter subgroup generated by $X$ , or equivalently the integral curve of X starting at the identity (Fig. 20.1). The following proposition shows that, like the matrix exponential, this map sends the line through $X$ to the one-parameter ion on M .

Proposition 20.5

FC08-C20-U007 · Ch. 20, § The Exponential Map; source L15579 · not formalized

Proposition 20.5. Let G be a Lie group. For any $X \in \operatorname { L i e } ( G ) , \gamma ( s ) = \exp s X$ is the one-parameter subgroup of G generated by $X$

Example 20.6

FC08-C20-U008 · Ch. 20, § The Exponential Map; source L15592 · not formalized

Example 20.6. The results of the preceding section show that the exponential map of GL.n; R/ (or any Lie subgroup of it) is given by exp $A = e ^ { A }$ . This, obviously, is the reason for the term exponential map.

Example 20.7

FC08-C20-U009 · Ch. 20, § The Exponential Map; source L15594 · not formalized

If $V$ is a finite-dimensional real vector space, a choice of basis gives isomorphisms $\mathrm{GL}(V) \cong \mathrm{GL}(n,\mathbb{R})$ and $\mathfrak{gl}(V) \cong \mathfrak{gl}(n,\mathbb{R})$, so the exponential map of $\mathrm{GL}(V)$ is \[ \exp A = \sum_{k=0}^{\infty} \frac{1}{k!}A^{k}, \tag{20.2} \] where $A \in \mathfrak{gl}(V)$ is regarded as a linear map $V \to V$ and $A^{k} = A \circ \cdots \circ A$.

Proposition 20.8

FC08-C20-U010 · Ch. 20, § The Exponential Map; source L15602 · not formalized

Proposition 20.8 (Properties of the Exponential Map). Let G be a Lie group and let g be its Lie algebra. (a) The exponential map is a smooth map from g to G. (b) For any $X \in { \mathfrak { g } }$ and $s , t \in \mathbb { R } , \exp ( s + t ) X = \exp s X \exp t X$ (c) For any $X \in { \mathfrak { g } } , ( \exp X ) ^ { - 1 } = \exp ( - X )$ (d) For any $X \in { \mathfrak { g } }$ and $n \in \mathbb { Z } , ( \exp X ) ^ { n } = \exp ( n X )$ (e) The differential $( d \exp ) _ { 0 } \colon T _ { 0 } \mathfrak { g } \to T _ { e } G$ is the identity map, under the canonical identifications of both $T _ { 0 9 }$ and $T _ { e } G$ with g itself. (f) The exponential map restricts to a diffeomorphism from some neighborhood of 0 in g to a neighborhood of e in G. (g) If H is another Lie group, h is its Lie algebra, and $\phi \colon G \to H$ is a Lie group homomorphism, the following diagram commutes: \[ \begin{array}{c} \mathfrak {g} \xrightarrow {\Phi_ {*}} \mathfrak {h} \\ \exp \Biggl \downarrow \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \exp \\ G \xrightarrow {\Phi} H. \end{array}\tag{20.3} \] (h)

Proposition 20.9

FC08-C20-U011 · Ch. 20, § The Exponential Map; source L15679 · not formalized

Proposition 20.9. Let G be a Lie group, and let $H \subseteq G$ be a Lie subgroup. With Lie.H / considered as a subalgebra of Lie.G/ in the usual way, the exponential map of H is the restriction to Lie.H / of the exponential map of G, and \[ \operatorname{Lie} (H) = \left\{X \in \operatorname{Lie} (G): \exp t X \in H \text { for all } t \in \mathbb {R} \right\}. \]

Proposition 20.10

FC08-C20-U012 · Ch. 20, § The Closed Subgroup Theorem; source L15699 · not formalized

Proposition 20.10. Let G be a Lie group and let g be its Lie algebra. For any $X , Y \in { \mathfrak { g } }$ , there is a smooth function $Z \colon ( - \varepsilon , \varepsilon ) \to { \mathfrak { g } }$ for some $\varepsilon > 0$ such that the following identity holds for all $t \in ( - \varepsilon , \varepsilon )$ \[ (\exp t X) (\exp t Y) = \exp \left(t (X + Y) + t ^ {2} Z (t)\right).\tag{20.4} \]

Corollary 20.11

FC08-C20-U013 · Ch. 20, § The Closed Subgroup Theorem; source L15737 · not formalized

Corollary 20.11. Under the hypotheses of the preceding proposition, \[ \lim _ {n \rightarrow \infty} \left(\left(\exp \frac {t}{n} X\right)\left(\exp \frac {t}{n} Y\right)\right) ^ {n} = \exp t (X + Y).\tag{20.5} \]

Theorem 20.12

FC08-C20-U014 · Ch. 20, § The Closed Subgroup Theorem; source L15757 · not formalized

Theorem 20.12 (Closed Subgroup Theorem). Suppose G is a Lie group and $H \subseteq G$ is a subgroup that is also a closed subset of G. Then H is an embedded Lie subgroup.

Corollary 20.13

FC08-C20-U015 · Ch. 20, § The Closed Subgroup Theorem; source L15827 · not formalized

and Theorem 7.21. Corollary 20.13. If G is a Lie group and H is any subgroup of G, the following are equivalent: (a) H is closed in G. (b) H is an embedded submanifold of G. (c) H is an embedded Lie subgroup of G.

Convention/notation — source terminology/construction

FC08-C20-U016 · Ch. 20, § Infinitesimal Generators of Group Actions; source L15841 · not formalized

Suppose we are given a smooth right action of a Lie group G on a smooth manifold M; which we denote either by $\theta \colon M \times G \to M$ g$ , depending on context. Each element $ ( G )$ determines a smooth global flow on $

Not formalized. none; no complete checked declaration under strict bundle semantics — P/H have smooth group actions, Lie brackets, and abstract Lie homomorphisms, but no checked infinitesimal-generator integration theorem, Lie correspondence, or local-Lie-group fundamental theorem matching this row. Strict whole-row semantics reject proper subsets, unbridged alternate encodings, and reconstruction.

Lemma 20.14

FC08-C20-U017 · Ch. 20, § Infinitesimal Generators of Group Actions; source L15861 · not formalized

Suppose $G$ is a Lie group and $\theta$ is a smooth right action of $G$ on a smooth manifold $M$. For any $X \in \operatorname{Lie}(G)$ and $p \in M$, the vector fields $X$ and $\widehat{\theta}(X)$ are $\theta^{(p)}$-related.

Theorem 20.15

FC08-C20-U018 · Ch. 20, § Infinitesimal Generators of Group Actions; source L15877 · not formalized

Theorem 20.15. Suppose G is a Lie group and is a smooth right action of G on a smooth manifold M . Then the map L i e } ( G ) ( M )$ defined above is a Lie algebra homomorphism. Proof. For each $

Definition/convention — a (right) g-action

FC08-C20-U019 · Ch. 20, § Infinitesimal Generators of Group Actions; source L15887 · not formalized

The Lie algebra homomorphism $\widehat{\theta} \colon \operatorname{Lie}(G) \to \mathfrak{X}(M)$ is the infinitesimal generator of $\theta$. More generally, for an arbitrary finite-dimensional Lie algebra $\mathfrak{g}$, any Lie algebra homomorphism $\widehat{\theta} \colon \mathfrak{g} \to \mathfrak{X}(M)$ is a right $\mathfrak{g}$-action on $M$, and it is complete if $\widehat{\theta}(X)$ is a complete vector field for every $X \in \mathfrak{g}$.

Theorem 20.16

FC08-C20-U020 · Ch. 20, § Infinitesimal Generators of Group Actions; source L15891 · not formalized

(Fundamental Theorem on Lie Algebra Actions). Let $M$ be a smooth manifold, $G$ a simply connected Lie group and $\mathfrak{g} = \operatorname{Lie}(G)$. If $\widehat{\theta} \colon \mathfrak{g} \to \mathfrak{X}(M)$ is a complete $\mathfrak{g}$-action on $M$, then there is a unique smooth right $G$-action on $M$ whose infinitesimal generator is $\widehat{\theta}$.

Theorem 20.18

FC08-C20-U021 · Ch. 20, § Left Actions; source L15965 · not formalized

Suppose $G$ is a Lie group and $M$ a smooth manifold. (a) If $\theta$ is a smooth left action of $G$ on $M$, the map $\widehat{\theta} \colon \operatorname{Lie}(G) \to \mathfrak{X}(M)$ defined by (20.11) is an antihomomorphism: a linear map with $\widehat{\theta}([X,Y]) = -[\widehat{\theta}(X),\widehat{\theta}(Y)]$ for all $X, Y \in \operatorname{Lie}(G)$. (b) Conversely, if $G$ is simply connected, every antihomomorphism $\widehat{\theta} \colon \operatorname{Lie}(G) \to \mathfrak{X}(M)$ for which each $\widehat{\theta}(X)$ is complete is the infinitesimal generator of a unique left $G$-action.

Definition/convention — left g-action

FC08-C20-U022 · Ch. 20, § Left Actions; source L15973 · not formalized

Because of this theorem, for a finite-dimensional Lie algebra g and a smooth manifold M; a left g-action on M is defined as an antihomomorphism f

Theorem 20.19

FC08-C20-U023 · Ch. 20, § The Lie Correspondence; source L15983 · not formalized

Suppose $G$ and $H$ are Lie groups with $G$ simply connected, with Lie algebras $\mathfrak{g}$ and $\mathfrak{h}$. For any Lie algebra homomorphism $\varphi \colon \mathfrak{g} \to \mathfrak{h}$ there is a unique Lie group homomorphism $\Phi \colon G \to H$ with $\Phi_{*} = \varphi$.

Corollary 20.20

FC08-C20-U024 · Ch. 20, § The Lie Correspondence; source L16019 · not formalized

Corollary 20.20. If G and H are simply connected Lie groups with isomorphic Lie algebras, then G and H are isomorphic.

Theorem 20.21

FC08-C20-U025 · Ch. 20, § The Lie Correspondence; source L16025 · not formalized

Theorem 20.21 (The Lie Correspondence). There is a one-to-one correspondence between isomorphism classes of finite-dimensional Lie algebras and isomorphism classes of simply connected Lie groups, given by associating each simply connected Lie group with its Lie algebra. P

Definition/convention — left-invariant

FC08-C20-U026 · Ch. 20, § Lie’s Fundamental Theorems; source L16043 · not formalized

The left translation map $L _ { g } \colon U \to V$ is defined just as for ordinary Lie groups, and a vector field $X \in { \mathfrak { X } } ( U )$ is said to be left-invariant if $d ( L _ { g } ) _ { g ^ { \prime } } ( X _ { g ^ { \prime } } ) = X _ { m ( g , g ^ { \prime } ) }$ for all $g , g ^ { \prime } \in U$ such that $m ( g , g ^ { \prime } ) \in U$ . Two local Lie groups $( U , e , m , i )$ and $( U ^ { \prime } , e ^ { \prime } , m ^ { \prime } , i ^ { \prime } )$ are said to be locally isomorphic if there is a diffeomorphism from a neighborhood of $e$ in $U$ to a neighborhood of $e ^ { \prime }$ in $U ^ { \prime }$ that takes $e$ to $e ^ { \prime } .$ , m to $m ^ { \prime }$ , and i to $i ^ { \prime }$ , whenever the respective operations are defined. A local (left or right) action of a local Lie group on an open subset $W \subseteq \mathbb { R } ^ { n }$ is defined like an ordinary action, except that $g \cdot x \left( \operatorname { o r } x \cdot g \right)$ is required to be defined only for $( g , x )$ in a neighborhood of $\{ e \} \times W$ in $U \times W$ . A coordinate neighborhood of the identity in any Lie group is a local Lie group, and any smooth action of a Lie group on a smooth manifold restricts to a local action on any sufficiently small neighborhood.

Theorem 20.22

FC08-C20-U027 · Ch. 20, § Lie’s Fundamental Theorems; source L16045 · not formalized

(The Fundamental Theorems of Sophus Lie). (i) First: the left-invariant vector fields on a local Lie group form a finite-dimensional Lie algebra under the Lie bracket, and two local Lie groups with isomorphic Lie algebras are locally isomorphic. (ii) Second: for an open subset $W \subseteq \mathbb{R}^{n}$ there is a one-to-one correspondence between smooth right actions of local Lie groups on $W$ and finite-dimensional Lie subalgebras of $\mathfrak{X}(W)$. (iii) Third: for any finite-dimensional abstract Lie algebra $\mathfrak{g}$ there is a local Lie group whose algebra of left-invariant vector fields is isomorphic to $\mathfrak{g}$.

Lemma 20.23

FC08-C20-U028 · Ch. 20, § Normal Subgroups; source L16061 · not formalized

Lemma 20.23. Let G be a connected Lie group, and let $H \subseteq G$ be a connected Lie subgroup. Let g and h denote the Lie algebras of G and H , respectively. Then H is normal in G if and only if \[ (\exp X) (\exp Y) \bigl (\exp (- X) \bigr) \in H \quad f o r a l l X \in \mathfrak {g} a n d Y \in \mathfrak {h}.\tag{20.13} \]

Definition/convention — ideal in g

FC08-C20-U029 · Ch. 20, § Normal Subgroups; source L16077 · in Mathlib

Our next goal is a theorem that expresses a deep relationship between Lie groups and their Lie algebras. If $\mathfrak { g }$ is a Lie algebra, a linear subspace ${ \mathfrak { h } } \subseteq { \mathfrak { g } }$ $ and $Y \in { \mathfrak { h } }$ (see Problem 8-31). Because ideals are kernels of Lie algebra homomorphisms and normal subgroups are kernels of Lie group homomorphisms, it should not be surprising that there is a connection between ideals and normal subgroups. The key to analyzing this connection is the adjoint representation, which we study next. ## The Adjoint Representation Let G be a Lie group and g be its Lie algebra. For any $

Formalized. Mathlib/Algebra/Lie/Ideal.lean::LieIdeal, LieIdeal.lie_mem_right — LieIdeal is a Lie submodule of the Lie algebra acting on itself; lie_mem_right states closure under [X,Y] when Y lies in the ideal. This is exactly Lee’s linear-subspace ideal condition.

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

Definition/convention — source terminology/construction

FC08-C20-U030 · Ch. 20, § The Adjoint Representation; source L16081 · after FC08-C07-U006 · not formalized

Let $G$ be a Lie group with Lie algebra $\mathfrak{g}$. For any $g \in G$ the conjugation map $C_{g} \colon G \to G$, $C_{g}(h) = ghg^{-1}$, is a Lie group homomorphism, and $\operatorname{Ad}(g) = (C_{g})_{*} \colon \mathfrak{g} \to \mathfrak{g}$ denotes its induced Lie algebra homomorphism.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has algebraic conjugation and LieAlgebra.ad, but no Lie-group adjoint representation defined as the differential of conjugation, nor the derivative theorem Ad_* = ad; the group-to-Lie bridge required here is absent. Strict whole-row semantics reject proper subsets, unbridged alternate encodings, and reconstruction.

Proposition 20.24

FC08-C20-U031 · Ch. 20, § The Adjoint Representation; source L16083 · not formalized

Proposition 20.24 (The Adjoint Representation). If G is a Lie group with Lie algebra g, the map Ad $G \to { \mathrm { G L } } ( { \mathfrak { g } } )$ is a Lie group representation, called the adjoint represent 9.12) on $U$ and let $\psi = u - \widetilde { u }$ .

Proposition 20.25

FC08-C20-U032 · Ch. 20, § The Adjoint Representation; source L16097 · in Mathlib

For any Lie algebra $\mathfrak{g}$, the map $\operatorname{ad} \colon \mathfrak{g} \to \mathfrak{gl}(\mathfrak{g})$ is a Lie algebra representation, the adjoint representation of $\mathfrak{g}$.

Formalized. Mathlib/Algebra/Lie/OfAssociative.lean::LieAlgebra.ad, LieAlgebra.ad_apply — LieAlgebra.ad : g →ₗ⁅R⁆ Module.End R g is a Lie algebra homomorphism, and ad_apply identifies its value with the bracket. This is exactly the adjoint representation of a Lie algebra.

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

Theorem 20.27

FC08-C20-U033 · Ch. 20, § The Adjoint Representation; source L16103 · not formalized

Theorem 20.27. Let G be a Lie group, let g be its Lie algebra, and let Ad $G $ ${ \mathrm { G L } } ( { \mathfrak { g } } )$ be the adjoint representation of G. The induced Lie algebra representation $\operatorname { A d } _ { * } \colon { \mathfrak { g } } \to { \mathfrak { g l } } ( { \mathfrak { g } } )$ is given (19.14) is a necessary condition for (19.13) to have a solution in a neighborhood of each point $( x _ { 0 } , y _ { 0 } )$ with freely specified initial value $u ( x _ { 0 } , y _ { 0 } ) = z _ { 0 }$ .

Theorem 20.28

FC08-C20-U034 · Ch. 20, § Ideals and Normal Subgroups; source L16135 · not formalized

Theorem 20.28 (Ideals and Normal Subgroups). Let G be a connected Lie group, and suppose $H \subseteq G$ is a connected Lie subgroup. Then H is a normal subgroup of G if and only if Lie.H / is an ideal in Lie.G/.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib formalizes LieIdeal, but has no checked theorem relating ideals to connected normal Lie subgroups because the Lie-subgroup integration/correspondence layer is absent. Strict whole-row semantics reject proper subsets, unbridged alternate encodings, and reconstruction.