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

FC08 — Lee, Introduction to Smooth Manifolds.

This chapter contains 16 definitions, 1 theorem, 13 propositions, 2 lemmas, 4 corollaries, 5 examples, 2 constructions and 6 conventions.

Of the 49 statements checked against Lean, 10 are formalized somewhere and 39 are not.

Status	Statements	Share	What it means
not formalized	39	80%	A documented search found no Lean statement of it anywhere.
in Mathlib	10	20%	Mathlib states and proves it.
checked in total	49

Which versions of Lean and Mathlib were searched

Canonical source block: FC08 Lee, Chapter 12, FC08-C12-U001–FC08-C12-U049, exactly 49 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 indexed/external Lean searches. No project-existing, package-import, or reference-port C12 owner survived strict whole-row checking.
C12 has 10 pinned mathlib rows and 39 dated unmatched rows. Positive rows are: U001, U004, U005, U006, U008, U009, U010, U012, U014, U027.
The algebraic tensor-product layer is strongly covered. MultilinearMap owns U001; Basis.multilinearMap gives the dual-coordinate basis of scalar-valued multilinear maps for U004; S →₀ ℝ and Finsupp.lift give the free real vector space and its universal property for U005–U006. PiTensorProduct gives an indexed k-fold tensor product, pure-tensor map, relations, spanning theorem, universal property, and pure-tensor basis, owning U008–U010.
U012 is a checked short assembly rather than an inferred equivalence. For finite-dimensional real factors, PiTensorProduct.dualDistribEquiv identifies the tensor product of duals with the dual of the tensor product, and PiTensorProduct.lift identifies that dual with scalar-valued multilinear maps. /tmp/fc08-c12-witness.lean compiles their canonical composite and proves the expected pure-tensor evaluation formula. The same witness typechecks U014’s k-fold-dual representation.
U011 is deliberately not inferred from the available associators. P has TensorProduct.assoc and PiTensorProduct.tmulEquiv with exact pure-tensor formulas, but no single checked statement supplies Lee’s full pair of canonical three-factor identifications together with the stated uniqueness condition. Strict whole-row semantics keep it unmatched.
The symmetric-tensor block U021–U026 has a clear interface boundary. TensorPower/Symmetric.lean defines SymmetricPower as a quotient by permutations, but its module documentation explicitly leaves the product and universal-property layer as TODO. Exact P/H searches found no Lee-style symmetric-multilinear subspace, averaging symmetrization projection, fixed-point theorem, or normalized symmetric product. The quotient model is not silently identified with Lee’s subspace model.
U027 is independent of that gap: AlternatingMap is exactly an alternating scalar-valued multilinear map, with swap/permutation sign laws and vector-space structure. Combined with the checked U012 tensor/multilinear identification, it is an equivalent formalization of alternating covariant tensors.
The canonical catalogue is visibly truncated at U013, U015, U017, U018, U028, and U030. These rows remain dated unmatched from the canonical text; Sweep II does not reconstruct their missing conclusions from the book.
The manifold half U029–U049 remains blocked at a distinct abstraction boundary. P/H have no general manifold tensor-bundle/tensor-field type for covariant, contravariant, or mixed tensors. Topology/VectorBundle/ContinuousAlternatingMap.lean supplies a topological bundle of continuous alternating maps, while Geometry/Manifold/VectorBundle/Tensoriality.lean gives unary/binary tensoriality criteria on sections; neither is Lee’s arbitrary-k smooth tensor-field layer. Analysis/Calculus/DifferentialForm/Basic.lean separately records manifold differential forms as future work.
Those manifold rows also inherit earlier promoted FC08 boundaries: C03 established that Lee’s tangent vectors use point derivations while Mathlib’s mature manifold vector-bundle APIs use standard TangentSpace, with no checked equivalence; C11 found no manifold cotangent-bundle/1-form layer. The Lie-derivative rows U042–U049 additionally depend on the C09 local/maximal-flow layer, which is absent at P/H.
Current upstream H=5315eef9e4ffb98e0f89f278b765c50a149f66ca was searched by exact git object and does not add a manifold tensor-field bundle, tensor Lie derivative, symmetric-multilinear projection/product, or a bridge that closes these gaps. Targeted external searches surfaced no compatible completed Lean owner warranting reference-port.
N=2026-09-07 marks dated unmatched decisions after the prescribed search layers. Strict whole-row semantics apply uniformly.

Definition/convention — multilinear

FC08-C12-U001 · Ch. 12, § Multilinear Algebra; source L8889 · in Mathlib

Suppose $V_{1},\dots,V_{k}$ and $W$ are vector spaces. A map $F \colon V_{1} \times \cdots \times V_{k} \to W$ is multilinear if it is linear in each variable separately when the others are held fixed: for each $i$, \[ F(v_{1},\dots,av_{i} + a'v_{i}',\dots,v_{k}) = aF(v_{1},\dots,v_{i},\dots,v_{k}) + a'F(v_{1},\dots,v_{i}',\dots,v_{k}). \] The multilinear maps form a vector space $\operatorname{L}(V_{1},\dots,V_{k};W)$ under pointwise addition and scalar multiplication.

Formalized. Mathlib/LinearAlgebra/Multilinear/Basic.lean::MultilinearMap — MultilinearMap ℝ V W is precisely a map linear in each argument separately. Its dependent-domain form covers Lee’s possibly different vector spaces V₁,…,Vₖ.

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

Example 12.1

FC08-C12-U002 · Ch. 12, § Multilinear Algebra; source L8903 · not formalized

Example 12.1 (Some Familiar Multilinear Functions). (a) The dot product in $\mathbb { R } ^ { n }$ is a scalar-valued bilinear function of two vectors, used to compute lengths of vectors and angles between them. (b) The cross product in $\mathbb { R } ^ { 3 }$ is a vector-valued bilinear function of two vectors, used to compute areas of parallelograms and to find a third vector orthogonal to two given ones. (c) The determinant is a real-valued multilinear function of n vectors in $\mathbb { R } ^ { n }$ , used to detect linear independence and to compute the volume of the parallelepiped spanned by the vectors. (d) The bracket in a Lie algebra $\mathfrak { g }$ is a g-valued bilinear function of two elements of $\mathfrak{g}$.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib separately formalizes dot products, cross products, determinants, and Lie brackets, but no single checked declaration packages Lee’s four-example multilinear bundle. The row is therefore not owned as a whole. Strict whole-row semantics reject proper subsets, unproved equivalences, stronger hypotheses, truncated-source reconstruction, and substantive assembly from generic ingredients.

Example 12.2

FC08-C12-U003 · Ch. 12, § Multilinear Algebra; source L8915 · not formalized

Example 12.2 (Tensor Products of Covectors). Suppose V is a vector space, and $\omega , \eta \in V ^ { * }$ . Define a function $\omega \otimes \eta \colon V \times V \to \mathbb { R }$ by \[ \omega \otimes \eta (v _ {1}, v _ {2}) = \omega (v _ {1}) \eta (v _ {2}), \] where the product on the right is just ordinary multiplication of real numbers. The linearity of ! and guarantees that $\omega \otimes \eta$ is a bilinear function of $v _ { 1 }$ and $v _ { 2 }$ , so it is an element of $\operatorname { L } ( V , V ; \mathbb { R } )$ . For example, if $\left( e ^ { 1 } , e ^ { 2 } \right)$ denotes the standard dual basis for $\left( \mathbb { R } ^ { 2 } \right) ^ { * }$ , then $e ^ { 1 } \otimes e ^ { 2 } \colon \mathbb { R } ^ { 2 } \times \mathbb { R } ^ { 2 } \to \mathbb { R }$ is the bilinear function \[ e ^ {1} \otimes e ^ {2} ((w, x), (y, z)) = w z. \] The last example can be generalized to arbitrary real-valued multilinear functions as follows: let $V _ { 1 } , \dots , V _ { k } , W _ { 1 } , \dots , W _ { l }$ be real vector spaces, and suppose $F \in \operatorname { L } ( V _ { 1 } , \ldots , V _ { k } ; \mathbb { R } )$ and $G \in \mathrm { L } ( W _ { 1 } , \ldots , W _ { l } ; \mathbb { R } )$ . Define a function \[ F \otimes G \colon V _ {1} \times \dots \times V _ {k} \times W _ {1} \times \dots \times W _ {l} \to \mathbb {R} \] by \[ F \otimes G (v _ {1}, \dots , v _ {k}, w _ {1}, \dots , w _ {l}) = F (v _ {1}, \dots , v _ {k}) G (w _ {1}, \dots , w _ {l}).\tag{12.1} \] It follows from the multilinearity of F and $G$ that $F \otimes G ( v _ { 1 } , \ldots , v _ { k } , w _ { 1 } , \ldots , w _ { l } )$ depends linearly on each argument $v _ { i }$ or $w _ { j }$ separately, so $F \otimes G$ is an element of $\operatorname { L } ( V _ { 1 } , \dots , V _ { k } , W _ { 1 } , \dots , W _ { l } ; \mathbb { R } )$ , called the tensor product of F and $\pmb { G }$ . Exercise 12.3. Show that the tensor product operation boundary is said to be exact (or an exact differential) on M if there is a function $f \in$ $C ^ { \infty } ( M )$ such that $\omega = d f$ .

Not formalized. none; no complete checked declaration under strict bundle semantics — MultilinearMap.domCoprod and tensor-product primitives provide ingredients for multiplying scalar-valued multilinear maps on disjoint argument blocks, but no checked declaration packages Lee’s full covector example, explicit ℝ² computation, and general scalar-valued tensor-product construction as one source row. Strict whole-row semantics reject proper subsets, unproved equivalences, stronger hypotheses, truncated-source reconstruction, and substantive assembly from generic ingredients.

Proposition 12.4

FC08-C12-U004 · Ch. 12, § Multilinear Algebra; source L8957 · in Mathlib

(A Basis for the Space of Multilinear Functions). Let $V_{1},\dots,V_{k}$ be real vector spaces of dimensions $n_{1},\dots,n_{k}$. For each $j$ let $\left(E^{(j)}_{1},\dots,E^{(j)}_{n_{j}}\right)$ be a basis for $V_{j}$ and $\left(\varepsilon^{1}_{(j)},\dots,\varepsilon^{n_{j}}_{(j)}\right)$ the dual basis for $V_{j}^{*}$. Then \[ \mathcal{B} = \left\{\varepsilon^{i_{1}}_{(1)} \otimes \cdots \otimes \varepsilon^{i_{k}}_{(k)} : 1 \leq i_{1} \leq n_{1},\ \dots,\ 1 \leq i_{k} \leq n_{k}\right\} \] is a basis for $\operatorname{L}(V_{1},\dots,V_{k};\mathbb{R})$, which therefore has dimension $n_{1}\cdots n_{k}$.

Formalized. Mathlib/LinearAlgebra/Multilinear/Basis.lean::Basis.multilinearMap, Basis.multilinearMap_apply_apply; Mathlib/LinearAlgebra/Basis/Basic.lean::Basis.singleton — Given bases on each finite-dimensional domain and the singleton basis of ℝ, Basis.multilinearMap gives the basis of scalar-valued multilinear maps indexed by tuples of basis indices; multilinearMap_apply_apply identifies its elements with products of the corresponding dual-coordinate functionals. This is Lee’s basis and dimension statement up to the inessential singleton codomain index.

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

Definition/convention — formal linear combination of elements of S

FC08-C12-U005 · Ch. 12, § Abstract Tensor Products of Vector Spaces; source L8999 · in Mathlib

simple.) To begin, we need to make sense of “formal linear combinations.” Let S be a set. Roughly speaking, a formal linear combination of elements of S is an expression of the form $\scriptstyle \sum _ { i = 1 } ^ { m } a _ { i } x _ { i }$ , where $a _ { 1 } , \ldots , a _ { m }$ are real numbers and $x _ { 1 } , \ldots , x _ { m }$ are elements of S. Of course, since we are not assuming that S has any algebraic structure, we cannot literally add elements of S together or multiply them by numbers. But the essential feature of such an expression is that it is completely determined by which elements of S appear in the sum, and what coefficients appear with them. Thus, we make the following definition: for any set S, a formal linear combination of elements of S is a function $f \colon S \to \mathbb { R }$ such that $f ( s ) = 0$ for all but finitely many $s \in S$ . The free (real) vector space on S , denoted by ${ \mathcal { F } } ( S )$ , is the set of all formal linear combinations of elements of S. Under pointwise addition and scalar multiplication, ${ \mathcal { F } } ( S )$ becomes have $d f = \omega$ , thus completing the proof.

Formalized. Mathlib/Data/Finsupp/Defs.lean::Finsupp; Mathlib/LinearAlgebra/Finsupp/Defs.lean::Finsupp.instModule — S →₀ ℝ is exactly the type of finitely supported coefficient functions on S, with pointwise additive and real-module structure: Lee’s free real vector space on the set S.

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

Proposition 12.5

FC08-C12-U006 · Ch. 12, § Abstract Tensor Products of Vector Spaces; source L9003 · in Mathlib

Proposition 12.5 (Characteristic Property of the Free Vector Space). For any set S and any vector space W , every map $A \colon S W$ has a unique extension to a linear map $\overline { { A } } \colon \mathcal { F } ( S ) \to W$ Exercise 12.6. Prove the preceding act.

Formalized. Mathlib/LinearAlgebra/Finsupp/LSum.lean::Finsupp.lift, Finsupp.lift_symm_apply — Finsupp.lift is the free-forgetful adjunction equivalence between arbitrary functions S → W and linear maps (S →₀ ℝ) →ₗ[ℝ] W; its inverse recovers the map on basis elements. This is exactly the existence-and-uniqueness characteristic property.

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

Definition/convention — source terminology/construction

FC08-C12-U007 · Ch. 12, § Abstract Tensor Products of Vector Spaces; source L9007 · not formalized

For real vector spaces $V_{1},\dots,V_{k}$, form the free vector space $\mathcal{F}(V_{1} \times \cdots \times V_{k})$ of finite formal linear combinations of $k$-tuples $(v_{1},\dots,v_{k})$ with $v_{i} \in V_{i}$, and let $\mathcal{R}$ be the subspace spanned by all elements of the forms \[ (v_{1},\dots,av_{i},\dots,v_{k}) - a(v_{1},\dots,v_{i},\dots,v_{k}), \] \[ (v_{1},\dots,v_{i}+v_{i}',\dots,v_{k}) - (v_{1},\dots,v_{i},\dots,v_{k}) - (v_{1},\dots,v_{i}',\dots,v_{k}), \tag{12.4} \] with $v_{j}, v_{j}' \in V_{j}$, $i \in \{1,\dots,k\}$ and $a \in \mathbb{R}$. The tensor product is the quotient $\mathcal{F}(V_{1} \times \cdots \times V_{k})/\mathcal{R}$.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib’s indexed tensor product uses an equivalent quotient by a generated congruence on a free additive monoid; it does not expose Lee’s particular intermediate subspace R inside the free vector space on tuples. U008 owns the resulting tensor product, but this implementation-specific construction row has no exact interface owner. Strict whole-row semantics reject proper subsets, unproved equivalences, stronger hypotheses, truncated-source reconstruction, and substantive assembly from generic ingredients.

Construction/definition — the (abstract) tensor product of v

FC08-C12-U008 · Ch. 12, § Abstract Tensor Products of Vector Spaces; source L9019 · in Mathlib

The tensor product of $V_{1},\dots,V_{k}$ is the quotient vector space \[ V_{1} \otimes \cdots \otimes V_{k} = \mathcal{F}(V_{1} \times \cdots \times V_{k})/\mathcal{R}, \] with natural projection $\pi$. The class of $(v_{1},\dots,v_{k})$ is written \[ v_{1} \otimes \cdots \otimes v_{k} = \pi(v_{1},\dots,v_{k}), \tag{12.5} \] the abstract tensor product of $v_{1},\dots,v_{k}$. It follows that $v_{1} \otimes \cdots \otimes av_{i} \otimes \cdots \otimes v_{k} = a(v_{1} \otimes \cdots \otimes v_{i} \otimes \cdots \otimes v_{k})$ and $v_{1} \otimes \cdots \otimes (v_{i}+v_{i}') \otimes \cdots \otimes v_{k} = (v_{1} \otimes \cdots \otimes v_{i} \otimes \cdots \otimes v_{k}) + (v_{1} \otimes \cdots \otimes v_{i}' \otimes \cdots \otimes v_{k})$. Every element of the tensor product is a linear combination of elements $v_{1} \otimes \cdots \otimes v_{k}$, though not in general of that form itself.

Formalized. Mathlib/LinearAlgebra/PiTensorProduct/Basic.lean::PiTensorProduct, PiTensorProduct.tprod, PiTensorProduct.Eqv, PiTensorProduct.span_tprod_eq_top — PiTensorProduct ℝ V is the indexed tensor product, defined by quotienting formal generators by additivity/scalar relations in each slot. tprod is the pure-tensor map and span_tprod_eq_top says pure tensors span. This is an equivalent formal construction of Lee’s abstract k-fold tensor product and its displayed multilinearity relations.

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

Proposition 12.7

FC08-C12-U009 · Ch. 12, § Abstract Tensor Products of Vector Spaces; source L9043 · in Mathlib

(Characteristic Property of the Tensor Product Space). Let $V_{1},\dots,V_{k}$ be finite-dimensional real vector spaces. If $A \colon V_{1} \times \cdots \times V_{k} \to X$ is any multilinear map into a vector space $X$, there is a unique linear map $\widetilde{A} \colon V_{1} \otimes \cdots \otimes V_{k} \to X$ with $\widetilde{A} \circ \pi = A$, where $\pi(v_{1},\dots,v_{k}) = v_{1} \otimes \cdots \otimes v_{k}$.

Formalized. Mathlib/LinearAlgebra/PiTensorProduct/Basic.lean::PiTensorProduct.lift, PiTensorProduct.lift.tprod, PiTensorProduct.lift.unique — PiTensorProduct.lift is a linear equivalence between multilinear maps from the factors and linear maps out of their indexed tensor product; lift.tprod gives the commuting triangle and lift.unique gives uniqueness. This is Lee’s universal property exactly.

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

Proposition 12.8

FC08-C12-U010 · Ch. 12, § Abstract Tensor Products of Vector Spaces; source L9067 · in Mathlib

Proposition 12.8 (A Basis for the Tensor Product Space). Suppose $V _ { 1 } , \dots , V _ { k }$ are real vector spaces of dimensions $n _ { 1 } , \ldots , n _ { k }$ , respectively. For each $j = 1 , \dots , k$ suppose $\big ( E _ { 1 } ^ { ( j ) } , \dots , E _ { n _ { j } } ^ { ( j ) } \big )$ is a basis for $V _ { j }$ . Then the set \[ \mathcal {C} = \left\{E _ {i _ {1}} ^ {(1)} \otimes \dots \otimes E _ {i _ {k}} ^ {(k)}: 1 \leq i _ {1} \leq n _ {1}, \dots , 1 \leq i _ {k} \leq n _ {k} \right\} \] is a basis for $V _ { 1 } \otimes \cdots \otimes V _ { k }$ , which therefore has dimension t there is no smooth (or even continuous) angle function on all of $\mathbb { R } ^ { 2 } \setminus \{ 0 \}$ , which is a consequence of the “hole” in the center.

Formalized. Mathlib/LinearAlgebra/PiTensorProduct/Basis.lean::Basis.piTensorProduct, Basis.piTensorProduct_apply — Basis.piTensorProduct gives the basis indexed by tuples of basis indices and Basis.piTensorProduct_apply identifies each basis vector with the corresponding pure tensor. /tmp/fc08-c12-witness.lean compiles the resulting finite-dimensional dimension formula as the product of the factor basis cardinalities.

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

Proposition 12.9

FC08-C12-U011 · Ch. 12, § Abstract Tensor Products of Vector Spaces; source L9097 · not formalized

(Associativity of Tensor Product Spaces). Let $V_{1}, V_{2}, V_{3}$ be finite-dimensional real vector spaces. There are unique isomorphisms \[ V_{1} \otimes (V_{2} \otimes V_{3}) \cong V_{1} \otimes V_{2} \otimes V_{3} \cong (V_{1} \otimes V_{2}) \otimes V_{3}, \] under which $v_{1} \otimes (v_{2} \otimes v_{3})$, $v_{1} \otimes v_{2} \otimes v_{3}$ and $(v_{1} \otimes v_{2}) \otimes v_{3}$ all correspond.

Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib has the binary associator TensorProduct.assoc and indexed flattening equivalences PiTensorProduct.tmulEquiv, all with pure-tensor formulas. No checked theorem packages Lee’s entire three-space statement with both canonical identifications and their stated uniqueness characterization, so the row is not inferred from adjacent equivalences. Strict whole-row semantics reject proper subsets, unproved equivalences, stronger hypotheses, truncated-source reconstruction, and substantive assembly from generic ingredients.

Proposition 12.10

FC08-C12-U012 · Ch. 12, § Abstract Tensor Products of Vector Spaces; source L9115 · in Mathlib

Proposition 12.10 (Abstract vs. Concrete Tensor Products). If $V _ { 1 } , \dots , V _ { k }$ are finite-dimensional vector spaces, there is a canonical isomorphism \[ V _ {1} ^ {*} \otimes \dots \otimes V _ {k} ^ {*} \cong \mathrm{L} (V _ {1}, \ldots , V _ {k}; \mathbb {R}), \] under which the abstract tensor product defined by (12.5) corresponds to the tensor product of covectors defined ying family of paths starting at a fixed base point and reaching every point of the domain exactly once.

Formalized. Mathlib/LinearAlgebra/PiTensorProduct/Dual.lean::PiTensorProduct.dualDistribEquiv; Mathlib/LinearAlgebra/PiTensorProduct/Basic.lean::PiTensorProduct.lift — For finite-dimensional real spaces, dualDistribEquiv identifies the tensor product of the duals with the dual of the indexed tensor product, while PiTensorProduct.lift identifies that dual with scalar-valued multilinear maps. Their canonical composite is Lee’s abstract-vs-concrete tensor isomorphism; /tmp/fc08-c12-witness.lean compiles the composite and proves that a pure tensor of covectors evaluates as the product of their evaluations.

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

Convention/notation — source terminology/construction

FC08-C12-U013 · Ch. 12, § Abstract Tensor Products of Vector Spaces; source L9137 · not formalized

Using this canonical isomorphism, we henceforth use the notation V _1 * ⊗ ·s ⊗ V _k * to denote either the abstract tensor product space or the space L ( V _1 , … , V _k ; ℝ ) focusing on whichever interpretation is more convenient for the problem at hand. Since we are assuming the vector spaces are all finite-dimensional, we can also identify each V _j with its second dual space V _j ^* * , and thereby obtain another canonical identification \[ V_{1} \otimes \cdots \otimes V_{k} \cong \operatorname{L}\big(V_{1}^{*},\dots,V_{k}^{*};\mathbb{R}\big). \]

Not formalized. none; no complete checked declaration under strict bundle semantics — The canonical Sweep-I source statement for U013 is truncated before completing its mathematical assertion. Sweep II preserves that source defect and does not reconstruct the missing conclusion from the book or nearby rows. Strict whole-row semantics reject proper subsets, unproved equivalences, stronger hypotheses, truncated-source reconstruction, and substantive assembly from generic ingredients.

Definition/convention — covariant k-tensor

FC08-C12-U014 · Ch. 12, § Covariant and Contravariant Tensors on a Vector Space; source L9145 · in Mathlib

Let V be a finite-dimensional real vector space. If k is a positive integer, a covariant k-tensor on V is an element of the k-fold tensor product $V ^ { * } \otimes \cdots \otimes V ^ { * }$ , which we typically think of as a real-valued multilinear function of k elements of $V :$ : \[ \alpha \colon \underbrace {V \times \cdots \times V} _ {k \text { copies }} \to \mathbb {R}. \]

Formalized. Mathlib/LinearAlgebra/PiTensorProduct/Basic.lean::PiTensorProduct; Mathlib/LinearAlgebra/PiTensorProduct/Dual.lean::PiTensorProduct.dualDistribEquiv; Mathlib/LinearAlgebra/PiTensorProduct/Basic.lean::PiTensorProduct.lift — Specializing the indexed family to Fin k → V* gives exactly the k-fold tensor product of the dual; the U012 canonical equivalence realizes it as a scalar-valued k-multilinear map. The audit witness typechecks this representation as CovariantTensor at P.

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

Convention/notation — rank of

FC08-C12-U015 · Ch. 12, § Covariant and Contravariant Tensors on a Vector Space; source L9151 · not formalized

The number k is called the rank of ˛. A 0-tensor is, by convention, just a real number (a real-valued function depending multilinearly on no vectors!). We denote the vector space of all covariant k-tensors on V by the shorthand notation \[ T^{k}(V^{*}) = \underbrace{V^{*} \otimes \cdots \otimes V^{*}}_{k \text{ copies}}. \]

Not formalized. none; no complete checked declaration under strict bundle semantics — The canonical Sweep-I source statement for U015 is truncated before completing its mathematical assertion. Sweep II preserves that source defect and does not reconstruct the missing conclusion from the book or nearby rows. Strict whole-row semantics reject proper subsets, unproved equivalences, stronger hypotheses, truncated-source reconstruction, and substantive assembly from generic ingredients.

Example 12.11

FC08-C12-U016 · Ch. 12, § Covariant and Contravariant Tensors on a Vector Space; source L9159 · not formalized

Example 12.11 (Covariant Tensors). Let V be a finite-dimensional vector space. (a) Every linear functional $\omega \colon V \mathbb { R }$ is multilinear, so a covariant 1-tensor is just a covector. Thus, $T ^ { 1 } ( V ^ { * } )$ is equal to $V ^ { * }$ (b) A covariant 2-tensor on V is a real-valued bilinear function of two vectors, also called a bilinear form. One example is the dot product on $\mathbb { R } ^ { n }$ . More generally, every inner product is a covariant 2-tensor. (c) The determinant, thought of as a function of n vectors, is a covariant n-tensor _ {W} \ V ^ {} A ^ {} W ^ {*}.

Not formalized. none; no complete checked declaration under strict bundle semantics — Each example has strong nearby algebraic infrastructure, but the row bundles the identifications of 1-tensors with covectors, 2-tensors with bilinear forms/inner products, and determinant as an n-tensor. No single checked declaration owns this whole example bundle. Strict whole-row semantics reject proper subsets, unproved equivalences, stronger hypotheses, truncated-source reconstruction, and substantive assembly from generic ingredients.

Definition/convention — space of contravariant tensors

FC08-C12-U017 · Ch. 12, § Covariant and Contravariant Tensors on a Vector Space; source L9167 · not formalized

For some purposes, it is important to generalize the notion of covariant tensors as follows. For any finite-dimensional real vector space V , we define the space of contravariant tensors on V of rank k to be the vector space \[ T^{k}(V) = \underbrace{V \otimes \cdots \otimes V}_{k \text{ copies}}, \] so $T^{1}(V) = V$ and, by convention, $T^{0}(V) = \mathbb{R}$.

Not formalized. none; no complete checked declaration under strict bundle semantics — The canonical Sweep-I source statement for U017 is truncated before completing its mathematical assertion. Sweep II preserves that source defect and does not reconstruct the missing conclusion from the book or nearby rows. Strict whole-row semantics reject proper subsets, unproved equivalences, stronger hypotheses, truncated-source reconstruction, and substantive assembly from generic ingredients.

Definition/convention — space of mixed tensors

FC08-C12-U018 · Ch. 12, § Covariant and Contravariant Tensors on a Vector Space; source L9181 · not formalized

For any nonnegative integers $k, l$, the space of mixed tensors on $V$ of type $(k,l)$ is \[ T^{(k,l)}(V) = \underbrace{V \otimes \cdots \otimes V}_{k \text{ copies}} \otimes \underbrace{V^{*} \otimes \cdots \otimes V^{*}}_{l \text{ copies}}. \] Some of these spaces coincide: $T^{(0,0)}(V) = \mathbb{R}$, $T^{(0,1)}(V) = V^{*}$, $T^{(1,0)}(V) = V$, $T^{(0,k)}(V) = T^{k}(V^{*})$ and $T^{(k,0)}(V) = T^{k}(V)$.

Not formalized. none; no complete checked declaration under strict bundle semantics — The canonical Sweep-I source statement for U018 is truncated before completing its mathematical assertion. Sweep II preserves that source defect and does not reconstruct the missing conclusion from the book or nearby rows. Strict whole-row semantics reject proper subsets, unproved equivalences, stronger hypotheses, truncated-source reconstruction, and substantive assembly from generic ingredients.

Convention/notation — mixed-tensor notation

FC08-C12-U019 · Ch. 12, § Covariant and Contravariant Tensors on a Vector Space; source L9193 · not formalized

(Be aware that the notation $T ^ { ( k , l ) } ( V )$ is not universal. Another notation that is in common use for this space is $T _ { l } ^ { k } ( V )$ . To make matters worse, some books reverse the roles of k and l in either of these notations; for example, the previous edition of this text used the notation $T _ { k } ^ { l } ( V )$ for the space we are here denoting by $T ^ { ( k , l ) } ( V )$ We have chosen the notation given here because it is common and nearly always means the same thing. The moral, as usual, is that when you read any differential geometry book, you need to make sure you understand the author’s notational conventions.)

Not formalized. none; no complete checked declaration under strict bundle semantics — This row is primarily a source notation/convention about mixed-tensor index order and conflicting literature conventions. Mathlib’s generic tensor types do not formalize that prose convention as a mathematical interface. Strict whole-row semantics reject proper subsets, unproved equivalences, stronger hypotheses, truncated-source reconstruction, and substantive assembly from generic ingredients.

Corollary 12.12

FC08-C12-U020 · Ch. 12, § Covariant and Contravariant Tensors on a Vector Space; source L9199 · not formalized

Let $V$ be an $n$-dimensional real vector space with basis $(E_{i})$ and dual basis $(\varepsilon^{j})$. Then $\{\varepsilon^{i_{1}} \otimes \cdots \otimes \varepsilon^{i_{k}}\}$ is a basis for $T^{k}(V^{*})$, $\{E_{i_{1}} \otimes \cdots \otimes E_{i_{k}}\}$ for $T^{k}(V)$, and $\{E_{i_{1}} \otimes \cdots \otimes E_{i_{k}} \otimes \varepsilon^{j_{1}} \otimes \cdots \otimes \varepsilon^{j_{l}}\}$ for $T^{(k,l)}(V)$, with all indices running from $1$ to $n$. Hence $\dim T^{k}(V^{*}) = \dim T^{k}(V) = n^{k}$ and $\dim T^{(k,l)}(V) = n^{k+l}$. In particular every covariant $k$-tensor $\alpha \in T^{k}(V^{*})$ is uniquely $\alpha = \alpha_{i_{1}\dots i_{k}}\,\varepsilon^{i_{1}} \otimes \cdots \otimes \varepsilon^{i_{k}}$ with $\alpha_{i_{1}\dots i_{k}} = \alpha(E_{i_{1}},\dots,E_{i_{k}})$; for example $T^{2}(V^{*})$ is the space of bilinear forms, each written $\beta = \beta_{ij}\varepsilon^{i} \otimes \varepsilon^{j}$ for a unique $n \times n$ matrix $(\beta_{ij})$. Tensors are understood to be covariant unless stated otherwise.

Not formalized. none; no complete checked declaration under strict bundle semantics — Basis.piTensorProduct, dual bases, and dimension lemmas supply most algebraic ingredients, but this row simultaneously bundles bases for covariant, contravariant, and mixed tensors, all dimension formulas, component expansions, the bilinear-form matrix case, and a source-wide covariant-tensor convention. No single checked interface owns the whole bundle. Strict whole-row semantics reject proper subsets, unproved equivalences, stronger hypotheses, truncated-source reconstruction, and substantive assembly from generic ingredients.

Definition/convention — symmetric

FC08-C12-U021 · Ch. 12, § Symmetric Tensors; source L9237 · not formalized

Let V be a finite-dimensional vector space. A covariant k-tensor ˛ on V is said to be symmetric if its value is unchanged by interchanging any pair of arguments: \[ \alpha (v _ {1}, \dots , v _ {i}, \dots , v _ {j}, \dots , v _ {k}) = \alpha (v _ {1}, \dots , v _ {j}, \dots , v _ {i}, \dots , v _ {k}) \]

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has permutation actions on multilinear maps and a quotient SymmetricPower, but no bundled predicate/subspace for Lee’s symmetric covariant multilinear tensors under the U012 realization. The quotient construction is not silently identified with Lee’s symmetric subspace. Strict whole-row semantics reject proper subsets, unproved equivalences, stronger hypotheses, truncated-source reconstruction, and substantive assembly from generic ingredients.

Convention/notation — new k - t e n s o r

FC08-C12-U022 · Ch. 12, § Symmetric Tensors; source L9253 · not formalized

The set of symmetric covariant k-tensors is a linear subspace of the space $T ^ { k } ( V ^ { * } )$ of all covariant k-tensors on $V :$ ; we denote this subspace by $\Sigma ^ { k } ( \dot { V } ^ { * } )$ There is a natural projection from $T ^ { k } ( V ^ { * } )$ to $\Sigma ^ { k } ( V ^ { * } )$ defined as follows. First, let $S _ { k }$ denote the symmetric group on k elements, that is, the group of permutations of the set $\{ 1 , \ldots , k \}$ . Given a k-tensor ˛ and a permutation $\sigma \in S _ { k }$ , we define a new $k \mathrm { - t e n s o r } ^ { \sigma } \alpha$ by \[ { } ^ { \sigma } \alpha ( v _ { 1 } , \dots , v _ { k } ) = \alpha \left( v _ { \sigma ( 1 ) } , \dots , v _ { \sigma ( k ) } \right) . \]

Not formalized. none; no complete checked declaration under strict bundle semantics — TensorPower/Symmetric.lean defines a quotient symmetric power, but explicitly leaves the product and universal-property layer as TODO; targeted P/H searches found no Lee-style permutation action on covariant tensors, averaging symmetrization projection, fixed-point characterization, or normalized symmetric product. The available quotient is not an equivalent whole-row owner. Strict whole-row semantics reject proper subsets, unproved equivalences, stronger hypotheses, truncated-source reconstruction, and substantive assembly from generic ingredients.

Convention/notation — symmetrization by Sym α

FC08-C12-U023 · Ch. 12, § Symmetric Tensors; source L9259 · not formalized

Note that $^{\tau}(^{\sigma}\alpha) = {}^{\tau\sigma}\alpha$, where $\tau\sigma$ is the composition, $\tau\sigma(i) = \tau(\sigma(i))$ — the reason for writing $\sigma$ before $\alpha$. The projection $\operatorname{Sym} \colon T^{k}(V^{*}) \to \Sigma^{k}(V^{*})$, called symmetrization, is defined by \[ \operatorname{Sym}\alpha = \frac{1}{k!}\sum_{\sigma \in S_{k}} {}^{\sigma}\alpha. \]

Proposition 12.14

FC08-C12-U024 · Ch. 12, § Symmetric Tensors; source L9271 · not formalized

Proposition 12.14 (Properties of Symmetrization). Let ˛ be a covariant tensor on a finite-dimensional vector space. (a) Sym ˛ is symmetric. (b) Sym $\alpha = \alpha$ if and only if ˛ is symmetric.

Definition/convention — their symmetric product to be the ( k

FC08-C12-U025 · Ch. 12, § Symmetric Tensors; source L9291 · not formalized

If ˛ and $\beta$ are symmetric tensors on $V ,$ , then $\alpha \otimes \beta$ is not symmetric in general. However, using the symmetrization operator, it is possible to define a new product that takes a pair of symmetric tensors and yields another symmetric tensor. If $\alpha \in$ $\Sigma ^ { k } ( V ^ { * } )$ and $\beta \in \Sigma ^ { \bar { l } } ( V ^ { * } )$ , we define their symmetric product to be the $( k + l ) \dash$ tensor $\alpha \beta$ (denoted by juxtaposition with no intervening product symbol) given by \[ \alpha \beta = \operatorname{Sym} (\alpha \otimes \beta). \]

Proposition 12.15

FC08-C12-U026 · Ch. 12, § Symmetric Tensors; source L9303 · not formalized

Proposition 12.15 (Properties of the Symmetric Product). (a) The symmetric product is symmetric and bilinear: for all symmetric tensors ˛, $\beta , \gamma$ and all $a , b \in \mathbb { R }$ \[ \begin{array}{c} \alpha \beta = \beta \alpha , \\ (a \alpha + b \beta) \gamma = a \alpha \gamma + b \beta \gamma = \gamma (a \alpha + b \beta). \end{array} \] (b) If ˛ and $\beta$ are covectors, then \[ \alpha \beta = \frac {1}{2} (\alpha \otimes \beta + \beta \otimes \alpha). \] Exercise 12.16. Prove Proposition 12.15. ## Alternating Tensors We continue to assume that V is a finite-dimensional unction $f \in C ^ { \infty } ( U )$ such that X grad $f$ .

Definition/convention — exterior forms

FC08-C12-U027 · Ch. 12, § Alternating Tensors; source L9321 · in Mathlib

We continue to assume that V is a finite-dimensional real vector space. A covariant k-tensor ˛ on $V$ is said to be alternating (or antisymmetric or skew-symmetric) if it changes sign whenever two of its arguments are interchanged. This means that for all vectors $v _ { 1 } , \dotsc , v _ { k } \in V$ and every pair of distinct indices i , j it satisfies \[ \alpha (v _ {1}, \ldots , v _ {i}, \ldots , v _ {j}, \ldots , v _ {k}) = - \alpha (v _ {1}, \ldots , v _ {j}, \ldots , v _ {i}, \ldots , v _ {k}). \] Alternating covariant k-tensors are also variously called exterior forms, multicovectors, or k-covectors. The subspace of all alternating covariant k-tensors on $V$ is denoted by $\Lambda ^ { k } ( V ^ { * } ) \subseteq T ^ { k } ( V ^ { * } )$ . Recall that for any permutation $\sigma \in S _ { k }$ , the sign of , denoted by sgn , is equal to 1 if is even (i.e., can be written as a composition of an even number of transpositions), and 1 if is odd (see Proposition

Formalized. Mathlib/LinearAlgebra/Alternating/Basic.lean::AlternatingMap, AlternatingMap.map_swap, AlternatingMap.map_perm — AlternatingMap ℝ V ℝ (Fin k) is a scalar-valued k-multilinear map that changes sign under swaps/permutations, with the inherited real vector-space structure. Via U012’s tensor/multilinear equivalence this is exactly the space of alternating covariant k-tensors.

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

Definition/convention — alternating 2-tensor

FC08-C12-U028 · Ch. 12, § Alternating Tensors; source L9343 · not formalized

Every 0-tensor (which is just a real number) is both symmetric and alternating, because there are no arguments to interchange. Similarly, every 1-tensor is both symmetric and alternating. An alternating 2-tensor on V is a skew-symmetric bilinear form. It is interesting to note that every covariant 2-tensor β can be expressed as a sum of an alternating tensor and a symmetric one, because \[ \beta(v,w) = \tfrac{1}{2}\big(\beta(v,w) - \beta(w,v)\big) + \tfrac{1}{2}\big(\beta(v,w) + \beta(w,v)\big) = \alpha(v,w) + \sigma(v,w), \] with $\alpha$ alternating and $\sigma$ symmetric.

Not formalized. none; no complete checked declaration under strict bundle semantics — The canonical Sweep-I source statement for U028 is truncated before completing its mathematical assertion. Sweep II preserves that source defect and does not reconstruct the missing conclusion from the book or nearby rows. Strict whole-row semantics reject proper subsets, unproved equivalences, stronger hypotheses, truncated-source reconstruction, and substantive assembly from generic ingredients.

Definition/convention — bundle of covariant k-tensors

FC08-C12-U029 · Ch. 12, § Tensors and Tensor Fields on Manifolds; source L9355 · not formalized

Now let M be a smooth manifold with or without boundary. We define the bundle of covariant k-tensors on M by \[ T ^ {k} T ^ {*} M = \coprod_ {p \in M} T ^ {k} \big (T _ {p} ^ {*} M \big). \]

Not formalized. none; no complete checked declaration under strict bundle semantics — P/H have no general manifold tensor-bundle/tensor-field layer. ContinuousAlternatingMap constructs a topological bundle of alternating maps between arbitrary vector-bundle fibers, and Tensoriality.lean handles unary/binary tensorial operations on sections, but neither supplies Lee’s covariant/contravariant/mixed tensor bundles and smooth fields. These rows also inherit C03’s unbridged point-derivation vs standard-TangentSpace models and C11’s absent manifold cotangent bundle. Strict whole-row semantics reject proper subsets, unproved equivalences, stronger hypotheses, truncated-source reconstruction, and substantive assembly from generic ingredients.

Definition/convention — bundle of contravariant k-tensors by T

FC08-C12-U030 · Ch. 12, § Tensors and Tensor Fields on Manifolds; source L9361 · not formalized

The bundle of contravariant $k$-tensors is \[ T^{k}TM = \coprod_{p \in M} T^{k}\big(T_{p}M\big), \] and the bundle of mixed tensors of type $(k,l)$ is \[ T^{(k,l)}TM = \coprod_{p \in M} T^{(k,l)}\big(T_{p}M\big). \]

Not formalized. none; no complete checked declaration under strict bundle semantics — The canonical Sweep-I source statement for U030 is truncated before completing its mathematical assertion. Sweep II preserves that source defect and does not reconstruct the missing conclusion from the book or nearby rows. Strict whole-row semantics reject proper subsets, unproved equivalences, stronger hypotheses, truncated-source reconstruction, and substantive assembly from generic ingredients.

Definition/convention — tensor bundle

FC08-C12-U031 · Ch. 12, § Tensors and Tensor Fields on Manifolds; source L9397 · not formalized

Any one of these bundles is called a tensor bundle over M . (Thus, the tangent and cotangent bundles are special cases of tensor bundles.) A section of a tensor bundle is called a (covariant, contravariant, or mixed) tensor field on M . A smooth tensor field is a section that is smooth in the usual sense of smooth sections of vector bundles. Using the identifications above, we see that contravariant 1-tensor fields are the same as vector fields, and covariant 1-tensor fields are covector fields. Because a 0-tensor is just a real number, a 0-tensor field is the same as a continuous real-valued function.

Convention/notation — component functions of A in the chosen coordinates

FC08-C12-U032 · Ch. 12, § Tensors and Tensor Fields on Manifolds; source L9405 · not formalized

\[ The functions $A _ { i _ { 1 } . . . i _ { k } } , A ^ { i _ { 1 } . . . i _ { k } }$ , or $A _ { j _ { 1 } \ldots i _ { l } } ^ { i _ { 1 } \ldots i _ { k } }$ are called the component functions of A in the chosen coordinates. Because smooth covariant tensor fields occupy most of our attention, we adopt the following shorthand notation for the space of all smooth covariant k-tensor fields: \] ^ {k} (M) = (T

Proposition 12.19

FC08-C12-U033 · Ch. 12, § Tensors and Tensor Fields on Manifolds; source L9411 · not formalized

Proposition 12.19 (Smoothness Criteria for Tensor Fields). Let M be a smooth manifold with or without boundary, and let A $M \to T ^ { k } T ^ { * } M$ be a rough section. The following are equivalent. (a) A is smooth. (b) In every smooth coordinate chart, the component functions of A are smooth. (c) Each point of M is contained in some coordinate chart in which A has smooth component functions. (d) { k } ( M )$ , then the function $ X _ { k } ) M _ {p} (X _ {1} | _ {p}, , X _ {k} | _ {p} ), smooth. (e) Whenever $X _ { 1 } , \ldots , X _ { k }$ are smooth vector fields defined on some open subset $U \subseteq M$

Proposition 12.22

FC08-C12-U034 · Ch. 12, § Tensors and Tensor Fields on Manifolds; source L9433 · not formalized

Suppose $M$ is a smooth manifold with or without boundary, $A \in \mathcal{T}^{k}(M)$, $B \in \mathcal{T}^{l}(M)$ and $f \in C^{\infty}(M)$. Then $fA$ and $A \otimes B$ are smooth tensor fields, with components in any smooth chart \[ (fA)_{i_{1}\dots i_{k}} = f\,A_{i_{1}\dots i_{k}}, \qquad (A \otimes B)_{i_{1}\dots i_{k+l}} = A_{i_{1}\dots i_{k}}\,B_{i_{k+1}\dots i_{k+l}}. \]

Lemma 12.24

FC08-C12-U035 · Ch. 12, § Tensors and Tensor Fields on Manifolds; source L9455 · not formalized

(Tensor Characterization Lemma). A map \[ \mathcal{A} \colon \underbrace{\mathfrak{X}(M) \times \cdots \times \mathfrak{X}(M)}_{k \text{ copies}} \to C^{\infty}(M) \tag{12.7} \] is induced by a smooth covariant $k$-tensor field if and only if it is multilinear over $C^{\infty}(M)$.

Definition/convention — covariant tensor field

FC08-C12-U036 · Ch. 12, § Tensors and Tensor Fields on Manifolds; source L9489 · after FC08-C12-U026 · not formalized

A symmetric tensor field on a manifold (with or without boundary) is simply a covariant tensor field whose value at each point is a symmetric tensor. The symmetric product of two or more tensor fields is defined pointwise, just like the tensor product. Thus, for example, if A and B are smooth covector fields, their symmetric product is the smooth 2-tensor field AB, which by Proposition 12.15(b) is given by \[ A B = \frac {1}{2} (A \otimes B + B \otimes A). \]

Definition/convention — differential forms

FC08-C12-U037 · Ch. 12, § Tensors and Tensor Fields on Manifolds; source L9495 · not formalized

Alternating tensor fields are called differential forms; we will study them in depth beginning in Chapter 14.

Construction/definition — pointwise pullback of

FC08-C12-U038 · Ch. 12, § Pullbacks of Tensor Fields; source L9501 · not formalized

For any point $p \in M$ and any k-tensor $\alpha \in T ^ { k } \bigl ( T _ { F ( p ) } ^ { * } N \bigr )$ , we define a tensor d $\bar { F } _ { p } ^ { * } ( \alpha ) \in \bar { T } ^ { \bar { k } } \big ( T _ { p } ^ { * } \bar { M } \big )$ , called the pointwise pullback of ˛ by F at p, by \[ d F _ {p} ^ {*} (\alpha) (v _ {1}, \dots , v _ {k}) = \alpha \left(d F _ {p} (v _ {1}), \dots , d F _ {p} (v _ {k})\right) \] for any $v _ { 1 } , \dotsc , v _ { k } \in T _ { p } M$ . If A is a covariant k-tensor field on N , we define a rough k-tensor field $F ^ { * } A$ on M; called the pullback of A by F , by \[ (F ^ {*} A) _ {p} = d F _ {p} ^ {*} \big (A _ {F (p)} \big). \] This tensor field acts on vectors $v _ { 1 } , \dotsc , v _ { k } \in T _ { p } M$ by \[ (F ^ {*} A) _ {p} (v _ {1}, \dots , v _ {k}) = A _ {F (p)} \left(d F _ {p} (v _ {1}), \dots , d F _ {p} (v _ {k})\right). \] Proposition 12.25 (Properties of Tensor Pullbacks). Suppose $F \colon M \to N$

Proposition 12.25

FC08-C12-U039 · Ch. 12, § Pullbacks of Tensor Fields; source L9519 · not formalized

Proposition 12.25 (Properties of Tensor Pullbacks). Suppose and $G \colon N \to P$ are smooth maps, A and B are covariant tensor fields on N , and f is a real-valued function on N . (a) $F ^ { * } ( f B ) = ( f \circ F ) F ^ { * } B$ F ^ { * } A F ^ { * } B .$ (c) $F ^ { * } ( A + B ) = F ^ { * } A + F (d) F B is a (continuous) tensor field, and is smooth if B is smooth. (e) $( G \circ F ) ^ { * } B = F ^ { * } ( G ^ { * } B )$ (f) $( \mathrm { I d } _ { N } ) ^ { * } B = B$

Corollary 12.28

FC08-C12-U040 · Ch. 12, § Pullbacks of Tensor Fields; source L9541 · not formalized

(Pullback of a Tensor Field). Let $M = \{(r,\theta) : r > 0,\ |\theta| < \pi/2\}$ and $N = \{(x,y) : x > 0\}$, and let $F \colon M \to \mathbb{R}^{2}$ be the smooth map $F(r,\theta) = (r\cos\theta,\ r\sin\theta)$. The pullback of the tensor field $A = x^{-2}\,dy \otimes dy$ is computed by substituting the coordinate functions of $F$ and expanding.

Example 12.29

FC08-C12-U041 · Ch. 12, § Pullbacks of Tensor Fields; source L9549 · not formalized

of a Tensor Field). Let $M = \{ ( r , \theta ) : r > 0 , | \theta | < \pi / 2 \}$ and $N = \{ ( x , y ) : x > 0 \}$ , and let $F \colon M \to \mathbb { R } ^ { 2 }$ be the smooth map $F ( r , \theta ) =$ .r cos ; r sin /. The pullback of the tensor field $A = x ^ { - 2 } d y \otimes d y$ by F can be computed easily by substituting $x = r \cos \theta , y = r$ sin and simplifying: \[ \begin{array}{l} F ^ {*} A = (r \cos \theta) ^ {- 2} d (r \sin \theta) \otimes d (r \sin \theta) \\ \qquad = (r \cos \theta) ^ {- 2} (\sin \theta d r + r \cos \theta d \theta) \otimes (\sin \theta d r + r \cos \theta d \theta) \\ \qquad = r ^ {- 2} \tan^ {2} \theta d r \otimes d r + r ^ {- 1} \tan \theta (d \theta \otimes d r + d r \otimes d \theta) + d \theta \otimes d \theta . \end{array} \] In general, there is neither a pushforward nor a pullback operation for mixed tensor fields. However, in the special case of a diffeomorphism, tensor fields of any variance can be pushed forward and pulled back at will (s

Definition/convention — source terminology/construction

FC08-C12-U042 · Ch. 12, § Lie Derivatives of Tensor Fields; source L9561 · after FC08-C09-U049 · not formalized

Suppose M is a smooth manifold, V is a smooth vector field on M; and θ is its flow. (For simplicity, we discuss only the case ∂ M = emptyset here, but these definitions and results carry over essentially unchanged to manifolds with boundary as long as V is tangent to the boundary, so that its flow exists by Theorem 9.34.) For any p ∈ M; if t is sufficiently close to zero, then θ _t is a diffeomorphism from a neighborhood of p to a neighborhood of θ _t ( p ) , so d ( θ _t ) _p * pulls back tensors at θ _t ( p ) to ones at p by the formula \[ d(\theta_{t})^{*}_{p}\big(A_{\theta_{t}(p)}\big)(v_{1},\dots,v_{k}) = A_{\theta_{t}(p)}\big(d(\theta_{t})_{p}(v_{1}),\dots,d(\theta_{t})_{p}(v_{k})\big), \] which is the value at $p$ of the pullback tensor field $\theta_{t}^{*}A$.

Not formalized. none; no complete checked declaration under strict bundle semantics — No checked manifold tensor-field Lie-derivative API exists at P or current H. These rows require the absent tensor-field/pullback layer plus the C09 maximal/local-flow machinery and, for formulas involving vector fields/brackets, the C03/C08 tangent-model bridge. Generic flow, bracket, and algebraic tensor ingredients do not own the source statements. Strict whole-row semantics reject proper subsets, unproved equivalences, stronger hypotheses, truncated-source reconstruction, and substantive assembly from generic ingredients.

Lemma 12.30

FC08-C12-U043 · Ch. 12, § Lie Derivatives of Tensor Fields; source L9579 · not formalized

Lemma 12.30. With M; V , and A as above, the derivative in (12.8) exists for every $p \in M$ and defines $\mathcal { L } _ { V } A$ as a smooth tensor field se of “formal linear combinations.” Let S be a set.

Proposition 12.32

FC08-C12-U044 · Ch. 12, § Lie Derivatives of Tensor Fields; source L9586 · not formalized

Proposition 12.32. Let M be a smooth manifold and let $V \in { \mathfrak { X } } ( M )$ . Suppose f is a smooth real-valued function (regarded as a 0-tensor field) on M; and A; B are smooth covariant tensor fields on M . (a) $\mathcal { L } _ { V } f = V f$ (b) $\displaystyle \mathcal { L } _ { V } ( f A ) = ( \mathcal { L } _ { V } f ) A + f \mathcal { L } _ { V } A .$ (c) ${ \mathcal { L } } _ { V } ( A \otimes B ) = ( { \mathcal { L } } _ { V } A ) \otimes B + A \otimes { \mathcal { L } } _ { V } B .$ (d) $I f X _ { 1 } , \ldots , X _ { k }$ are smooth vector fields and A is a smooth k-tensor field, \[ \begin{array}{c} \mathcal {L} _ {V} \big (A (X _ {1}, \ldots , X _ {k}) \big) = (\mathcal {L} _ {V} A) (X _ {1}, \ldots , X _ {k}) + A (\mathcal {L} _ {V} X _ {1}, \ldots , X _ {k}) \\ + \dots + A (X _ {1}, \ldots , \mathcal {L} _ {V} X _ {k}). \end{array}\tag{12.9} \]

Corollary 12.33

FC08-C12-U045 · Ch. 12, § Lie Derivatives of Tensor Fields; source L9618 · not formalized

Corollary 12.33. If V is a smooth vector field and A is a smooth covariant k-tensor field, then for any smooth vector $X _ { 1 } , \ldots , X _ { k }$ \[ \begin{array}{c} (\mathcal {L} _ {V} A) (X _ {1}, \ldots , X _ {k}) = V \big (A (X _ {1}, \ldots , X _ {k}) \big) - A \big ([ V, X _ {1} ], X _ {2}, \ldots , X _ {k} \big) \\ - \dots - A \big (X _ {1}, \ldots , X _ {k - 1}, [ V, X _ {k} ] \big). \end{array}\tag{12.10} \]

Corollary 12.34

FC08-C12-U046 · Ch. 12, § Lie Derivatives of Tensor Fields; source L9626 · not formalized

If $f \in C^{\infty}(M)$, then $\mathcal{L}_{V}(df) = d(\mathcal{L}_{V}f)$.

Example 12.35

FC08-C12-U047 · Ch. 12, § Lie Derivatives of Tensor Fields; source L9636 · after FC08-C09-U058, FC08-C09-U056 · not formalized

For a smooth covariant 2-tensor field $A$ and a smooth vector field $V$, since $\mathcal{L}_{V}dx^{i} = d(\mathcal{L}_{V}x^{i}) = d(Vx^{i}) = dV^{i}$, the Lie derivative in smooth local coordinates is \[ \mathcal{L}_{V}A = \left(VA_{ij} + A_{kj}\frac{\partial V^{k}}{\partial x^{i}} + A_{ik}\frac{\partial V^{k}}{\partial x^{j}}\right) dx^{i} \otimes dx^{j}. \] A smooth tensor field $A$ is invariant under a flow $\theta$ if each $\theta_{t}$ pulls $A$ back to itself wherever defined, that is \[ d(\theta_{t})^{*}_{p}\left(A_{\theta_{t}(p)}\right) = A_{p} \tag{12.11} \] for all $(t,p)$ in the domain of $\theta$; for a global flow this is $\theta_{t}^{*}A = A$ for all $t \in \mathbb{R}$.

Proposition 12.36

FC08-C12-U048 · Ch. 12, § Lie Derivatives of Tensor Fields; source L9652 · not formalized

Proposition 12.36. Suppose M is a smooth manifold with or without boundary and { } ( M ) . I f M = $ , assume in addition that V is tangent to @M . Let be the flow of V . For any smooth covariant tensor field A and any $ \[ \left. \frac {d}{d t} \right| _ {t = t _ {0}} \left(\theta_ {t} ^ {*} A\right) _ {p} = \left(\theta_ {t _ {0}} ^ {*} (\mathcal {L} _ {V} A)\right) _ {p}.\tag{12.12} \]

Theorem 12.37

FC08-C12-U049 · Ch. 12, § Lie Derivatives of Tensor Fields; source L9670 · not formalized

Let $M$ be a smooth manifold and $V \in \mathfrak{X}(M)$. A smooth covariant tensor field $A$ is invariant under the flow of $V$ if and only if $\mathcal{L}_{V}A = 0$.