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

FC08 — Lee, Introduction to Smooth Manifolds.

This chapter contains 20 definitions, 4 theorems, 17 propositions, 3 lemmas, 7 corollaries, 13 examples and 5 conventions.

Of the 69 statements checked against Lean, 6 are formalized somewhere and 63 are not.

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

Which versions of Lean and Mathlib were searched

Canonical source block: FC08 Lee, Chapter 8, FC08-C08-U001–FC08-C08-U069, exactly 69 unique contiguous rows retrieved from FC08 — John M. Lee, Introduction to Smooth Manifolds through agent-memory.
Search order followed the Sweep-II plan: project source first at A=3b2239e161592472b34e02ad3b7da308f9ce7280, pinned Mathlib P=db584cd6d46c92f209a44c0f1c829460d327499d (Apache-2.0, Lean 4.33.0), current upstream Mathlib H=5315eef9e4ffb98e0f89f278b765c50a149f66ca (Apache-2.0, Lean 4.34.0-rc2), then targeted current/indexed/external Lean searches. No project-existing, package-import, or reference-port C08 owner survived strict whole-row checking.
C08 has 6 pinned mathlib rows and 63 dated unmatched rows. Positive rows are: U023, U045, U047, U048, U050, U067.
The controlling semantic boundary is inherited from promoted C03 and was rechecked for C08. Lee’s tangent vectors are the point-derivation model formalized by PointDerivation; Mathlib’s mature vector-field, tangent-bundle, local-frame, pullback, and mlieBracket APIs use the separate standard TangentSpace model. Pinned DerivationBundle.lean/LeftInvariantDerivation.lean document that the finite-dimensional C∞ real identification with the usual tangent space/vector fields should hold, but do not formalize it. Exact searches at P and H again found no PointDerivation ≃ TangentSpace or vector-field/global-derivation equivalence. Therefore C08 does not silently route Lee vector-field rows through standard-tangent APIs that C03 already treated as unbridged.
This boundary excludes several otherwise excellent matches deliberately. ContMDiffSection gives smooth standard-tangent sections and their real vector-space operations; ContMDiff.smul_section gives smooth-function multiplication; LocalFrame.lean gives local frames and coefficient smoothness criteria; VectorField.mlieBracket proves smoothness and the full bracket laws. /tmp/fc08-c08-witness.lean compiled all four clauses of Lee’s U039 bracket proposition in the standard tangent model, plus the smooth-section operations. Those checks establish adjacency, not equivalence to Lee’s derivation-defined vector fields.
U023 is independent of the missing bridge: Derivation ℝ C^∞⟮I,M;ℝ⟯ C^∞⟮I,M;ℝ⟯ exactly owns Lee’s definition of a global derivation. U024 remains unmatched precisely because the converse identification of such derivations with smooth vector fields is not formalized.
U045, U047, U048, U050, and U067 are likewise model-independent algebraic interfaces. Mathlib’s generic LieAlgebra, LieSubalgebra, LieHom/LieEquiv, IsLieAbelian, and Lie-homomorphism-to-Module.End/faithfulness interfaces specialize exactly to Lee’s real finite-dimensional definitions. The audit witness typechecked these interfaces at the pin.
For Lie groups, P has substantial adjacent machinery: GroupLieAlgebra I G := TangentSpace I 1, mulInvariantVectorField, smoothness and bracket invariance of those constructed fields, and the separate LeftInvariantDerivation Lie algebra. But there is no checked evaluation equivalence identifying Lee’s Lie algebra of all left-invariant vector fields with T_eG, and no bridge between the standard-tangent and derivation models. Consequently U043–U044 and U051–U059 are not inferred from these constructions.
The map/functor boundary is also explicit: neither P nor current H has a GroupLieAlgebra Lie homomorphism induced by a smooth group homomorphism, or a Lie functor. Targeted H searches found no GroupLieAlgebra.*LieHom, LieHom.*GroupLieAlgebra, LieSubgroup, or invariant-field evaluation equivalence. U060–U066 remain unmatched.
The submanifold-dependent rows U032–U034, U042, and U064–U066 inherit C05’s separate blocker: P/H still have no general embedded/immersed submanifold or Lie-subgroup package.
The orthonormal/global-frame block has partial infrastructure only. LocalFrame.lean explicitly refers to a planned OrthonormalFrame.lean, which is absent at both P and H; no named parallelizability theorem for Lie groups was found. U018–U021 and U055–U056 therefore remain unmatched independently of the tangent-model issue.
Targeted indexed search surfaced the current TauCeti Lie-groups roadmap, which independently records the Lie functor, closed-subgroup/Lie-subgroup theory, and Ado theorem as future targets rather than completed upstream interfaces. This was used only as secondary external evidence; route decisions are grounded in the exact checked revisions above.
N=2026-09-07 marks dated unmatched decisions after the prescribed search layers. Strict whole-row semantics apply uniformly.

Convention/notation — vector field

FC08-C08-U001 · Ch. 8, § Vector Fields on Manifolds; source L4877 · not formalized

If M is a smooth manifold with or without boundary, a vector field on M is a section of the map $\pi \colon T M \to M$ . More concretely, a vector field is a continuous map $X \colon M \to T M$ ; usually written $p \mapsto X _ { p }$ , with the property that \[ \pi \circ X = \operatorname{Id} _ {M},\tag{8.1} \] or equivalently, $X _ { p } \in T _ { p } M$ for each $p \in M$ . (We write the value of X at $p$ as $X _ { p }$ instead of $X ( p )$ to be consistent with our notation for elements of the tangent bundle, as well as to avoid conflict with the notation $v ( f )$ for the action of a vector on a function.) You should visualize a vector field on M in the same way as you visualize vector fields in Euclidean space: as an arrow attached to each point of M; chosen to be tangent to M and to vary continuously from point eft is zero.

Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib has a rich standard-tangent vector-field API (TangentSpace, TangentBundle, smooth sections, local frames and coefficient criteria), but Lee’s tangent spaces in this source were introduced via point derivations. As recorded in FC08 C03, no checked PointDerivation ≃ TangentSpace bridge exists at P or H. Therefore these vector-field/coordinate-component rows cannot be routed through the standard tangent model. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Definition/convention — compactly supported

FC08-C08-U002 · Ch. 8, § Vector Fields on Manifolds; source L4888 · after FC08-C03-U031 · not formalized

We are primarily interested in smooth vector fields, the ones that are smooth as maps from M to TM; when TM is given the smooth manifold structure described in Proposition 3.18. In addition, for some purposes it is useful to consider maps from M to TM that would be vector fields except that they might not be continuous. A rough vector field on M is a (not necessarily continuous) map $X \colon M \to T M$ satisfying (8.1). Just as for functions, if X is a vector field on M; the support of X is defined to be the closure of the set $\{ p \in M : X _ { p } \neq 0 \}$ . A vector field is said to be compactly supported if its support is a compact set.

Definition/convention — component functions of X in the given chart

FC08-C08-U003 · Ch. 8, § Vector Fields on Manifolds; source L4890 · not formalized

Suppose M is a smooth n-manifold (with or without boundary). If $X \colon M \to T M$ is a rough vector field and $\left( U , \left( x ^ { i } \right) \right)$ is any smooth coordinate chart for M; we can write the value of X at any point $p \in U$ in terms of the coordinate basis vectors: \[ X _ {p} = X ^ {i} (p) \left. \frac {\partial}{\partial x ^ {i}} \right| _ {p}.\tag{8.2} \] This defines n functions $X ^ { i } \colon U \mathbb { R }$ , called the com basis for $\mathbb { C } ^ { n }$ with respect to the Hermitian dot product $\begin{array} { r } { z \cdot w = \sum _ { i } z ^ { i } \overline { { w ^ { i } } } } \end{array}$ .

Proposition 8.1

FC08-C08-U004 · Ch. 8, § Vector Fields on Manifolds; source L4898 · not formalized

Proposition 8.1 (Smoothness Criterion for Vector Fields). Let M be a smooth manifold with or without boundary, and let $X \colon M \to T M$ be a rough vector field. $I f \left( U , \left( x ^ { i } \right) \right)$ is any smooth coordinate chart on M; then the restriction of X to U is smooth if and only if its component functions with respect to t

Example 8.2

FC08-C08-U005 · Ch. 8, § Vector Fields on Manifolds; source L4908 · not formalized

Example 8.2 (Coordinate Vector Fields). If $\left( U , \left( x ^ { i } \right) \right)$ is any smooth chart on $M ,$ the assignment \[ p \mapsto \left. \frac {\partial}{\partial x ^ {i}} \right| _ {p} \] determines a vector field on $U$ , called the i th coordinate vector field and denoted by $\partial / \partial x ^ { i }$ . It is smooth because its component fu automorphism of N (i.e., an isomorphism from N to itself).

Example 8.3

FC08-C08-U006 · Ch. 8, § Vector Fields on Manifolds; source L4916 · not formalized

Example 8.3 (The Euler Vector Field). The vector field $V$ on $\mathbb { R } ^ { n }$ whose value at $x \in \mathbb { R } ^ { n }$ is \[ V _ {x} = x ^ {1} \left. \frac {\partial}{\partial x ^ {1}} \right| _ {x} + \dots + x ^ {n} \left. \frac {\partial}{\partial x ^ {n}} \right| _ {x} \] is smooth because its coordinate functions are linear. It vanishes at the origin, and points radially outward everywhere else. It is called the Euler vector field because of its appearance in Euler’s homogeneous function theorem (see Problem

Not formalized. none; no complete checked declaration under strict bundle semantics — These are explicit Euclidean/circle/torus vector-field examples in Lee’s derivation-defined tangent model. Generic smooth maps, circle/torus manifold infrastructure, and standard-tangent sections are adjacent, but no checked declaration packages the complete example; the missing derivation↔︎TangentSpace bridge also prevents importing standard-tangent field proofs. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Example 8.4

FC08-C08-U007 · Ch. 8, § Vector Fields on Manifolds; source L4924 · not formalized

(The Angle Coordinate Vector Field on the Circle). Let $\theta$ be any angle coordinate on a proper open subset $U \subseteq \mathbb{S}^{1}$ and let $d/d\theta$ be the corresponding coordinate vector field. It is smooth because its component function is constant in any such chart. The resulting global vector field is written $d/d\theta$, although strictly it is not a coordinate vector field on the whole circle at once.

Example 8.5

FC08-C08-U008 · Ch. 8, § Vector Fields on Manifolds; source L4926 · not formalized

Example 8.5 (Angle Coordinate Vector Fields on Tori). On the n-dimensional torus $\mathbb { T } ^ { n }$ , choosing an angle function $\theta ^ { i }$ for the i th circle factor, $i = 1 , \ldots , n$ , yields local coordinates $\left( \theta ^ { 1 } , \ldots , \theta ^ { n } \right)$ for $\mathbb { T } ^ { n }$ . An analysis similar to that of the previous example shows that the coordinate vector fields $\partial / \partial \theta ^ { 1 } , \ldots , \partial / \partial \theta ^ { n }$ are smooth and globa and H , respectively.

Definition/convention — vector field along a subset

FC08-C08-U009 · Ch. 8, § Vector Fields on Manifolds; source L4930 · after FC08-C02-U033 · not formalized

The next lemma is a generalization of Lemma 2.26 to vector fields, and is proved in much the same way. If M is a smooth manifold with or without boundary and $A \subseteq M$ is an arbitrary subset, a vector field along A is a continuous map $X \colon A \to$ TM satisfying $X = _ { A } $ (or in other words $X _ { p } \in T _ { p } M$ for each $p \in A )$ . We call it a smooth vector field along A if for each $p \in A$ , there is a neighborhood $V$ of $p$ in M and a smooth vector field $\widetilde { X }$ on $V$

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has local extension of a vector-bundle fiber element and partition-of-unity machinery for constructing smooth sections, but no checked theorem matching Lee’s vector-field-along-a-closed-set extension with prescribed support or the global prescribed-value theorem. Moreover these APIs live in the standard TangentSpace model, still unbridged from Lee’s point-derivation tangent spaces. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Lemma 8.6

FC08-C08-U010 · Ch. 8, § Vector Fields on Manifolds; source L4932 · not formalized

on $V \cap A$ Lemma 8.6 (Extension Lemma for Vector Fields). Let M be a smooth manifold with or without boundary, and let $A \subseteq M$ be a closed subset. Suppose X is a smooth vector field along A. Given any open subset U containing A, there exists a smooth global vector field $\widetilde { X }$ on M such that ${ \tilde { X } } | _ { A } = X$

Proposition 8.7

FC08-C08-U011 · Ch. 8, § Vector Fields on Manifolds; source L4938 · not formalized

Proposition 8.7. Let M be a smooth manifold with or without boundary. Given $p \in M$ and $v \in T _ { p } M$ ; there is a smooth global vector field X on M such tha $X _ { p } = v$

Convention/notation — source terminology/construction

FC08-C08-U012 · Ch. 8, § Vector Fields on Manifolds; source L4942 · not formalized

If M is a smooth manifold with or without boundary, it is standard to use the notation ${ \mathfrak { X } } ( M )$ to denote the set of all smooth vector fields on M . It is a vector space under pointwise addition and scalar multiplication: \[ (a X + b Y) _ {p} = a X _ {p} + b Y _ {p}. \] The zero oup.

Not formalized. none; no complete checked declaration under strict bundle semantics — ContMDiffSection and ContMDiff.smul_section directly provide the corresponding vector-space/smooth-function operations for standard-tangent smooth sections, and the audit witness typechecks them. They are nevertheless not promoted because C03 established that Mathlib’s standard TangentSpace is not checked equivalent to Lee’s derivation-defined T_pM; using them here would silently cross that same missing bridge. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Definition/convention — f X

FC08-C08-U013 · Ch. 8, § Vector Fields on Manifolds; source L4948 · not formalized

The zero element of this vector space is the zero vector field, whose value at each $p \in M$ is $0 \in T _ { p } M$ . In addition, smooth vector fields can be multiplied by smooth real-valued functions: if $f \in C ^ { \infty } ( M )$ and $X \in { \mathfrak { X } } ( M )$ , we define $f X \colon M \to T M$ by \[ (f X) _ {p} = f (p) X _ {p}. \]

Proposition 8.8

FC08-C08-U014 · Ch. 8, § Vector Fields on Manifolds; source L4956 · not formalized

Proposition 8.8. Let M be a smooth manifold with or without boundary. (a) If X and Y are smooth vector fields on M and f; $g \in C ^ { \infty } ( M )$ , then $f X + g Y$ is a smooth vector field. (b) X.M / is a module over the ring $C ^ { \infty } ( M ) .$

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib proves that smooth scalar functions multiply smooth vector-bundle sections and bundles the base-field module on ContMDiffSection, but it does not bundle the full C^∞(M)-module instance asserted by Lee. The standard-tangent/point-derivation bridge is also absent. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Convention/notation — global frame

FC08-C08-U015 · Ch. 8, § Local and Global Frames; source L4976 · not formalized

or without boundary. An ordered $k \mathrm { - }$ tuple $( X _ { 1 } , \ldots , X _ { k } )$ of vector fields defined on some subset $A \subseteq M$ is said to be linearly independent if $\left( X _ { 1 } | _ { p } , \ldots , X _ { k } | _ { p } \right)$ is a linearly independent k-tuple in $T _ { p } M$ for each $p \in A$ , and is said to span the tangent bundle if the k-tuple $\left( X _ { 1 } | _ { p } , \ldots , X _ { k } | _ { p } \right)$ spans $T _ { p } M$ at each $p \in A$ . A local frame for M is an ordered n-tuple of vector fields $( E _ { 1 } , \ldots , E _ { n } )$ defined on an open subset $U \subseteq M$ that is linearly independen and spans the tangent bundle; thus the vectors $( E _ { 1 } | _ { p } , \ldots , E _ { n } | _ { p } )$ form a basis for $T _ { p } M$ at each $p \in U$ . It is called a global frame if $U = M$ ; and a smooth frame if each of the vector fields $E _ { i }$ is smooth. We often use the shorthand notation $( E _ { i } )$ to denote a frame $( E _ { 1 } , \ldots , E _ { n } )$ . If M has dimension n, then to check that an ordered n-tuple of vector fields $( E _ { 1 } , \ldots , E _ { n } )$ is a local frame, it suffices to check either that it is linearly independent or that it spans A faithful representation of E.n/ is given by the map $\rho \colon \operatorname { E } ( n ) \operatorname { G L } ( n + 1 , \mathbb { R } )$ defined in block form by \[ \rho (b, A) = \left( \begin{array}{c c} A & b \\ 0 & 1 \end{array} \right), \] where b is considered as a column matrix.

Not formalized. none; no complete checked declaration under strict bundle semantics — IsLocalFrameOn, bundle trivializations, and local-frame coefficient APIs formalize substantial smooth-frame infrastructure in the standard tangent/vector-bundle model. The complete Lee row additionally uses his derivation-defined tangent spaces and, in the orthonormal/parallelizable rows, interfaces not present at P/H (OrthonormalFrame is explicitly only planned). No whole-row owner survives the C03 tangent-model boundary. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Example 8.10

FC08-C08-U016 · Ch. 8, § Local and Global Frames; source L4978 · after FC08-C08-U007 · not formalized

(Local and Global Frames). (a) The standard coordinate vector fields form a smooth global frame for $\mathbb{R}^{n}$. (b) For any smooth chart $(U,(x^{i}))$ on a smooth manifold $M$, possibly with boundary, the coordinate vector fields form a smooth local frame $(\partial/\partial x^{i})$ on $U$, a coordinate frame; every point of $M$ lies in the domain of such a frame. (c) The vector field $d/d\theta$ of Example 8.4 is a smooth global frame for the circle. (d) The $n$-tuple $(\partial/\partial\theta^{1},\dots,\partial/\partial\theta^{n})$ on the $n$-torus is a smooth global frame for $\mathbb{T}^{n}$.

Proposition 8.11

FC08-C08-U017 · Ch. 8, § Local and Global Frames; source L4990 · not formalized

Proposition 8.11 (Completion of Local Frames). Let M be a smooth n-manifold with or without boundary. (a) 1 } , , X _ { k } )$ is a linearly independent k-tuple of smooth vector fields on an open subset $ ; with $1 \leq k < n$ , then for each $p \in U$ there exist smooth vector fields 1 } , , X _ { n }$ in a neighborhood V of p such that $ 1 } , , X _ { n } )$ is a smooth local frame for M on $ _ { 1 } , , v _ { k } )$ is a linearly independent k-tuple of vectors in $T M$ ; with $1 \leq k \leq n$ , then there exists a smooth local frame $( X _ { i } )$ on a neighborhood of p such that $X _ { i } | _ { p } = v _ { i } f o r i = 1 , . . . , f ( X _ { 1 } , \ldots , X _ { n } )$ is a linearly independent n-tuple of smooth vector fields along a closed subset $ _ { 1 } , , _ { n } )$ on some neighborhood of A such that $ _ { i } | _

Definition/convention — orthonormal frame

FC08-C08-U018 · Ch. 8, § Local and Global Frames; source L5000 · not formalized

For subsets of $\mathbb { R } ^ { n }$ , there is a special type of frame that is often more useful for geometric problems than arbitrary frames. A k-tuple of vector fields $( E _ { 1 } , \ldots , E _ { k } )$ defined on some subset $A \subseteq \mathbb { R } ^ { n }$ is said to be orthonormal if for each $p \in A$ , the vectors $\left( E _ { 1 } | _ { p } , \ldots , E _ { k } | _ { p } \right)$ are orthonormal with respect to the Euclidean dot product (where we identify $T _ { p } \mathbb { R } ^ { n }$ with $\mathbb { R } ^ { n }$ in the usual way). A (local or global) frame consisting of orthonormal vector fields te the matrix entries of $\rho ( g )$ with respect to this basis, it follows that $\rho _ { j } ^ { i } ( g ) = \pi ^ { i } \left( g \cdot E _ { i } \right)$ so each function $\rho _ { j } ^ { i }$ is a composition of smooth functions.

Example 8.12

FC08-C08-U019 · Ch. 8, § Local and Global Frames; source L5002 · not formalized

Example 8.12. The standard coordinate frame is a global orthonormal frame on $\mathbb { R } ^ { n }$ For a less obvious example, consider the smooth vector fields defined on $\mathbb { R } ^ { 2 } \setminus \{ 0 \}$ by \[ E _ {1} = \frac {x}{r} \frac {\partial}{\partial x} + \frac {y}{r} \frac {\partial}{\partial y}, \quad E _ {2} = - \frac {y}{r} \frac {\partial}{\partial x} + \frac {x}{r} \frac {\partial}{\partial y},\tag{8.3} \] where $r = \sqrt { x ^ { 2 } + y ^ { 2 } }$ . A straightforward computation shows that $( E _ { 1 } , E _ { 2 } )$ is an orthonormal frame for $\mathbb { R } ^ { 2 }$ over the open subset $\mathbb { R } ^ { 2 } \setminus \{ 0 \}$ . Geometrically, $E _ { 1 }$ and $E _ { 2 }$ are unit vector fields tangent to radial lines and circles centered at the origin.

Lemma 8.13

FC08-C08-U020 · Ch. 8, § Local and Global Frames; source L5012 · not formalized

Lemma 8.13 (Gram–Schmidt Algorithm for Frames). Suppose $( X _ { j } )$ is a smooth local frame for $T \mathbb { R } ^ { n }$ over an open subset $U \subseteq \mathbb { R } ^ { n }$ . 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)$ fo othness of the inversion map is redundant: if $G$ is a smooth manifold with a group structure such that the multiplication map m $G \times G \to G$ is smooth, then G is a Lie group.

Definition/convention — parallelizable

FC08-C08-U021 · Ch. 8, § Local and Global Frames; source L5022 · after FC08-C08-U016 · not formalized

a smooth orthonormal frame on U that satisfies the conclusion of the lemma. Although smooth local frames are plentiful, global ones are not. A smooth manifold with or without boundary is said to be parallelizable if it admits a smooth global frame. Example 8.10 shows that $\mathbb { R } ^ { n } , \mathbb { S } ^ { 1 }$ , and $\mathbb { T } ^ { n }$ are all parallelizable. Problems 8-6 and 8-7 show that $\mathbb { S } ^ { 3 }$ and $\mathbb { S } ^ { 7 }$ are parallelizable. Later in this chapter, we will see that all Lie groups are parallelizable (see Corollary 8.39 below). However, despite the evidence of these examples, most smooth manifolds are not parallelizable. (As we will see in Chapter 10, parallelizability of M is intimately connected to the question of whether its tangent bundle is diff on pp.

Proposition 8.14

FC08-C08-U022 · Ch. 8, § Local and Global Frames; source L5042 · not formalized

Proposition 8.14. Let M be a smooth manifold with or without boundary, and le X M TM be a rough vector field. The following are equivalent: (a) X is smooth. (b) For every $f \in C ^ { \infty } ( M )$ , the function Xf is smooth on M . (c) For every open subset $U \subseteq M$ and every $f \in C ^ { \infty } ( U )$ , the function $X f$ is smooth on $U$

Not formalized. none; no complete checked declaration under strict bundle semantics — Lee characterizes smooth vector fields by their action on all smooth functions. This is precisely where a checked identification between tangent-vector fields and global derivations is needed. Mathlib has both sides separately, but LeftInvariantDerivation.lean explicitly notes that the finite-dimensional vector-field/derivation identification is not formalized; U024’s global correspondence is likewise absent. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Definition/convention — derivation (as distinct

FC08-C08-U023 · Ch. 8, § Local and Global Frames; source L5076 · in Mathlib

as you can easily check by evaluating both sides at an arbitrary point $p \in M$ } ( M )$ is called a derivation (as distinct from a derivation at $p ,$ defined in Chapter 3) if it is linear over R and satisfies (8.5) for all $f

Formalized. Mathlib/RingTheory/Derivation/Basic.lean::Derivation, Derivation.leibniz; Mathlib/Geometry/Manifold/Algebra/SmoothFunctions.lean::ContMDiffMap — Specializing Derivation to Derivation ℝ C^∞⟮I,M;ℝ⟯ C^∞⟮I,M;ℝ⟯ is exactly Lee’s global derivation: an ℝ-linear endomorphism of the smooth-function algebra satisfying Leibniz. The C08 witness typechecks this specialization at P.

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

Proposition 8.15

FC08-C08-U024 · Ch. 8, § Local and Global Frames; source L5080 · not formalized

Proposition 8.15. Let M be a smooth manifold with or without boundary. A map $D \colon C ^ { \infty } ( M ) \to C ^ { \infty } ( M )$ is a derivation if and only if it is of the form $D f = X f f o r$ some smooth vector field $X \in { \mathfrak { X } } ( M ) .$

Not formalized. none; no complete checked declaration under strict bundle semantics — Generic global derivations are formalized (U023), but the theorem identifying every derivation of C^∞(M) with a unique smooth vector field is not. This is the missing global counterpart of the unformalized PointDerivation ≃ TangentSpace bridge recorded in C03. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Definition/convention — source terminology/construction

FC08-C08-U025 · Ch. 8, § Vector Fields and Smooth Maps; source L5099 · not formalized

Suppose $F \colon M \to N$ is smooth and X is a vector field on M; and suppose there happens to be a vector field Y on N with the property that for each $p \in M ,$ $d F _ { p } ( X _ { p } ) = Y _ { F ( p ) }$ . In this case, we say the vector fields X and Y are F -related (see $\mathrm { F i g . } \ 8 . 3 )$ . The next proposition shows how F -related vector fields act on smooth w Lie group homomorphisms induce homomorphisms of their Lie algebras, from which it follows that isomorphic Lie groups have isomorphic Lie algebras.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib’s standard-tangent mfderiv/mpullback API supplies nearby derivative and diffeomorphism transport identities, but there is no bundled Lee-style F-related/pushforward interface realizing this full row. More fundamentally, those fields use standard TangentSpace, still unbridged from Lee’s derivation tangent model. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Proposition 8.16

FC08-C08-U026 · Ch. 8, § Vector Fields and Smooth Maps; source L5101 · not formalized

Proposition 8.16. Suppose $F \colon M \to N$ is a smooth map between manifolds with or without boundary, $X \in { \mathfrak { X } } ( M )$ , and $Y \in { \mathfrak { X } } ( N )$ . Then X and Y are F -related if and only if for every smooth real-valued function f defined on an open sub s a smooth manifold with or without boundary, a vector field on M is a section of the map $\pi \colon T M \to M$ .

Example 8.17

FC08-C08-U027 · Ch. 8, § Vector Fields and Smooth Maps; source L5121 · not formalized

Example 8.17. Let $F \colon { \mathbb { R } } \to { \mathbb { R } } ^ { 2 }$ be the smooth map $F ( t ) = ( \cos t , \sin t )$ . Then $d / d t \in { \mathfrak { X } } ( \mathbb { R } )$ is F -related to the vector field $Y \in \mathcal { X } \left( \mathbb { R } ^ { 2 } \right)$ defined by \[ Y = x \frac {\partial}{\partial y} - y \frac {\partial}{\partial x}.\tag{//} \]

Proposition 8.19

FC08-C08-U028 · Ch. 8, § Vector Fields and Smooth Maps; source L5134 · not formalized

Proposition 8.19. Suppose M and N are smooth manifolds with or without boundary, and $F \colon M \to N$ is a diffeomorphism. For every $X \in { \mathfrak { X } } ( M )$ , there is a unique smooth vector field on N that is F -re is said to be compactly supported if its support is a compact set.

Convention/notation — source terminology/construction

FC08-C08-U029 · Ch. 8, § Vector Fields and Smooth Maps; source L5150 · after FC08-C08-U028 · not formalized

In the situation of the preceding proposition we denote the unique vector field that is F -related to X by $F _ { * } X$ , and call it the pushforward of X by F . Remember, it is only when F is a diffeomorphism that $F _ { * } X$ is defined. The proof of Proposition 8.19 shows that $F _ { * } X$ is defined explicitly by the formula \[ (F _ {*} X) _ {q} = d F _ {F ^ {- 1} (q)} \bigl (X _ {F ^ {- 1} (q)} \bigr).\tag{8.7} \]

Example 8.20

FC08-C08-U030 · Ch. 8, § Vector Fields and Smooth Maps; source L5158 · after FC08-C08-U026 · not formalized

Example 8.20 (Computing the Pushforward of a Vector Field). Let M and N be the following open submanifolds of $\mathbb { R } ^ { 2 }$ : \[ \begin{array}{l} M = \big \{(x, y): y > 0 \text { and } x + y > 0 \big \}, \\ N = \big \{(u, v): u > 0 \text { and } v > 0 \big \}, \end{array} \] and define $F \colon M \to N$ by $F ( x , y ) = ( x + y , x / y + 1 )$ . Then F is a diffeomorphism because its inverse is easily computed: just solve $( u , v ) = ( x + y , x / y + 1 )$ for x and y to obtain the formula $( x , y ) = F ^ { - 1 } ( u , v ) = ( u - u / v , ~ u / v )$ . Let us compute the pushforward $F _ { * } X$ , where X is the following smooth vector field on M : \[ X _ {(x, y)} = y ^ {2} \frac {\partial}{\partial x} \Big | _ {(x, y)}. \] The differential of F at a point $( x , y ) \in M$ is represented by its Jacobian matrix, \[ D F (x, y) = \left( \begin{array}{c c} 1 & 1 \\ \frac {1}{y} & - \frac {x}{y ^ {2}} \end{array} \right), \] and thus $d F _ { F ^ { - 1 } ( u , v ) }$ is represented by the matrix \[ D F \left(u - \frac {u}{v}, \frac {u}{v}\right) = \left( \begin{array}{c c} 1 & 1 \\ \frac {v}{u} & \frac {v - v ^ {2}}{u} \end{array} \right). \] For any $( u , v ) \in N$ \[ X _ {F ^ {- 1} (u, v)} = \frac {u ^ {2}}{v ^ {2}} \left. \frac {\partial}{\partial x} \right| _ {F ^ {- 1} (u, v)}. \] Therefore, applying (8.7) with $\boldsymbol { p } = \left( u , v \right)$ yields the formula for $F _ { * } X$ \[ (F _ {*} X) _ {(u, v)} = \left. \frac {u ^ {2}}{v ^ {2}} \frac {\partial}{\partial u} \right| _ {(u, v)} + \left. \frac {u}{v} \frac {\partial}{\partial v} \right| _ {(u, v)}. \] The next corollary follows directly from Proposition 8.16. Corollary 8.21. Suppose

Corollary 8.21

FC08-C08-U031 · Ch. 8, § Vector Fields and Smooth Maps; source L5196 · not formalized

Suppose $F \colon M \to N$ is a diffeomorphism and $X \in \mathfrak{X}(M)$. For any $f \in C^{\infty}(N)$, \[ \big((F_{*}X)f\big) \circ F = X(f \circ F). \]

Definition/convention — tangent to S at p

FC08-C08-U032 · Ch. 8, § Vector Fields and Submanifolds; source L5204 · not formalized

M$ is an immersed or embedded submanifold (with or without boundary), a vector field X on M does not necessarily restrict to a vector field on S, because $X _ { p }$ may not lie in the subspace $T _ { p } S T _ { p } M$ at a point $p S$ Given a point $p S$ a vector field X on M is said to be tangent to S at p if $X _ { p T _ { p } M$ . It is tangent to S if it is tangent to S at every point of S (Fig. 8.4). Proposition 8.22. Let M be a smooth manifold, $

Not formalized. none; no complete checked declaration under strict bundle semantics — These rows require arbitrary immersed/embedded submanifolds and their ambient tangent-space inclusion. C05 established that P/H have no general submanifold object/package; the standard-tangent/derivation bridge is also missing. The source statements therefore cannot be expressed completely in the checked interface. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Proposition 8.22

FC08-C08-U033 · Ch. 8, § Vector Fields and Submanifolds; source L5206 · not formalized

Proposition 8.22. Let M be a smooth manifold, $S \subseteq M$ be an embedded submanifold with or without boundary, and X be a smooth vector field on M . Then X is tangent to S if and only $i f ( X f ) | _ { S } = 0$ for every $f \in C ^ { \infty } ( M )$ such that $f | _ { S } \equiv 0$

Proposition 8.23

FC08-C08-U034 · Ch. 8, § Vector Fields and Submanifolds; source L5217 · not formalized

Proposition 8.23 (Restricting Vector Fields to Submanifolds). Let M be a smooth manifold, let $S \subseteq M$ be an immersed submanifold with or without boundary, and let $S \hookrightarrow M$ denote the inclusion map. If $Y \in { \mathfrak { X } } ( M )$ is tangent to S, then there is a unique smooth vector field on S, denoted by $Y | _ { S }$ , that is -related tor field along A is a continuous map $X \colon A \to$ TM satisfying $X = _ { A } $ (or in other words $X _ { p } \in T _ { p } M$ for each $p \in A )$ .

Example 8.24

FC08-C08-U035 · Ch. 8, § Lie Brackets; source L5231 · not formalized

Example 8.24. Define vector fields $X = \partial / \partial x$ and $Y = x \partial / \partial y$ on $\mathbb { R } ^ { 2 }$ , and let $f ( x , y ) = x , g ( x , y ) = y$ . Then direct computation shows that $X Y ( f g ) = 2 x $ , while $f X Y g + g X Y f = x$ , so $X Y$ is not a derivation of $C ^ { \infty } \left( \mathbb { R } ^ { 2 } \right)$

Not formalized. none; no complete checked declaration under strict bundle semantics — No checked declaration packages Lee’s explicit X=∂/∂x, Y=x∂/∂y calculation showing composition of vector fields is not a derivation. Generic calculus/derivation primitives would require reconstructing the example, and the coordinate-field model is itself behind the tangent bridge. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Lemma 8.25

FC08-C08-U036 · Ch. 8, § Lie Brackets; source L5241 · not formalized

Lemma 8.25. The Lie bracket of any pair of smooth vector fields is a smooth vector field.

Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned VectorField.mlieBracket has a theorem ContMDiff.mlieBracket_vectorField proving the bracket of smooth standard-tangent fields is smooth, and the audit witness compiles it. It is not promoted because those fields are in Mathlib’s standard TangentSpace model, with no checked equivalence to Lee’s derivation-defined tangent fields. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Proposition 8.26

FC08-C08-U037 · Ch. 8, § Lie Brackets; source L5259 · not formalized

Proposition 8.26 (Coordinate Formula for the Lie Bracket). Let X; Y be smooth vector fields on a smooth manifold M with or without boundary, and let $X =$ $X ^ { i } \partial / \partial x ^ { i }$ and $Y = Y ^ { j } \partial / \partial x ^ { j }$ be the coordinate expressions for X and Y in terms of some smooth local coordinates $\left( x ^ { i } \right)$ for M . Then $[ X , Y ]$ has the following coordinate expression: \[ [ X, Y ] = \left(X ^ {i} \frac {\partial Y ^ {j}}{\partial x ^ {i}} - Y ^ {i} \frac {\partial X ^ {j}}{\partial x ^ {i}}\right) \frac {\partial}{\partial x ^ {j}},\tag{8.8} \] or more concisely, \[ [ X, Y ] = \big (X Y ^ {j} - Y X ^ {j} \big) \frac {\partial}{\partial x ^ {j}}.\tag{8.9} \]

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib defines the manifold Lie bracket through charts and has extensive local formulas, but no checked declaration packages Lee’s coordinate-expression/example as this row. The standard-tangent/derivation-model bridge is also absent. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Example 8.27

FC08-C08-U038 · Ch. 8, § Lie Brackets; source L5287 · not formalized

Example 8.27. Define smooth vector fields X; $Y \in \mathcal { X } \left( \mathbb { R } ^ { 3 } \right)$ by \[ X = x \frac {\partial}{\partial x} + \frac {\partial}{\partial y} + x (y + 1) \frac {\partial}{\partial z}, \] \[ Y = \frac {\partial}{\partial x} + y \frac {\partial}{\partial z}. \] Then (8.9) yields \[ \begin{array}{l} [ X, Y ] = X (1) \frac {\partial}{\partial x} + X (y) \frac {\partial}{\partial z} - Y (x) \frac {\partial}{\partial x} - Y (1) \frac {\partial}{\partial y} - Y \big (x (y + 1) \big) \frac {\partial}{\partial z} \\ \qquad = 0 \frac {\partial}{\partial x} + 1 \frac {\partial}{\partial z} - 1 \frac {\partial}{\partial x} - 0 \frac {\partial}{\partial y} - (y + 1) \frac {\partial}{\partial z} \\ \qquad = - \frac {\partial}{\partial x} - y \frac {\partial}{\partial z}. \end{array} \]

Proposition 8.28

FC08-C08-U039 · Ch. 8, § Lie Brackets; source L5303 · not formalized

Proposition 8.28 (Properties of the Lie Bracket). The Lie bracket satisfies the following identities for all $X , Y , Z \in { \mathfrak { X } } ( M )$ : (a) BILINEARITY: $F o r a , b \in$ R, \[ [ a X + b Y, Z ] = a [ X, Z ] + b [ Y, Z ], \] \[ [ Z, a X + b Y ] = a [ Z, X ] + b [ Z, Y ]. \] (b) ANTISYMMETRY: \[ [ X, Y ] = - [ Y, X ]. \] (c) JACOBI IDENTITY: \[ [ X, [ Y, Z ] ] + [ Y, [ Z, X ] ] + [ Z, [ X, Y ] ] = 0. \] (d) For $f , g \in C ^ { \infty } ( M )$ /, \[ [ f X, g Y ] = f g [ X, Y ] + (f X g) Y - (g Y f) X.\tag{8.11} \]

Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib contains all four standard-tangent bracket laws—bilinearity, antisymmetry, Jacobi, and the smooth-function product rules—and /tmp/fc08-c08-witness.lean compiles Lee’s complete identities. They are deliberately not promoted because the fields inhabit unbridged standard TangentSpace, whereas Lee’s source tangent vectors are point derivations. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Proposition 8.30

FC08-C08-U040 · Ch. 8, § Lie Brackets; source L5345 · not formalized

Proposition 8.30 (Naturality of the Lie Bracket). Let $F \colon M \to N$ be a smooth map between manifolds with or without boundary, and let $X _ { 1 } , X _ { 2 } \in { \mathfrak { X } } ( M )$ and $Y _ { 1 } , Y _ { 2 } \in \mathfrak { X } ( N )$ be vector fields such that $X _ { i }$ is F -related to $Y _ { i } f o r i = 1 , 2$ . Then $[ X _ { 1 } , X _ { 2 } ]$ is F -related are not.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib proves naturality of mlieBracket for its mpullback under suitable derivative hypotheses, but Lee states naturality using the more general F-related/pushforward language. No checked whole-row interface matches that formulation, and the underlying standard-tangent fields remain unbridged from Lee’s derivation model. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Corollary 8.31

FC08-C08-U041 · Ch. 8, § Lie Brackets; source L5371 · not formalized

(Pushforwards of Lie Brackets). Suppose $F \colon M \to N$ is a diffeomorphism and $X_{1}, X_{2} \in \mathfrak{X}(M)$. Then $F_{*}[X_{1},X_{2}] = [F_{*}X_{1}, F_{*}X_{2}]$.

Corollary 8.32

FC08-C08-U042 · Ch. 8, § Lie Brackets; source L5377 · not formalized

Corollary 8.32 (Brackets of Vector Fields Tangent to Submanifolds). Let M be a smooth manifold and let S be an immersed submanifold with or without boundary in M . If $Y _ { 1 }$ and $Y _ { 2 }$ are smooth vector fields on M that are tangent to S, then $[ Y _ { 1 } , Y _ { 2 } ]$ is also tangent to S .

Not formalized. none; no complete checked declaration under strict bundle semantics — This bracket-tangency theorem needs the absent general submanifold layer from C05, in addition to the vector-field tangent-model bridge. No complete checked owner exists. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Definition/convention — left-invariant

FC08-C08-U043 · Ch. 8, § The Lie Algebra of a Lie Group; source L5383 · after FC08-C07-U031 · not formalized

Group One of the most important applications of Lie brackets occurs in the context of Lie groups. Suppose G is a Lie group. Recall that G acts smoothly and transitively on itself by left translation: $L _ { g } ( h ) = g h$ . (See Example 7.22(c).) A vector field X on G is said to be left-invariant if it is invariant under all left translations, in the sense that it is $L _ { g } \mathrm { - r e l a t e d }$ to itself for every $g \in G$ . More explicitly, this means \[ d (L _ {g}) _ {g ^ {\prime}} (X _ {g ^ {\prime}}) = X _ {g g ^ {\prime}}, \quad \mathrm{forall} g, g ^ {\prime} \in G.\tag{8.12} \] Since $L _ { g }$ is a diffeomorphism, this can be abbreviated by writing $( L _ { g } ) _ { * } X = X$

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has two adjacent but deliberately separate models: GroupLieAlgebra.mulInvariantVectorField for standard tangent fields and LeftInvariantDerivation for global derivations. The latter file explicitly says the canonical identification with left-invariant vector fields/tangent space in finite-dimensional C∞ real manifolds is not formalized. Hence Lee’s left-invariant-vector-field definition and closure-under-bracket theorem cannot be credited through either unbridged model. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Proposition 8.33

FC08-C08-U044 · Ch. 8, § The Lie Algebra of a Lie Group; source L5393 · not formalized

Proposition 8.33. Let G be a Lie group, and suppose X and Y are smooth leftinvariant vector fields on G. Then ŒX; Y is also left-invariant.

Definition/convention — bracket

FC08-C08-U045 · Ch. 8, § The Lie Algebra of a Lie Group; source L5403 · in Mathlib

A Lie algebra (over R) is a real vector space g endowed with a map called the bracket from ${ \mathfrak { g } } \times { \mathfrak { g } }$ to g, usually denoted by $( X , Y ) \mapsto [ X , Y ]$ , that satisfies the following properties for all X; Y; $Z \in { \mathfrak { g } }$ (i) BILINEARITY: For a; $b \in \mathbb { R }$ \[ [ a X + b Y, Z ] = a [ X, Z ] + b [ Y, Z ], \] \[ [ Z, a X + b Y ] = a [ Z, X ] + b [ Z, Y ]. \] (ii) ANTISYMMETRY: \[ [ X, Y ] = - [ Y, X ]. \] (iii) JACOBI IDENTITY: \[ [ X, [ Y, Z ] ] + [ Y, [ Z, X ] ] + [ Z, [ X, Y ] ] = 0. \]

Formalized. Mathlib/Algebra/Lie/Basic.lean::LieRing, LieAlgebra, lie_skew, leibniz_lie — LieAlgebra ℝ 𝔤 is a real vector space with a bilinear Lie bracket; LieRing supplies alternation/antisymmetry and the Jacobi identity (in the equivalent Leibniz form). This is exactly Lee’s real Lie-algebra structure.

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

Definition/convention — Lie algebras

FC08-C08-U046 · Ch. 8, § The Lie Algebra of a Lie Group; source L5427 · not formalized

Notice that the Jacobi identity is a substitute for associativity, which does not hold in general for brackets in a Lie algebra. It is useful in some circumstances to define Lie algebras over C or other fields, but we do not have any reason to consider such Lie algebras; thus all of our Lie algebras are assumed without further comment to be real.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib’s LieAlgebra R L is intentionally generic over the scalar ring/field; specializing to ℝ supports U045 but does not formalize Lee’s source-level convention that all subsequent unqualified Lie algebras are real. No separate interface owns this convention row. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Definition/convention — Lie subalgebra of g

FC08-C08-U047 · Ch. 8, § The Lie Algebra of a Lie Group; source L5429 · in Mathlib

If $\mathfrak { g }$ is a Lie algebra, a linear subspace ${ \mathfrak { h } } \subseteq { \mathfrak { g } }$ is called a Lie subalgebra of g if it is closed under brackets. In this case h is itself a Lie algebra with the restrictio {i}) = X ^ {i}.

Formalized. Mathlib/Algebra/Lie/Subalgebra.lean::LieSubalgebra — LieSubalgebra ℝ 𝔤 is a linear subspace closed under the Lie bracket and inherits the Lie-algebra structure, exactly Lee’s definition.

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

Definition/convention — Lie algebra homomorphism

FC08-C08-U048 · Ch. 8, § The Lie Algebra of a Lie Group; source L5431 · in Mathlib

If g and h are Lie algebras, a linear map $A \colon { \mathfrak { g } } { \mathfrak { h } }$ is called a Lie algebra homomorphism if it preserves brackets: $A [ X , Y ] = [ A X , A Y ]$ . An invertible Lie algebra homomorphism is called a Lie algebra isomorphism. If there exists a Lie algebra isomorphism from g to h, we say that they are isomorph over R.

Formalized. Mathlib/Algebra/Lie/Basic.lean::LieHom, LieHom.map_lie, LieEquiv — LieHom ℝ 𝔤 𝔥 is an ℝ-linear bracket-preserving map, and LieEquiv ℝ 𝔤 𝔥 is the invertible version. These are exactly Lee’s Lie-algebra homomorphism and isomorphism.

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

Example 8.36

FC08-C08-U049 · Ch. 8, § The Lie Algebra of a Lie Group; source L5437 · after FC08-C08-U039 · not formalized

(Lie Algebras). (a) The space $\mathfrak{X}(M)$ of smooth vector fields on a smooth manifold $M$ is a Lie algebra under the Lie bracket. (b) For a Lie group $G$, the smooth left-invariant vector fields form a Lie subalgebra of $\mathfrak{X}(G)$, hence a Lie algebra. (c) The vector space $M(n,\mathbb{R})$ of real $n \times n$ matrices is an $n^{2}$-dimensional Lie algebra under the commutator bracket $[A,B] = AB - BA$; with this bracket it is written $\mathfrak{gl}(n,\mathbb{R})$. (d) Similarly $\mathfrak{gl}(n,\mathbb{C})$ is the $2n^{2}$-dimensional real Lie algebra $M(n,\mathbb{C})$ with the commutator bracket. (e) For a vector space $V$, the linear maps $V \to V$ form a Lie algebra $\mathfrak{gl}(V)$ under $[A,B] = A \circ B - B \circ A$; identifying $n \times n$ matrices with linear maps of $\mathbb{R}^{n}$ gives $\mathfrak{gl}(\mathbb{R}^{n}) = \mathfrak{gl}(n,\mathbb{R})$. (f) Any vector space becomes an abelian Lie algebra if all brackets are defined to be zero.

Not formalized. none; no complete checked declaration under strict bundle semantics — Most algebraic ingredients of this six-part example exist (commutator Lie algebras, zero-bracket/abelian structures), but the row also asserts that smooth vector fields and left-invariant vector fields form the relevant Lie algebras. Those parts depend on the unformalized vector-field/derivation and invariant-field identifications, so the whole example bundle is not owned. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Definition/convention — abelian Lie algebra

FC08-C08-U050 · Ch. 8, § The Lie Algebra of a Lie Group; source L5464 · in Mathlib

Any vector space V becomes a Lie algebra if we define all brackets to be zero. Such a Lie algebra is said to be abelian. (The name reflects the fact that brackets in most Lie algebras, as in the preceding examples, are defined as commutators in terms of underlying associative products, so all brackets are zero precisely when the underlying product is commutative; it also reflects the connection between abelian Lie algebras and abelian Lie groups, which you will explore in Problems 8-25 and 20-7.)

Formalized. Mathlib/Algebra/Lie/Abelian.lean::IsLieAbelian, LieModule.trivial_lie_zero — IsLieAbelian 𝔤 means the self Lie action is trivial, equivalently every bracket is zero; this is exactly Lee’s abelian Lie-algebra condition.

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

Definition/convention — Lie algebra of G

FC08-C08-U051 · Ch. 8, § The Lie Algebra of a Lie Group; source L5466 · not formalized

Lie algebras and abelian Lie groups, which you will explore in Problems 8-25 and 20-7.) Example (b) is the most important one. The Lie algebra of all smooth leftinvariant vector fields on a Lie group G is called the Lie algebra of G , and is denoted by Lie.G/. (We will see below that the assumption of smoothness is redundant; see Corollary 8.38.) The fundamental fact is that Lie.G/ is finite-dimensional, and in fact has the same dimension as G itself, as the following theorem shows. T

Not formalized. none; no complete checked declaration under strict bundle semantics — GroupLieAlgebra I G is defined at P as the standard tangent space at 1 with bracket induced by mulInvariantVectorField; LeftInvariantDerivation gives a second derivation model. However there is no checked equivalence between either Mathlib model and Lee’s Lie algebra defined as smooth left-invariant vector fields, no evaluation linear equivalence, and no named parallelizability/frame theorem. The source row therefore remains unmatched despite substantial adjacent infrastructure. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Theorem 8.37

FC08-C08-U052 · Ch. 8, § The Lie Algebra of a Lie Group; source L5468 · not formalized

Theorem 8.37. Let G be a Lie group. The evaluation map ” Lie.G/ T G, given by “.X / Xe, is a vector space isomorphism. Thus, Lie.G/ is finite-dimensional, with dimension equal to dim $G .$

Convention/notation — source terminology/construction

FC08-C08-U053 · Ch. 8, § The Lie Algebra of a Lie Group; source L5496 · not formalized

Given any vector $v \in T_{e}G$, $v^{L}$ denotes the smooth left-invariant vector field defined by (8.13).

Corollary 8.38

FC08-C08-U054 · Ch. 8, § The Lie Algebra of a Lie Group; source L5500 · not formalized

Corollary 8.38. Every left-invariant rough vector field on a Lie group is smooth.

Definition/convention — left-invariant frame

FC08-C08-U055 · Ch. 8, § The Lie Algebra of a Lie Group; source L5504 · not formalized

The existence of global left-invariant vector fields also yields the following important property of Lie groups. Recall that a smooth manifold is said to be parallelizable if it admits a smooth global frame. If G is a Lie group, a local or global frame consisting of left-invariant vector fields is called a left-invariant 0 (Computing the Pushforward of a Vector Field).

Corollary 8.39

FC08-C08-U056 · Ch. 8, § The Lie Algebra of a Lie Group; source L5506 · not formalized

Corollary 8.39. Every Lie group admits a left-invariant smooth global frame, and therefore every Lie group is parallelizable.

Example 8.40

FC08-C08-U057 · Ch. 8, § The Lie Algebra of a Lie Group; source L5510 · after FC08-C08-U007 · not formalized

Example 8.40. Let us determine the Lie algebras of some familiar Lie groups. (a) EUCLIDEAN SPACE $\mathbb { R } ^ { n }$ : If we consider $\mathbb { R } ^ { n }$ as a Lie group under addition, left translation by an element $b \in \mathbb { R } ^ { n }$ is given by the affine map $L _ { b } ( x ) = b + x$ whose differential $d ( L _ { b } )$ is represented by the identity matrix in standard coordinates. Thus a vector field $\bar { X } ^ { i } \partial / \partial x ^ { i }$ is left-invariant if and only if its coefficients $X ^ { i }$ are constants. Because the Lie bracket of two constant-coefficient vector fields is zero by (8.8), the Lie algebra of $\mathbb { R } ^ { n }$ is abelian, and is isomorphic to $\mathbb { R } ^ { n }$ itself with the trivial bracket. In brief, Lie $( \mathbb { R } ^ { n } ) \cong \mathbb { R } ^ { n }$ (b) THE CIRCLE GROUP $\mathbb { S } ^ { 1 }$ : In terms of appropriate angle coordinates, each left translation has a local coordinate representation of the form $\theta \mapsto \theta + c$ . Since the differential of this map is the $1 \times 1$ identity matrix, it follows that the vector field $d / d \theta$ defined in Example 8.4 is left-invariant, and is therefore a basis for the Lie algebra of $\mathbb { S } ^ { 1 }$ This Lie algebra is 1-dimensional and abelian, and therefore $\operatorname { L i e } ( \mathbb { S } ^ { 1 } ) \cong \mathbb { R }$ (c) THE n-TORUS $\mathbb { T } ^ { n } = \mathbb { S } ^ { 1 } \times \cdots \times \mathbb { S } ^ { 1 }$ : An analysis similar to the one above shows that $\left( \partial / \partial \theta ^ { 1 } , \ldots , \partial / \partial \theta ^ { n } \right)$ is a basis for $\operatorname { L i e } ( \mathbb { T } ^ { n } )$ /, where $\partial / \partial \theta ^ { i }$ is the angle coordinate vector field on the $i$th factor.

Not formalized. none; no complete checked declaration under strict bundle semantics — No checked declaration packages Lee’s three explicit computations of the Lie algebras of Euclidean space, the circle, and the torus with the stated invariant bases and abelian identifications. The general group-Lie-algebra infrastructure does not own this whole example. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Proposition 8.41

FC08-C08-U058 · Ch. 8, § The Lie Algebra of a Lie Group; source L5526 · not formalized

(Lie Algebra of the General Linear Group). The composition of the natural maps \[ \operatorname{Lie}(\mathrm{GL}(n,\mathbb{R})) \to T_{I_{n}}\mathrm{GL}(n,\mathbb{R}) \to \mathfrak{gl}(n,\mathbb{R}) \tag{8.14} \] is a Lie algebra isomorphism between $\operatorname{Lie}(\mathrm{GL}(n,\mathbb{R}))$ and the matrix algebra $\mathfrak{gl}(n,\mathbb{R})$.

Not formalized. none; no complete checked declaration under strict bundle semantics — Targeted searches at P and H found no checked Lie-algebra isomorphism Lie(GL(n,ℝ)) ≃ gl(n,ℝ) or its basis-free GL(V) version. GroupLieAlgebra is generic tangent-at-identity infrastructure only; no general-linear specialization closes the row. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Corollary 8.42

FC08-C08-U059 · Ch. 8, § The Lie Algebra of a Lie Group; source L5580 · not formalized

Corollary 8.42. If V is any finite-dimensional real vector space, the composition of the canonical isomorphisms in (8.16) yields a Lie algebra isomorphism between Lie GL.V / and gl.V /. E

Theorem 8.44

FC08-C08-U060 · Ch. 8, § Induced Lie Algebra Homomorphisms; source L5588 · not formalized

Theorem 8.44 (Induced Lie Algebra Homomorphisms). Let G and H be Lie groups, and let g and h be their Lie algebras. Suppose $F \colon G \to H$ is a Lie group homomorphism. For every $X \in { \mathfrak { g } }$ , there is a unique vector field in h that is F -related to X. With this vector field denoted by $F _ { * } X$ , the map $F _ { * } \colon { \mathfrak { g } } \to { \mathfrak { h } }$ so defined is a Lie algebra homomorphism.

Not formalized. none; no complete checked declaration under strict bundle semantics — The checked GroupLieAlgebra file defines the object-level Lie algebra but has no map on smooth group homomorphisms, no GroupLieAlgebra-valued LieHom, and no Lie functor. Current H is unchanged on this boundary; indexed external search likewise describes the Lie functor as future work. Thus the induced-homomorphism/functoriality rows have no owner. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Definition/convention — induced Lie algebra homomorphism

FC08-C08-U061 · Ch. 8, § Induced Lie Algebra Homomorphisms; source L5615 · not formalized

The map $F_{*} \colon \mathfrak{g} \to \mathfrak{h}$ given by the theorem is called the induced Lie algebra homomorphism. In particular, for any left-invariant vector field $X \in \mathfrak{g}$, $F_{*}X$ is a well-defined smooth vector field on $H$, even when $F$ is not a diffeomorphism.

Proposition 8.45

FC08-C08-U062 · Ch. 8, § Induced Lie Algebra Homomorphisms; source L5617 · not formalized

Proposition 8.45 (Properties of Induced Homomorphisms). (a) The homomorphism $( \operatorname { I d } _ { G } ) _ { * } \colon \operatorname { L i e } ( G ) \to \operatorname { L i e } ( G )$ induced by the identity map of G is the identity of Lie.G/. (b) If $F _ { 1 } \colon G \to H$ and $F _ { 2 } \colon H \to K$ are Lie group homomorphisms, then \[ (F _ {2} \circ F _ {1}) _ {*} = (F _ {2}) _ {*} \circ (F _ {1}) _ {*} \colon \operatorname{Lie} (G) \to \operatorname{Lie} (K). \] (c) Isomorphic Lie groups have isomorphic Lie algebras. Proof. Both of the relations $d ( \mathrm { I d } _ { G } ) _ { e } = \mathrm { I d } _ { T _ { e } G }$ and $d ( F _ { 2 } \circ F _ { 1 } ) _ { e } = d ( F _ { 2 } ) _ { e } \circ d ( F _ { 1 } ) _ { e }$

Definition/convention — covariant functor

FC08-C08-U063 · Ch. 8, § Induced Lie Algebra Homomorphisms; source L5631 · after FC08-C08-U062 · not formalized

Let $\mathsf{Lie}$ be the category whose objects are Lie groups and whose morphisms are Lie group homomorphisms, and $\mathsf{lie}$ the category of finite-dimensional Lie algebras and Lie algebra homomorphisms. Proposition 8.45 says that the assignments $G \mapsto \operatorname{Lie}(G)$, $F \mapsto F_{*}$ define a covariant functor from $\mathsf{Lie}$ to $\mathsf{lie}$.

Theorem 8.46

FC08-C08-U064 · Ch. 8, § The Lie Algebra of a Lie Subgroup; source L5637 · not formalized

Theorem 8.46 (The Lie Algebra of a Lie Subgroup). Suppose $H \subseteq G$ is a Lie subgroup, and $\iota \colon H \hookrightarrow G$ is the inclusion map. There is a Lie subalgebra ${ \mathfrak { h } } \subseteq$ Lie.G/ that is canonically isomorphic to Lie.H /, characterized by either of the following descriptions: \[ \begin{array}{l} \mathfrak {h} = \iota_ {*} \big (\operatorname{Lie} (H) \big) \\ \qquad = \big \{X \in \operatorname{Lie} (G): X _ {e} \in T _ {e} H \big \}. \end{array}\tag{8.17} \]

Not formalized. none; no complete checked declaration under strict bundle semantics — These rows require a smooth Lie-subgroup/submanifold layer and concrete O(n)/GL(n,ℂ) group-Lie-algebra identifications. P/H have no LieSubgroup interface (consistent with C05’s absent submanifold abstraction), and no matching concrete group-Lie-algebra isomorphisms were found. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Example 8.47

FC08-C08-U065 · Ch. 8, § The Lie Algebra of a Lie Subgroup; source L5649 · after FC08-C07-U039, FC08-C08-U064 · not formalized

it is equal to the level set $\Phi ^ { - 1 } ( I _ { n } )$ , where $\phi \colon \mathbf { G L } ( n , \mathbb { R } ) \to \mathbf { M } ( n , \mathbb { R } )$ is the map $\varPhi ( A ) = \bar { A ^ { T } } A$ . By the result of Exercise 5.40, $T _ { I _ { n } } \mathrm { O } ( n )$ is equal to the kernel of $d \Phi _ { I _ { n } } \colon T _ { I _ { n } } \mathrm { G L } ( n , \mathbb { R } ) \to T _ { I _ { n } } \mathrm { M } ( n , \mathbb { R } )$ By the computation in Example 7.27, this differential is d $\Phi _ { I _ { n } } ( B ) = B ^ { T } + B$ , so \[ \begin{array}{c} T _ {I _ {n}} \operatorname{O} (n) = \big \{B \in \mathfrak {g l} (n, \mathbb {R}): B ^ {T} + B = 0 \big \} \\ = \{\text {skew - symmetric n\times n matrices} \}. \end{array} \] We denote this subspace of gl.n; R/ by o.n/. Theorem 8.46 then implies that o.n/ is a Lie subalgebra of ${ \mathfrak { g l } } ( n , \mathbb { R } )$ that is canonically isomorphic to $\operatorname { L i e } \bigl ( \operatorname { O } ( n ) \bigr )$ . Notice that we did not even have to verify directly that o.n/ is a subalgebra. We showed above that the Lie algebra of GL $( n , \mathbb { R } )$ is naturally isomorphic to the matrix algebra ${ \mathfrak { g l } } ( n , \mathbb { R } )$ . We can now prove a similar result for $\mathrm { G L } ( n , \mathbb { C } )$

Proposition 8.48

FC08-C08-U066 · Ch. 8, § The Lie Algebra of a Lie Subgroup; source L5665 · not formalized

Proposition 8.48 (The Lie Algebra of $\mathbf { G L } ( \pmb { n } , \mathbb { C } ) )$ . The composition of the maps in (8.18) yields a Lie algebra isomorphism between Lie $\left( \operatorname { G L } ( n , \mathbb { C } ) \right)$ and the matrix algebra $\mathfrak{gl}(n,\mathbb{C})$.

Definition/convention — faithful

FC08-C08-U067 · Ch. 8, § The Lie Algebra of a Lie Subgroup; source L5695 · in Mathlib

Parallel to the notion of representations of Lie groups, there is also a notion of representations of Lie algebras. If g is a finite-dimensional Lie algebra, a (finitedimensional) representation of g is a Lie algebra homomorphism $\varphi \colon { \mathfrak { g } } \to { \mathfrak { g l } } ( V )$ for some finite-dimensional vector space V , where gl.V / denotes the Lie algebra of linear maps from V to itself. If ’ is injective, it is said to be faithful, in which case g is isomorphic to the Lie subalgebra $\varphi ( { \mathfrak { g } } ) \subseteq { \mathfrak { g l } } ( V ) \cong { \mathfrak { g l } } ( n , \mathbb { R } )$ There is a close connection between representations of Lie groups and representations of their Lie algebras. Suppose G is a Lie group and g is its Lie algebra. If $\rho \colon G \to \mathbf { G } \mathbf { L } ( V )$

Formalized. Mathlib/Algebra/Lie/Basic.lean::LieHom; Mathlib/Algebra/Lie/OfAssociative.lean::LieModule.toEnd, LieModule.IsFaithful — A representation is exactly a Lie homomorphism 𝔤 →ₗ⁅ℝ⁆ Module.End ℝ V; LieModule.toEnd is the associated endomorphism representation, and LieModule.IsFaithful is defined by injectivity of this map. Thus the representation/faithfulness interface matches Lee’s definition.

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

Theorem 8.49

FC08-C08-U068 · Ch. 8, § The Lie Algebra of a Lie Subgroup; source L5701 · not formalized

Theorem 8.49 (Ado’s Theorem). Every finite-dimensional real Lie algebra admits a faithful finite-dimensional representation. C

Not formalized. none; no complete checked declaration under strict bundle semantics — Targeted searches of P, current H, project source, and indexed Lean repositories found no completed Ado theorem. Mathlib has faithful Lie-module infrastructure but no theorem asserting existence of a faithful finite-dimensional representation for every finite-dimensional real Lie algebra. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Corollary 8.50

FC08-C08-U069 · Ch. 8, § The Lie Algebra of a Lie Subgroup; source L5703 · not formalized

Corollary 8.50. Every finite-dimensional real Lie algebra is isomorphic to a Lie subalgebra of some matrix algebra gl.n; R/ with the commutator bracket.

Not formalized. none; no complete checked declaration under strict bundle semantics — This is the matrix-subalgebra corollary of Ado’s theorem. Since U068 is absent and no independent checked embedding theorem into gl(n,ℝ) was found, the corollary is unmatched. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.