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

FC08 — Lee, Introduction to Smooth Manifolds.

This chapter contains 13 definitions, 2 theorems, 11 propositions, 5 lemmas, 2 corollaries, 6 examples, 3 constructions and 3 conventions.

Of the 45 statements checked against Lean, 10 are formalized somewhere and 35 are not.

Status	Statements	Share	What it means
not formalized	35	78%	A documented search found no Lean statement of it anywhere.
in Mathlib	10	22%	Mathlib states and proves it.
checked in total	45

Which versions of Lean and Mathlib were searched

Canonical source block: FC08 Lee, Chapter 14, FC08-C14-U001–FC08-C14-U045, exactly 45 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. Project search found exterior-algebra consumers/contraction lemmas but no source-row owner; no project-existing, package-import, or reference-port route survived strict whole-row checking.
C14 has 10 pinned mathlib rows and 35 dated unmatched rows. Positive rows are: U001, U002, U003, U005, U007, U012, U013, U014, U019, U021.
The algebraic alternating-map layer is strong. AlternatingMap directly represents scalar exterior forms; map_linearDependent and the defining repeated-input axiom give Lee’s equivalent alternating criteria. MultilinearMap.alternatization is the unnormalized signed permutation sum and AlternatingMap.coe_alternatization supplies the exact k! factor, so Lee’s normalized Alt and its projection property are short checked assemblies. /tmp/fc08-c14-witness.lean compiles U002/U003/U005 at exact P.
Elementary forms and top-degree determinant behavior also have direct checked realizations. Matrix.detRowAlternating composed with selected coordinate covectors gives Lee’s determinant elementary form (U007). AlternatingMap.eq_smul_basis_det plus Basis.det_comp gives the top-degree transformation law (U012). Both assemblies compile in the witness.
AlternatingMap.domCoprod is explicitly Mathlib’s exterior product and uses the signed shuffle formula. For scalar forms, composing with TensorProduct.lid and reindexing along finSumFinEquiv gives Lee’s determinant-convention wedge; MultilinearMap.domCoprod_alternization_eq verifies the factorial normalization. U013/U014 are therefore promoted. Lee’s alternate convention U019 is the corresponding normalized alternation of MultilinearMap.domCoprod, also compiled in the witness.
AlternatingMap.curryLeft is exactly interior multiplication by fixing the first argument, so U021 is promoted. curryLeft_same proves U022(a), but no checked Leibniz rule against the scalar specialized wedge was found; strict whole-row semantics keep U022 unmatched.
A deliberate representation boundary blocks several tempting algebraic promotions. Mathlib has ExteriorAlgebra, Module.Basis.exteriorPower, exteriorPower.finrank_eq, and grading machinery, but targeted P/H searches found no checked finite-dimensional equivalence identifying the abstract exterior powers of V* with the scalar-valued AlternatingMap realization used by Lee. U011/U018 and dependent coordinate/algebra laws are not inferred across that missing bridge.
The manifold half remains absent. P and H have Topology/VectorBundle/ContinuousAlternatingMap.lean, which constructs a topological bundle of continuous alternating maps between vector-bundle fibers, but no smooth ContMDiff alternating-map bundle or manifold DifferentialForm section API. Moreover, Lee’s FC08 tangent/cotangent spaces remain the point-derivation model from C03/C11 with no checked bridge to Mathlib’s standard TangentSpace. Thus U023–U031 are unmatched.
Exact P/H searches also find no manifold exterior-derivative layer: no smooth differential-form d, invariant exterior-derivative formula, Cartan magic formula, or Lie-derivative/exterior-derivative package. U032–U045 remain unmatched rather than being reconstructed from vector-space calculus and Lie-bracket ingredients.
Current-H file search shows the same relevant manifold surface: Topology/VectorBundle/ContinuousAlternatingMap.lean but no geometry/manifold differential-form implementation. Targeted external indexed search did not surface a compatible Lean owner; one current categorical-differential-geometry project describes de Rham cohomology only as a long-term goal rather than a replacement implementation.
N=2026-09-07 marks dated unmatched decisions. Strict whole-row semantics apply uniformly.

Definition/convention — exterior forms

FC08-C14-U001 · Ch. 14, § The Algebra of Alternating Tensors; source L10456 · in Mathlib

Let V be a finite-dimensional (real) vector space. Recall that a covariant k-tensor on V is said to be alternating if its value changes sign whenever two arguments are interchanged, or equivalently if any permutation of the arguments causes its value to be multiplied by the sign of the permutation (see Exercise 12.17). Alternating covariant k-tensors are also called exterior forms, multicovectors, or k-covectors. The vector space of all k-covectors on V is denoted by $\Lambda ^ { k } ( V ^ { * } )$ . As we noted in Chapter 12, all 0-tensors and 1-tensors are alternating.

Formalized. Mathlib/LinearAlgebra/Alternating/Basic.lean::AlternatingMap, AlternatingMap.map_perm, AlternatingMap.constLinearEquivOfIsEmpty, AlternatingMap.ofSubsingleton — AlternatingMap ℝ V ℝ (Fin k) is exactly a real-valued alternating k-linear form. map_perm gives the sign rule under permutations; constLinearEquivOfIsEmpty and ofSubsingleton identify degrees 0 and 1 with scalars and ordinary linear forms, matching the final clause of Lee’s definition.

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

Lemma 14.1

FC08-C14-U002 · Ch. 14, § The Algebra of Alternating Tensors; source L10460 · in Mathlib

Lemma 14.1. Let ˛ be a covariant k-tensor on a finite-dimensional vector space V . The following are equivalent: (a) ˛ is alternating. (b) $\alpha ( v _ { 1 } , \ldots , v _ { k } ) = 0$ v _ { k } )$ is linearly dependent. (c) ˛ gives the value zero whenever two of its arguments are equal: \[ \alpha (v _ {1}, \ldots , w, \ldots , w, \ldots , v _ {k}) = 0. \] Proof. The implications $

Formalized. Mathlib/LinearAlgebra/Alternating/Basic.lean::AlternatingMap.map_linearDependent, AlternatingMap.map_eq_zero_of_eq — map_linearDependent proves that an alternating map vanishes on linearly dependent input, while map_eq_zero_of_eq is the repeated-argument condition built into AlternatingMap. Conversely, the repeated-argument condition directly constructs an AlternatingMap; /tmp/fc08-c14-witness.lean compiles both equivalences at P.

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

Construction/definition — symmetrization

FC08-C14-U003 · Ch. 14, § The Algebra of Alternating Tensors; source L10492 · in Mathlib

Chapter 12 defined a projection $\operatorname{Sym} \colon T^{k}(V^{*}) \to \Sigma^{k}(V^{*})$ called symmetrization. The analogous projection $\operatorname{Alt} \colon T^{k}(V^{*}) \to \Lambda^{k}(V^{*})$, called alternation, is \[ \operatorname{Alt}\alpha = \frac{1}{k!}\sum_{\sigma \in S_{k}} (\operatorname{sgn}\sigma)\,({}^{\sigma}\alpha), \] where $S_{k}$ is the symmetric group on $k$ elements; explicitly, \[ (\operatorname{Alt}\alpha)(v_{1},\dots,v_{k}) = \frac{1}{k!}\sum_{\sigma \in S_{k}} (\operatorname{sgn}\sigma)\,\alpha(v_{\sigma(1)},\dots,v_{\sigma(k)}). \]

Formalized. Mathlib/LinearAlgebra/Alternating/Basic.lean::MultilinearMap.alternatization, MultilinearMap.alternatization_apply, AlternatingMap.coe_alternatization — alternatization is the signed sum over all permutations. Scaling by (k!)⁻¹ over ℝ gives exactly Lee’s normalized Alt; coe_alternatization states that alternatizing an already alternating form multiplies it by k!. The normalized wrapper compiles in /tmp/fc08-c14-witness.lean.

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

Example 14.2

FC08-C14-U004 · Ch. 14, § The Algebra of Alternating Tensors; source L10504 · after FC08-C12-U024 · not formalized

Example 14.2. If ˛ is any 1-tensor, then Alt $\alpha = \alpha$ . If $\beta$ is a 2-tensor, then \[ (\operatorname{Alt} \beta) (v, w) = \frac {1}{2} (\beta (v, w) - \beta (w, v)). \] For a 3-tensor $\gamma .$ , \[ \begin{array}{c} (\text {Alt} \gamma) (v, w, x) = \frac {1}{6} \big (\gamma (v, w, x) + \gamma (w, x, v) + \gamma (x, v, w) \\ - \gamma (w, v, x) - \gamma (v, x, w) - \gamma (x, w, v) \big). \end{array} \] The next proposition is the analogue for alternating tensors , and Example 13.18 shows that the induced metric is $d t ^ { 2 } + ( P t + K ) ^ { 2 } d \theta ^ { 2 }$ .

Not formalized. none; no complete checked declaration under strict bundle semantics — The normalized alternation operator is available by the U003 assembly, but no checked declaration packages Lee’s complete degree-1/2/3 worked formulas as one source example. Deriving the explicit six-term degree-3 expansion is example reconstruction rather than a direct route. Strict whole-row semantics reject proper subsets, missing representation bridges, and reconstruction of substantive source theorems from generic ingredients.

Proposition 14.3

FC08-C14-U005 · Ch. 14, § The Algebra of Alternating Tensors; source L10518 · in Mathlib

Proposition 14.3 (Properties of Alternation). Let ˛ be a covariant tensor on a finite-dimensional vector space. (a) Alt ˛ is alternating. (b) Alt $\alpha = \alpha$ if and only if ˛ is alternating.

Formalized. Mathlib/LinearAlgebra/Alternating/Basic.lean::MultilinearMap.alternatization, AlternatingMap.coe_alternatization — Because alternatization lands in AlternatingMap, normalized Alt α is alternating. coe_alternatization and nonvanishing of k! over ℝ give Alt α = α for an alternating α; the converse is immediate because Alt α itself is alternating. /tmp/fc08-c14-witness.lean compiles the iff.

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

Convention/notation — multi-index of length k

FC08-C14-U006 · Ch. 14, § Elementary Alternating Tensors; source L10528 · not formalized

For computations with alternating tensors, the following notation is exceedingly useful. Given a positive integer k, an ordered k-tuple $I = ( i _ { 1 } , \dots , i _ { k } )$ of positive integers is called a multi-index of length k. If I is such a multi-index and $\sigma \in S _ { k }$ is a permutation of $\{ 1 , \ldots , k \}$ , we write $I _ { \sigma }$ for the following multi-index: \[ I _ {\sigma} = \left(i _ {\sigma (1)}, \dots , i _ {\sigma (k)}\right). \]

Not formalized. none; no complete checked declaration under strict bundle semantics — This row is source-specific multi-index/Kronecker notation or a worked coordinate example. Mathlib has the underlying finite-index, determinant, and basis machinery, but no exact declaration owning the complete notation/example bundle. Strict whole-row semantics reject proper subsets, missing representation bridges, and reconstruction of substantive source theorems from generic ingredients.

Definition/convention — source terminology/construction

FC08-C14-U007 · Ch. 14, § Elementary Alternating Tensors; source L10542 · in Mathlib

In other words, if v denotes the $n \times k$ matrix whose columns are the components of the vectors $v _ { 1 } , \ldots , v _ { k }$ with respect to the basis $\left( E _ { i } \right)$ dual to $\left( \varepsilon ^ { i } \right)$ , then $\boldsymbol { \varepsilon } ^ { I } ( v _ { 1 } , \dots , v _ { k } )$ is the determinant of the $k \times k$ submatrix consisting of rows $i _ { 1 } , \ldots , i _ { k }$ of v. Because the determinant changes sign whenever two columns are interchanged, it is clear that $\varepsilon ^ { I }$ is an alternating k-tensor. We call $\varepsilon ^ { I }$ an elementary alternating tensor frac {}{t} () - ()) .

Formalized. Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean::Matrix.detRowAlternating; Mathlib/LinearAlgebra/Alternating/Basic.lean::AlternatingMap.compLinearMap — Matrix.detRowAlternating is determinant as an alternating map of rows. Composing it with the linear coordinate map v ↦ (ε^{i_j}(v))_j gives Lee’s elementary k-covector and its determinant-of-selected-coordinates formula. This exact construction compiles in /tmp/fc08-c14-witness.lean.

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

Example 14.5

FC08-C14-U008 · Ch. 14, § Elementary Alternating Tensors; source L10544 · not formalized

Example 14.5. In terms of the standard dual basis $\left( e ^ { 1 } , e ^ { 2 } , e ^ { 3 } \right)$ for $\left( \mathbb { R } ^ { 3 } \right) ^ { * }$ , we have \[ e ^ {1 3} (v, w) = v ^ {1} w ^ {3} - w ^ {1} v ^ {3}; \] \[ e ^ {1 2 3} (v, w, x) = \det (v, w, x). \] In order to streamline computations with the elementary k-covectors, it is useful to extend the Kronecker delta notation in the following way. If I and J are multiindices of length $k$ , we define \[ \delta_ {J} ^ {I} = \det \left( \begin{array}{c c c} \delta_ {j _ {1}} ^ {i _ {1}} & \ldots & \delta_ {j _ {k}} ^ {i _ {1}} \\ \vdots & \ddots & \vdots \\ \delta_ {j _ {1}} ^ {i _ {k}} & \ldots & \delta_ {j _ {k}} ^ {i _ {k}} \end{array} \right). \]

Lemma 14.7

FC08-C14-U009 · Ch. 14, § Elementary Alternating Tensors; source L10564 · not formalized

Lemma 14.7 (Properties of Elementary k-Covectors). Let $\left( E _ { i } \right)$ be a basis for V , let $\left( \varepsilon ^ { i } \right)$ be the dual basis for $V ^ { * }$ , and let $\varepsilon ^ { I }$ be as defined above. (a) If I has a repeated index, then $\varepsilon ^ { I } = 0$ (b) $I f J = I _ { \sigma }$ for some $\sigma \in S _ { k }$ , then $\varepsilon ^ { I } = ( \operatorname { s g n } \sigma ) \varepsilon ^ { J }$ (c) The result of evaluating $\varepsilon ^ { I }$ on a sequence of basis vectors is \[ \varepsilon^ {I} \left(E _ {j _ {1}}, \dots , E _ {j _ {k}}\right) = \delta_ {J} ^ {I}. \] Proof. If I has a repeated index, then for any vectors $v _ { 1 } , \ldots , v _ { k }$ , the determinant in (14.1) has two identical rows, so it vanishes.

Not formalized. none; no complete checked declaration under strict bundle semantics — The determinant and alternating-map APIs contain the ingredients for repeated selected indices, permutation signs, and evaluation on basis vectors, but no checked theorem packages Lee’s generalized-Kronecker multi-index statement. Reassembling all three clauses would be a substantive source-specific coordinate proof. Strict whole-row semantics reject proper subsets, missing representation bridges, and reconstruction of substantive source theorems from generic ingredients.

Definition/convention — increasing

FC08-C14-U010 · Ch. 14, § Elementary Alternating Tensors; source L10578 · not formalized

A multi-index $I = (i_{1},\dots,i_{k})$ is increasing if $i_{1} < \cdots < i_{k}$. A primed summation sign denotes a sum over increasing multi-indices only, so that, for example, \[ \sideset{}{'}\sum_{I} \alpha_{I}\varepsilon^{I} = \sum_{\{I \,:\, i_{1} < \cdots < i_{k}\}} \alpha_{I}\varepsilon^{I}. \]

Proposition 14.8

FC08-C14-U011 · Ch. 14, § Elementary Alternating Tensors; source L10584 · not formalized

Proposition 14.8 (A Basis for $\pmb { \Lambda } ^ { k } ( V ^ { \ast } ) )$ . Let V be an n-dimensional vector space. $H ^ { \prime } \left( \varepsilon ^ { i } \right)$ is any basis for $V ^ { * }$ , then for each positive integer $k \leq n$ , the collection of k-covectors \[ \mathcal {E} = \left\{\varepsilon^ {I}: I \text {is an increasing multi - index of length} k \right\} \] is a basis for $\Lambda ^ { k } ( V ^ { * } )$ . Therefore, \[ \dim \Lambda^ {k} (V ^ {*}) = \binom {n} {k} = \frac {n !}{k ! (n - k) !}. \] $I f k > n$ , then dim $\Lambda ^ { k } ( V ^ { * } ) = 0$ Proof. The fact that $\Lambda ^ { k } ( V ^ { * } )$ is the trivial vector space when $k > n$ follows immediately from Lemma 14.1(b), since every $k { \mathrm { - t u p l e } }$

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has Module.Basis.exteriorPower and exteriorPower.finrank_eq for the abstract exterior power, but no checked finite-dimensional equivalence identifies ⋀^k(V*) with Lee’s scalar-valued AlternatingMap realization. The missing representation bridge prevents using the abstract basis theorem for this source row. Strict whole-row semantics reject proper subsets, missing representation bridges, and reconstruction of substantive source theorems from generic ingredients.

Proposition 14.9

FC08-C14-U012 · Ch. 14, § Elementary Alternating Tensors; source L10626 · in Mathlib

Proposition 14.9. Suppose V is an n-dimensional vector space and $\omega \in \Lambda ^ { n } ( V ^ { * } )$ $I f T \colon V \to V$ is any linear map and $v _ { 1 } , \ldots , v _ { n }$ are arbitrary vectors in V , then \[ \omega (T v _ {1}, \dots , T v _ {n}) = (\det T) \omega (v _ {1}, \dots , v _ {n}).\tag{14.2} \]

Formalized. Mathlib/LinearAlgebra/Determinant.lean::AlternatingMap.eq_smul_basis_det, Module.Basis.det_comp — eq_smul_basis_det says every top-degree scalar alternating form is a scalar multiple of the determinant form for a basis, and Basis.det_comp gives composition with an endomorphism as multiplication by LinearMap.det. Together they prove Lee’s transformation formula; the assembly compiles in /tmp/fc08-c14-witness.lean.

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

Definition/convention — similar product operation for alternating tensors

FC08-C14-U013 · Ch. 14, § The Wedge Product; source L10652 · in Mathlib

In this section we define a similar product operation for alternating tensors. One way to define it would be to mimic what we did in the symmetric case and define the product of alternating tensors ! and to be $\mathbf { A l t } ( \omega \otimes \eta )$ . However, we will use a different definition that looks more complicated at first but turns out to be much better suited to compu Riemannian isometry.

Formalized. Mathlib/LinearAlgebra/Alternating/DomCoprod.lean::AlternatingMap.domCoprod — AlternatingMap.domCoprod is explicitly documented and defined as the exterior product of two alternating maps, using the signed shuffle sum. This is precisely the product operation Lee introduces before fixing notation in U014.

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

Definition/convention — their wedge product

FC08-C14-U014 · Ch. 14, § The Wedge Product; source L10654 · in Mathlib

We continue with the assumption that V is a finite-dimensional real vector space. Given $\omega \in \Lambda ^ { k } ( V ^ { * } )$ and $\eta \in \Lambda ^ { l } ( V ^ { * } )$ , we define their wedge product or exterior product to be the following $( k + l )$ -covector: \[ \omega \wedge \eta = \frac {(k + l) !}{k ! l !} \operatorname{Alt} (\omega \otimes \eta).\tag{14.3} \]

Formalized. Mathlib/LinearAlgebra/Alternating/DomCoprod.lean::AlternatingMap.domCoprod, MultilinearMap.domCoprod_alternization_eq; Mathlib/LinearAlgebra/TensorProduct/Basic.lean::TensorProduct.lid — For scalar-valued forms, compose domCoprod with the canonical ℝ ⊗[ℝ] ℝ ≃ₗ ℝ and reindex Fin k ⊕ Fin l ≃ Fin (k+l). domCoprod_alternization_eq gives the factorial relation showing this shuffle product equals Lee’s determinant convention ((k+l)!)/(k!l!) Alt(ω⊗η). The specialized wrapper compiles at P.

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

Lemma 14.10

FC08-C14-U015 · Ch. 14, § The Wedge Product; source L10662 · not formalized

Lemma 14.10. Let V be an n-dimensional vector space and let $\left( \varepsilon ^ { 1 } , \ldots , \varepsilon ^ { n } \right)$ be a basis for $V ^ { * }$ . For any multi-indices $I = ( i _ { 1 } , \dots , i _ { k } )$ and $J = ( j _ { 1 } , \ldots , j _ { l } )$ \[ \varepsilon^ {I} \wedge \varepsilon^ {J} = \varepsilon^ {I J},\tag{14.4} \] where $I J = ( i _ { 1 } , \dots , i _ { k } , j _ { 1 } , \dots , j _ { l } )$ is obtained by concatenating K, | v | _ {} = 1 }.

Not formalized. none; no complete checked declaration under strict bundle semantics — The determinant-convention wedge is available through U014, but no checked theorem states Lee’s elementary multi-index concatenation identity under the scalar AlternatingMap specialization. Proving it would reconstruct a coordinate theorem from determinant/shuffle ingredients. Strict whole-row semantics reject proper subsets, missing representation bridges, and reconstruction of substantive source theorems from generic ingredients.

Proposition 14.11

FC08-C14-U016 · Ch. 14, § The Wedge Product; source L10698 · not formalized

Proposition 14.11 (Properties of the Wedge Product). Suppose !, $\omega ^ { \prime } , \eta , \eta ^ { \prime }$ , and $\xi$ are multicovectors on a finite-dimensional vector space $V$ . (a) BILINEARITY: For $a , a ^ { \prime } \in \mathbb { R }$ \[ \begin{array}{l} (a \omega + a ^ {\prime} \omega^ {\prime}) \wedge \eta = a (\omega \wedge \eta) + a ^ {\prime} (\omega^ {\prime} \wedge \eta), \\ \eta \wedge (a \omega + a ^ {\prime} \omega^ {\prime}) = a (\eta \wedge \omega) + a ^ {\prime} (\eta \wedge \omega^ {\prime}). \end{array} \] (b) ASSOCIATIVITY: \[ \omega \wedge (\eta \wedge \xi) = (\omega \wedge \eta) \wedge \xi . \] (c) ANTICOMMUTATIVITY: For $\omega \in \Lambda ^ { k } ( V ^ { * } )$ and $\eta \in \Lambda ^ { l } ( V ^ { * } )$ , \[ \omega \wedge \eta = (- 1) ^ {k l} \eta \wedge \omega .\tag{14.6} \] (d) $H \left( \varepsilon ^ { i } \right)$ is any basis for $V ^ { * }$ and $I = ( i _ { 1 } , \dots , i _ { k } )$ is any multi-index, then \[ \varepsilon^ {i _ {1}} \wedge \dots \wedge \varepsilon^ {i _ {k}} = \varepsilon^ {I}.\tag{14.7} \] (e) For any covectors $\omega ^ { 1 } , \ldots , \omega ^ { k }$ and vectors $v _ { 1 } , \ldots , v _ { k }$ \[ \omega^ {1} \wedge \dots \wedge \omega^ {k} (v _ {1}, \dots , v _ {k}) = \det \left(\omega^ {j} (v _ {i})\right).\tag{14.8} \] Proof. Bilinearity follows immediately from the definition, because the tensor product is bilinear ball of radius ” around $p$ such that ${ \overline { { V } } } \subseteq U$ as above.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib’s AlternatingMap.domCoprod defines the wedge, but targeted P/H searches found no packaged scalar-valued associativity, graded-commutativity, elementary-wedge, and determinant-evaluation theorem bundle matching all five clauses. ExteriorAlgebra has algebra laws only after changing representation, and the needed representation bridge is absent. Strict whole-row semantics reject proper subsets, missing representation bridges, and reconstruction of substantive source theorems from generic ingredients.

Definition/convention — decomposable

FC08-C14-U017 · Ch. 14, § The Wedge Product; source L10748 · not formalized

A k-covector is said to be decomposable if it can be expressed in the form $\eta = \omega ^ { 1 } \wedge \cdots \wedge \omega ^ { k }$ , where $\omega ^ { 1 } , \ldots , \omega ^ { k }$ are covectors. It is important to be aware that not every k-covector is decomposable when $k > 1$ (see Problem 14-2); however, it follows from Propositions 14.8 and 14.11(d) that every k-covector can be written as a linear combination of decomposable ones.

Not formalized. none; no complete checked declaration under strict bundle semantics — No checked predicate/interface for decomposable scalar alternating forms was found. Abstract exterior-algebra generators and spanning theorems do not by themselves identify Lee’s AlternatingMap object with decomposable wedges. Strict whole-row semantics reject proper subsets, missing representation bridges, and reconstruction of substantive source theorems from generic ingredients.

Construction/definition — exterior algebra (

FC08-C14-U018 · Ch. 14, § The Wedge Product; source L10760 · after FC08-C14-U011, FC08-C14-U016 · not formalized

\[ It follows from Proposition 14.8 that dim $\Lambda ( V ^ { * } ) = 2 ^ { n }$ . Proposition 14.11 shows that the wedge product turns $\Lambda ( V ^ { * } )$ into an associative algebra, called the exterior algebra (or Grassmann algebra) of V . This algebra is not commutative, but it has a closely related property. An algebra A is said to be graded if it has a direct sum decomposition $\overset { \cdot } { A } = \overset { \cdot } { \oplus _ { k \in \mathbb { Z } } } \overset { \cdot } { A ^ { k } }$ such that the product satisfies $\left( A ^ { k } \right) \left( A ^ { l } \right) \subseteq A ^ { k + l }$ for each k and l. A graded algebra is anticommutative if the product satisfies $a b = ( - 1 ) ^ { k l } b a$ for $a \overset { \cdot } { \in } A ^ { k } , b \in A ^ { l }$ . Proposition 14.11(c) shows that $\Lambda ( V ^ { * } )$ is an anticommutative graded algebra (where we interpret $A ^ { k } = \Lambda ^ { k } ( V ^ { * } )$ for $0 \leq k \leq n$ and $A ^ { k } = \{ 0 \}$ otherwise). As we observed at the beginning of this section, one could also define the wedge product without the unwieldy coefficient of (14.3). Some authors choose this alternative definition of the wedge product. To avoid confusion, we denote it by : \]

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has a graded ExteriorAlgebra ℝ (Dual ℝ V) and exterior-power bases, but Lee’s row is explicitly the algebra on the previously defined scalar alternating tensors Λ^k(V*). No checked finite-dimensional algebra equivalence between these representations was found at P or H, so the abstract algebra cannot own the whole row. Strict whole-row semantics reject proper subsets, missing representation bridges, and reconstruction of substantive source theorems from generic ingredients.

Convention/notation — wedge product without the unwieldy coefficient of (14

FC08-C14-U019 · Ch. 14, § The Wedge Product; source L10762 · in Mathlib

As we observed at the beginning of this section, one could also define the wedge product without the unwieldy coefficient of (14.3). Some authors choose this alternative definition of the wedge product. To avoid confusion, we denote it by Z : ω ∧ η = Alt (ω ⊗ η).tag14.9

Formalized. Mathlib/LinearAlgebra/Multilinear/TensorProduct.lean::MultilinearMap.domCoprod; Mathlib/LinearAlgebra/Alternating/Basic.lean::MultilinearMap.alternatization; Mathlib/LinearAlgebra/TensorProduct/Basic.lean::TensorProduct.lid — Lee’s alternate convention is exactly normalized alternation of the multilinear tensor product. MultilinearMap.domCoprod forms the product, TensorProduct.lid multiplies scalar codomains, and (k+l)!⁻¹ • alternatization is the normalized Alt. /tmp/fc08-c14-witness.lean compiles this definition.

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

Definition/convention — source terminology/construction

FC08-C14-U020 · Ch. 14, § The Wedge Product; source L10782 · not formalized

Because of (14.8), we call definition (14.3) the determinant convention for the wedge product, and (14.9) the Alt convention. The choice of which definition to use is largely a matter of taste. Although the definition of the Alt convention is perhaps a bit more natural, the computational advantages of the determinant convention make it preferable for most applications, and we use it exclusively in this book. (But see Problem 14-3 for an argument in favor of the Alt convention.) The determinant convention is most common in introductory differential geometry texts, and is used, for example, in [Boo86, Cha06, dC92, LeeJeff09, Pet06, Spi99]. The Alt convention is used in [KN69] and is more common in complex differential geometry.

Not formalized. none; no complete checked declaration under strict bundle semantics — This is a source terminology/convention distinguishing two wedge normalizations. The underlying determinant and Alt conventions are separately formalized in U014/U019, but no additional checked object corresponds to Lee’s naming convention itself.

Definition/convention — interior multiplication by v

FC08-C14-U021 · Ch. 14, § Interior Multiplication; source L10786 · in Mathlib

There is an important operation that relates vectors with alternating tensors. Let V be a finite-dimensional vector space. For each $v \in V$ ^ { k - 1 } ( V ^ { * } )$ , called interior multiplication by v, as follows: \[ i _ {v} \omega (w _ {1}, \ldots , w _ {k - 1}) = \omega (v, w _ {1}, \ldots , w _ {k - 1}). \] In other words, $

Formalized. Mathlib/LinearAlgebra/Alternating/Curry.lean::AlternatingMap.curryLeft, AlternatingMap.curryLeft_apply_apply, AlternatingMap.curryLeftLinearMap — curryLeft sends an alternating (k+1)-form to the linear map v ↦ (w ↦ ω(v,w₁,…,w_k)), exactly Lee’s interior multiplication by v after fixing the first argument.

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

Lemma 14.13

FC08-C14-U022 · Ch. 14, § Interior Multiplication; source L10800 · not formalized

Lemma 14.13. Let V be a finite-dimensional vector space and $v \in V$ (a) $i _ { v } \circ i _ { v } = 0$ (b) $H \omega \in \Lambda ^ { k } ( V ^ { * } )$ and $\eta \in \Lambda ^ { l } ( V ^ { * } )$ \[ i _ {v} (\omega \wedge \eta) = (i _ {v} \omega) \wedge \eta + (- 1) ^ {k} \omega \wedge (i _ {v} \eta).\tag{14.11} \]

Not formalized. none; no complete checked declaration under strict bundle semantics — AlternatingMap.curryLeft_same directly proves i_v ∘ i_v = 0, but targeted P/H searches found no graded Leibniz rule for curryLeft against the specialized scalar domCoprod wedge. One of the two clauses is therefore missing. Strict whole-row semantics reject proper subsets, missing representation bridges, and reconstruction of substantive source theorems from generic ingredients.

Convention/notation — differential k-form

FC08-C14-U023 · Ch. 14, § Differential Forms on Manifolds; source L10852 · not formalized

A section of $\Lambda ^ { k } T ^ { * } M$ is called a differential k-form, or just a $k { \cdot } f o r m ^ { \cdot }$ ; this is a (continuous) tensor field whose value at each point is an alternating tensor. The integer $k$ is called the degree of the form. We denote the vector space of smooth k-forms by \[ \Omega^ {k} (M) = \Gamma \big (\Lambda^ {k} T ^ {*} M \big). \] The wedge product of a $k$-form and an $l$-form is a $(k+l)$-form.

Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib constructs a topological vector bundle of continuous alternating maps between fibers, but no smooth manifold differential-form bundle/section API was found. These rows also require Lee’s point-derivation tangent/cotangent model, whose bridge to standard TangentSpace remains absent from C03/C11. Hence form sections, pointwise wedge, pullback, and coordinate formulas are not complete checked rows. Strict whole-row semantics reject proper subsets, missing representation bridges, and reconstruction of substantive source theorems from generic ingredients.

Definition/convention — k-form

FC08-C14-U024 · Ch. 14, § Differential Forms on Manifolds; source L10858 · not formalized

The wedge product of two differential forms is defined pointwise: ( ω ∧ η ) _p = ω _p ∧ η _p . Thus, the wedge product of a k-form with an l -form is a ( k + l ) – form . If f is a 0-form and η is a k-form, we interpret the wedge product f ∧ η to mean the ordinary product f η . If we define \[ \Omega^{*}(M) = \bigoplus_{k=0}^{n} \Omega^{k}(M), \tag{14.14} \] then the wedge product turns $\Omega^{*}(M)$ into an associative, anticommutative graded algebra.

Example 14.15

FC08-C14-U025 · Ch. 14, § Differential Forms on Manifolds; source L10884 · not formalized

Example 14.15. A 0-form is just a continuous real-valued function, and a 1-form is a covector field. $\mathrm { O n } \mathbb { R } ^ { 3 }$ , some examples of smooth 2-forms are given by \[ \omega = (\sin x y) d y \wedge d z; \] \[ \eta = d x \wedge d y + d x \wedge d z + d y \wedge d z. \] Every 3-form on $\mathbb { R } ^ { 3 }$ is a continuous real-valued fun th manifold M is a smooth symmetric 2-tensor field whose value is nondegenerate at each point, with the same signature everywhere on M .

Construction/definition — source terminology/construction

FC08-C14-U026 · Ch. 14, § Differential Forms on Manifolds; source L10896 · not formalized

If $F \colon M \to N$ is a smooth map and $\omega$ is a differential form on N , the pullback $F ^ { * } \omega$ is a differential form on M; defined as for any covariant tensor field: \[ (F ^ {*} \omega) _ {p} (v _ {1}, \ldots , v _ {k}) = \omega_ {F (p)} \big (d F _ {p} (v _ {1}), \ldots , d F _ {p} (v _ {k}) \big). \]

Lemma 14.16

FC08-C14-U027 · Ch. 14, § Differential Forms on Manifolds; source L10904 · not formalized

Suppose $F \colon M \to N$ is smooth. (a) $F^{*} \colon \Omega^{k}(N) \to \Omega^{k}(M)$ is linear over $\mathbb{R}$. (b) $F^{*}(\omega \wedge \eta) = (F^{*}\omega) \wedge (F^{*}\eta)$. (c) In any smooth chart, \[ F^{*}\left(\sideset{}{'}\sum_{I} \omega_{I}\,dy^{i_{1}} \wedge \cdots \wedge dy^{i_{k}}\right) = \sideset{}{'}\sum_{I} (\omega_{I} \circ F)\,d(y^{i_{1}} \circ F) \wedge \cdots \wedge d(y^{i_{k}} \circ F). \]

Example 14.18

FC08-C14-U028 · Ch. 14, § Differential Forms on Manifolds; source L10920 · not formalized

Define $F \colon \mathbb{R}^{2} \to \mathbb{R}^{3}$ by $F(u,v) = (u,\ v,\ u^{2}-v^{2})$ and let $\omega = y\,dx \wedge dz + x\,dy \wedge dz$ on $\mathbb{R}^{3}$. Then \[ F^{*}\omega = v\,du \wedge (2u\,du - 2v\,dv) + u\,dv \wedge (2u\,du - 2v\,dv) = -2v^{2}\,du \wedge dv + 2u^{2}\,dv \wedge du, \] using $du \wedge du = dv \wedge dv = 0$; since $dv \wedge du = -du \wedge dv$ this simplifies to \[ F^{*}\omega = -2(u^{2}+v^{2})\,du \wedge dv. \]

Example 14.19

FC08-C14-U029 · Ch. 14, § Differential Forms on Manifolds; source L10934 · not formalized

Thinking of the transformation to polar coordinates $x = r \cos \theta , y = r$ sin as an expression for the identity map with respect to different coordinates on the domain and codomain, we obtain \[ \begin{array}{r l} d x \wedge d y & = d (r \cos \theta) \wedge d (r \sin \theta) \\ & = (\cos \theta d r - r \sin \theta d \theta) \wedge (\sin \theta d r + r \cos \theta d \theta) \\ & = r d r \wedge d \theta . \end{array} \] The similarity between this formula and the formula for changing a double integral from Cartesian to polar coordinates is striking. The following proposition generalizes this.

Proposition 14.20

FC08-C14-U030 · Ch. 14, § Differential Forms on Manifolds; source L10942 · not formalized

Proposition 14.20 (Pullback Formula for Top-Degree Forms). Let $F \colon M \to N$ be a smooth map between n-manifolds with or without boundary. $H \left( x ^ { i } \right)$ and $\left( y ^ { j } \right)$ are smooth coordinates on open subsets $U \subseteq M$ and $V \subseteq N$ , respectively, and u is a continuous real-valued function on V , then the following holds on $U \cap F ^ { - 1 } ( V )$ \[ F ^ {*} \left(u d y ^ {1} \wedge \dots \wedge d y ^ {n}\right) = (u \circ F) (\det D F) d x ^ {1} \wedge \dots \wedge d x ^ {n},\tag{14.15} \] where DF represents the Jacobian mat Compute the coordinate representation of $\mathring { g }$ in stereographic coordinates (see Problem 1-7).

Corollary 14.21

FC08-C14-U031 · Ch. 14, § Differential Forms on Manifolds; source L10964 · not formalized

If $(U,(x^{i}))$ and $(\widetilde{U},(\widetilde{x}^{j}))$ are overlapping smooth charts on $M$, then on $U \cap \widetilde{U}$ \[ d\widetilde{x}^{1} \wedge \cdots \wedge d\widetilde{x}^{n} = \det\left(\frac{\partial \widetilde{x}^{j}}{\partial x^{i}}\right) dx^{1} \wedge \cdots \wedge dx^{n}. \tag{14.16} \]

Definition/convention — exterior derivative

FC08-C14-U032 · Ch. 14, § Exterior Derivatives; source L10986 · not formalized

Derivatives In this section we define a natural differential operator on smooth forms, called the exterior derivative. It is a generalization of the differential of a function.

Not formalized. none; no complete checked declaration under strict bundle semantics — Neither pinned Mathlib nor current H contains a manifold differential-form exterior-derivative API. Searches find no smooth DifferentialForm type with d, no Cartan formula, and no Lie-derivative/exterior-derivative package; the existing vector-space alternating maps and topological alternating-map bundle are only prerequisites. Strict whole-row semantics reject proper subsets, missing representation bridges, and reconstruction of substantive source theorems from generic ingredients.

Definition/convention — its exterior derivative d

FC08-C14-U033 · Ch. 14, § Exterior Derivatives; source L11004 · not formalized

The definition of d on Euclidean space is straightforward: if $\begin{array} { r } { \omega = \sum _ { J } ^ { \prime } \omega _ { J } d x ^ { J } } \end{array}$ is a smooth k-form on an open subset $U \subseteq \mathbb { R } ^ { n }$ or $\mathbb { H } ^ { n }$ , we define its exterior derivative d! to be the following $( k + 1 )$ /-form: \[ d \left(\sum_ {J} ^ {\prime} \omega_ {J} d x ^ {J}\right) = \sum_ {J} ^ {\prime} d \omega_ {J} \wedge d x ^ {J},\tag{14.19} \]

Proposition 14.23

FC08-C14-U034 · Ch. 14, § Exterior Derivatives; source L11032 · not formalized

Proposition 14.23 (Properties of the Exterior Derivative on $\mathbb { R } ^ { n } )$ ). (a) d is linear over R. (b) If ! is a smooth k-form and is a smooth l-form on an open subset $U \subseteq \mathbb { R } ^ { n }$ or H, then \[ d (\omega \wedge \eta) = d \omega \wedge \eta + (- 1) ^ {k} \omega \wedge d \eta . \] (c) d $\circ d \equiv 0$ (d) d commutes with pullbacks: $i f U$ is an open subset of $\mathbb { R } ^ { n }$ or $\mathbb { H } ^ { n }$ , V is an open subset of $\mathbb { R } ^ { m }$ or $\mathbb { H } ^ { m } , F \colon U \to V$ is a smooth map, and $\omega \in \Omega ^ { k } ( V )$ , then \[ F ^ {*} (d \omega) = d \left(F ^ {*} \omega\right).\tag{14.21} \]

Theorem 14.24

FC08-C14-U035 · Ch. 14, § Exterior Derivatives; source L11092 · not formalized

Theorem 14.24 (Existence and Uniqueness of Exterior Differentiation). Suppose M is a smooth manifold with or without boundary. There are unique operators $d \colon \Omega ^ { k } ( M ) \Omega ^ { k + 1 } ( M )$ for all k, called exterior differentiation, satisfying the following four properties: (i) d is linear over R. (ii) If $\omega \in \Omega ^ { k } ( M )$ and $\eta \in \Omega ^ { l } ( M )$ , then \[ d (\omega \wedge \eta) = d \omega \wedge \eta + (- 1) ^ {k} \omega \wedge d \eta . \] (iii) d $\circ d \equiv 0$ (iv) For $f \in \Omega ^ { 0 } ( M ) = C ^ { \infty } ( M )$ , df is the differential of f , given by $d f ( X ) =$ $X f$ In any smooth coordinate chart, d is given by (14.19).

Definition/convention — a map of degree m

FC08-C14-U036 · Ch. 14, § Exterior Derivatives; source L11126 · not formalized

If $A = \bigoplus_{k} A^{k}$ is a graded algebra, a linear map $T \colon A \to A$ has degree $m$ if $T(A^{k}) \subseteq A^{k+m}$ for each $k$, and is an antiderivation if $T(xy) = (Tx)y + (-1)^{k}x(Ty)$ whenever $x \in A^{k}$ and $y \in A^{l}$. The preceding theorem says the differential on functions extends uniquely to an antiderivation of $\Omega^{*}(M)$ of degree $1$ whose square is zero.

Proposition 14.26

FC08-C14-U037 · Ch. 14, § Exterior Derivatives; source L11132 · not formalized

Proposition 14.26 (Naturality of the Exterior Derivative). If $F \colon M \to N$ is a smooth map, then for each k the pullback map $F ^ { * } \colon \Omega ^ { k } ( N ) \to \Omega ^ { k } ( M )$ commutes with d : for all $\omega \in \Omega ^ { k } ( N )$ , \[ F ^ {*} (d \omega) = d (F ^ {*} \omega).\tag{14.23} \]

Definition/convention — source terminology/construction

FC08-C14-U038 · Ch. 14, § Exterior Derivatives; source L11148 · not formalized

Extending the terminology we introduced for covector fields in Chapter 11, we say that a smooth differential form $\omega \in \Omega ^ { k } ( M )$ is closed if $d \omega = 0$ , and exact if there exists a smooth $( k - 1 )$ -form on M such that $\omega = d \eta$ . Because the exterior derivative of a 1-form satisfies (14.18), this definition of closed 1-forms agrees with the one we gave in Chapter 11.

Example 14.27

FC08-C14-U039 · Ch. 14, § Exterior Derivatives and Vector Calculus in ℝ ^3; source L11154 · not formalized

Example 14.27. Let us work out the exterior derivatives of arbitrary 1-forms and 2-forms on $\mathbb { R } ^ { 3 }$ . Any smooth 1-form can be written \[ \omega = P d x + Q d y + R d z \] for some smooth functions P; Q; R. Using (14.19) and the fact that the wedge product of any 1-form with itself is zero, we compute \[ \begin{array}{l} d \omega = d P \wedge d x + d Q \wedge d y + d R \wedge d z \\ \qquad = \left(\frac {\partial P}{\partial x} d x + \frac {\partial P}{\partial y} d y + \frac {\partial P}{\partial z} d z\right) \wedge d x + \left(\frac {\partial Q}{\partial x} d x + \frac {\partial Q}{\partial y} d y + \frac {\partial Q}{\partial z} d z\right) \wedge d y \\ \qquad + \left(\frac {\partial R}{\partial x} d x + \frac {\partial R}{\partial y} d y + \frac {\partial R}{\partial z} d z\right) \wedge d z \\ \qquad = \left(\frac {\partial Q}{\partial x} - \frac {\partial P}{\partial y}\right) d x \wedge d y + \left(\frac {\partial R}{\partial x} - \frac {\partial P}{\partial z}\right) d x \wedge d z \\ \qquad + \left(\frac {\partial R}{\partial y} - \frac {\partial Q}{\partial z}\right) d y \wedge d z. \end{array} \] on $\mathbb { R } ^ { 3 }$ can be written \[ \eta = u d x \wedge d y + v d x \wedge d z + w d y \wedge d z. \] computation shows that \[ d \eta = \left(\frac {\partial u}{\partial z} - \frac {\partial v}{\partial y} + \frac {\partial w}{\partial x}\right) d x \wedge d y \wedge d z. \] vector calculus operators on $\mathbb { R } ^ { n }$ : the (Euclidean) gradient of a function $f \in C ^ { \infty } ( \mathbb { R } ^ { n } )$ and divergence of a vector field $X \in { \mathfrak { X } } ( \mathbb { R } ^ { n } )$ f = _ {i = 1} ^ {n} , X = _ {i = 1} ^ {n} . \[ In addition, in the case $n = 3$ , the curl of a vector field $X \in \mathcal { X } \left( \mathbb { R } ^ { 3 } \right)$ is defined by (11.26). It is interesting to note that the components of the 2-form d! in the preceding example are exactly the components of the curl of the vector field with components $( P , Q , R )$ (except perhaps in a different order and with different signs). Similarly, but for signs and ordering of terms, there is a strong analogy between the formula for $d \eta$ and the divergence of a vector field. These analogies can be made precise in the following way. The Euclidean metric on $\mathbb { R } ^ { 3 }$ yields an index-lowering isomorphism [ $\mathcal { X } ( \mathbb { R } ^ { 3 } ) $ $\Omega ^ { 1 } \left( \mathbb { R } ^ { 3 } \right)$ . Interior multiplication yields another map $\beta \colon \mathfrak { X } ( \mathbb { R } ^ { 3 } ) \Omega ^ { 2 } ( \mathbb { R } ^ { 3 } )$ as follows: \] $T M$ to $\Lambda ^ { 2 } T ^ { * } \mathbb { R } ^ { 3 }$ . It is a bundle because it is injective and both $T M$ and $\Lambda ^ { 2 } T ^ { * } \mathbb { R } ^ { 3 }$ are bundles of rank 3. Similarly, we define bundle isomorphism $C ^ { \infty } ( \mathbb { R } ^ { 3 } ) \Omega ^ { 3 } ( \mathbb { R } ^ { 3 } )$ by \[ * (f) = f d x \wedge d y \wedge d z.\tag{14.26} \] all of these operators are summarized in the following diagram: \[ \begin{array}{c} C ^ {\infty} \left(\mathbb {R} ^ {3}\right) \xrightarrow {\text { grad }} \mathfrak {X} \left(\mathbb {R} ^ {3}\right) \xrightarrow {\text { curl }} \mathfrak {X} \left(\mathbb {R} ^ {3}\right) \xrightarrow {\text { div }} C ^ {\infty} \left(\mathbb {R} ^ {3}\right) \\ \Biggl \downarrow \text { Id } \qquad \qquad \Biggl \downarrow_ {\flat} \qquad \qquad \Biggl \downarrow_ {\beta} \qquad \qquad \Biggl \downarrow_ {*} \\ \Omega^ {0} \left(\mathbb {R} ^ {3}\right) \xrightarrow [ d ]{} \Omega^ {1} \left(\mathbb {R} ^ {3}\right) \xrightarrow [ d ]{} \Omega^ {2} \left(\mathbb {R} ^ {3}\right) \xrightarrow [ d ]{} \Omega^ {3} \left(\mathbb {R} ^ {3}\right). \end{array}\tag{14.27} \]

Proposition 14.29

FC08-C14-U040 · Ch. 14, § An Invariant Formula for the Exterior Derivative; source L11212 · not formalized

Proposition 14.29 (Exterior Derivative of a 1-Form). For any smooth 1-form ! and smooth vector fields X and $Y$ , \[ d \omega (X, Y) = X (\omega (Y)) - Y (\omega (X)) - \omega ([ X, Y ]).\tag{14.28} \]

Proposition 14.30

FC08-C14-U041 · Ch. 14, § An Invariant Formula for the Exterior Derivative; source L11234 · not formalized

Let $M$ be a smooth $n$-manifold with or without boundary, $(E_{i})$ a smooth local frame and $(\varepsilon^{i})$ the dual coframe. Define $b^{i}_{jk}$ and $c^{i}_{jk}$ by \[ d\varepsilon^{i} = \sum_{j<k} b^{i}_{jk}\,\varepsilon^{j} \wedge \varepsilon^{k}, \qquad [E_{j},E_{k}] = c^{i}_{jk}E_{i}. \] Then $b^{i}_{jk} = -c^{i}_{jk}$.

Proposition 14.32

FC08-C14-U042 · Ch. 14, § An Invariant Formula for the Exterior Derivative; source L11246 · not formalized

(Invariant Formula for the Exterior Derivative). Let $M$ be a smooth manifold with or without boundary and $\omega \in \Omega^{k}(M)$. For any smooth vector fields $X_{1},\dots,X_{k+1}$ on $M$, \[ d\omega(X_{1},\dots,X_{k+1}) = \sum_{1 \leq i \leq k+1} (-1)^{i-1} X_{i}\big(\omega(X_{1},\dots,\widehat{X}_{i},\dots,X_{k+1})\big) + \sum_{1 \leq i < j \leq k+1} (-1)^{i+j} \omega\big([X_{i},X_{j}],X_{1},\dots,\widehat{X}_{i},\dots,\widehat{X}_{j},\dots,X_{k+1}\big), \tag{14.29} \] the hats indicating omitted arguments.

Proposition 14.33

FC08-C14-U043 · Ch. 14, § Lie Derivatives of Differential Forms; source L11320 · not formalized

Suppose $M$ is a smooth manifold, $V \in \mathfrak{X}(M)$ and $\omega, \eta \in \Omega^{*}(M)$. Then \[ \mathcal{L}_{V}(\omega \wedge \eta) = (\mathcal{L}_{V}\omega) \wedge \eta + \omega \wedge (\mathcal{L}_{V}\eta). \]

Theorem 14.35

FC08-C14-U044 · Ch. 14, § Lie Derivatives of Differential Forms; source L11330 · not formalized

Theorem 14.35 (Cartan’s Magic Formula). On a smooth manifold M; for any smooth vector field V and any smooth differential form !, \[ \mathcal {L} _ {V} \omega = V \lrcorner (d \omega) + d (V \lrcorner \omega).\tag{14.32} \]

Corollary 14.36

FC08-C14-U045 · Ch. 14, § Lie Derivatives of Differential Forms; source L11364 · not formalized

Corollary 14.36 (The Lie Derivative Commutes with d). $I f V$ is a smooth vector field and ! is a smooth differential form, then \[ \mathcal {L} _ {V} (d \omega) = d (\mathcal {L} _ {V} \omega). \] Proof.