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

FC08 — Lee, Introduction to Smooth Manifolds.

This chapter contains 19 definitions, 3 theorems, 20 propositions, 1 lemma, 3 corollaries, 10 examples, 2 constructions, 9 conventions and 1 other statements.

Of the 68 statements checked against Lean, 9 are formalized somewhere and 59 are not.

Status	Statements	Share	What it means
not formalized	59	87%	A documented search found no Lean statement of it anywhere.
in Mathlib	9	13%	Mathlib states and proves it.
checked in total	68

Which versions of Lean and Mathlib were searched

Canonical source block: FC08 Lee, Chapter 11, FC08-C11-U001–FC08-C11-U068, exactly 68 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 C11 owner survived strict whole-row checking.
C11 has 9 pinned mathlib rows and 59 dated unmatched rows. Positive rows are: U001, U002, U003, U004, U005, U007, U009, U035, U065.
The pure finite-dimensional dual-space block has direct owners. Module.Dual, Basis.dualBasis, LinearMap.dualMap, the identity/composition laws, and Module.evalEquiv match U001–U005 and U007. /tmp/fc08-c11-witness.lean compiled these specializations at P. U006 remains unmatched because no contravariant dual functor on the category of real vector spaces/modules matching Lee’s categorical statement was found.
C11 preserves the tangent-model contract established in promoted C03. Lee’s TₚM is the point-derivation model, so U009 can be represented exactly as Module.Dual ℝ (PointDerivation I p). The same choice makes U035 a short exact assembly: dualize fdifferential F p with LinearMap.dualMap. The witness compiles (dFₚ)⁎ ω v = ω (dFₚ v) at the pin. This does not assert any unproved bridge to Mathlib’s standard TangentSpace.
No general manifold cotangent bundle or bundled manifold 1-form/covector-field theory was found at P or H. Analysis/Calculus/DifferentialForm explicitly represents forms on normed vector spaces, and Geometry/Manifold/MFDeriv/NormedSpace represents scalar differentials using the separate standard TangentSpace. Exact P/H searches found no CotangentBundle/manifold 1-form layer. Therefore U011–U025 and the global pullback/smoothness rows U036–U042 are not inferred from vector-space or standard-tangent infrastructure.
The differential-of-functions block U026–U033 is likewise not silently transferred. mvfderiv is excellent standard-tangent infrastructure, while DerivationBundle.fdifferential stays within point derivations and does not package df as a cotangent field. Without the missing PointDerivation ≃ TangentSpace theorem or a derivation-model cotangent bundle, the source rows remain unmatched.
Pinned Mathlib does contain a substantial curve-integral theory: MeasureTheory/Integral/CurveIntegral/Basic.lean defines curveIntegral for 1-forms on normed vector spaces and proves reversal, concatenation, linearity, and the ordinary-integral formula. CurveIntegral/Poincare.lean proves homotopy invariance and a Poincaré lemma for convex subsets. These are recorded as adjacent evidence only: Lee’s U043–U064 are stated for cotangent fields and piecewise-smooth curves on arbitrary manifolds, an interface absent from P/H.
U065 is independent and exact: StarConvex ℝ c U plus c ∈ U is precisely Lee’s star-shaped condition, with starConvex_iff_segment_subset giving the source formulation. The C11 witness compiles the equivalence.
U066 is deliberately not promoted from the pinned Poincaré theorem. Mathlib assumes Convex ℝ U, while Lee assumes only star-shaped; convexity is strictly stronger. No star-shaped Poincaré theorem was found at P, current H, project source, or targeted indexed Lean searches. U067 then also lacks the manifold closed-1-form layer needed for Lee’s local-exactness corollary.
Submanifold restriction U041–U042 additionally inherits the promoted C05 blocker: P/H still lack Lee’s general embedded/immersed submanifold abstraction. No reconstruction from inclusions and linear restrictions was used.
N=2026-09-07 marks dated unmatched decisions after the prescribed search layers. Strict whole-row semantics apply uniformly.

Definition/convention — dual space of V

FC08-C11-U001 · Ch. 11, § Covectors; source L7805 · in Mathlib

Let V be a finite-dimensional vector space. (As usual, all of our vector spaces are assumed to be real.) We define a covector on V to be a real-valued linear functional on V , that is, a linear map ! $V \mathbb { R }$ . The space of all covectors on V is itself a real vector space under the obvious operations of pointwise addition and scalar multiplication. It is denoted by $V ^ { * }$ and called the dual space m Corollary 10.21 that the natural coordinate chart ${ \widetilde { \varphi } } = ( \varphi \times \operatorname { I d } _ { \mathbb { R } ^ { n } } )$ ˚ belongs to the given smooth structure.

Formalized. Mathlib/LinearAlgebra/Dual/Defs.lean::Module.Dual — Module.Dual ℝ V is exactly the real vector space of linear functionals V →ₗ[ℝ] ℝ, i.e. Lee’s covectors and dual space.

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

Proposition 11.1

FC08-C11-U002 · Ch. 11, § Covectors; source L7809 · in Mathlib

Proposition 11.1. Let V be a finite-dimensional vector space. Given any basis $( E _ { 1 } , \ldots , E _ { n } )$ for V , let $\varepsilon ^ { 1 } , \ldots , \varepsilon ^ { n } \in V ^ { * }$ be the covectors defined by \[ \varepsilon^ {i} (E _ {j}) = \delta_ {j} ^ {i}, \] where $\delta _ { j } ^ { i }$ is the Kronecker delta symbol defined by (4.4). Then $\left( \varepsilon ^ { 1 } , \ldots , \varepsilon ^ { n } \right)$ is a basis for $V ^ { * }$ , called the dual basis to $( E _ { j } )$ . Therefore, dim $V^{*} = \dim V$.

Formalized. Mathlib/LinearAlgebra/Dual/Basis.lean::Basis.dualBasis, Basis.dualBasis_apply_self; Mathlib/LinearAlgebra/Dual/Lemmas.lean::Subspace.dual_finrank_eq — b.dualBasis is a basis of the dual with b.dualBasis i (b j)=δᵢⱼ; finite-dimensional duality gives equal finrank. This is Lee’s Proposition 11.1.

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

Definition/convention — standard dual basis

FC08-C11-U003 · Ch. 11, § Covectors; source L7819 · in Mathlib

Proposition 11.1. For example, we can apply this to the standard basis $( e _ { 1 } , \ldots , e _ { n } )$ for $\mathbb { R } ^ { n }$ . The dual basis is denoted by $\left( e ^ { 1 } , \ldots , e ^ { n } \right)$ (note the upper indices), and is called the standard dual basis. These basis covectors are the linear functionals on $\mathbb { R } ^ { n }$ given by \[ e ^ {i} (v) = e ^ {i} \left(v ^ {1}, \dots , v ^ {n}\right) = v ^ {i}. \]

Formalized. Mathlib/LinearAlgebra/Dual/Basis.lean::Basis.dualBasis, Basis.dualBasis_apply — Specializing Basis.dualBasis to the standard basis of ℝ^n, dualBasis_apply identifies each dual basis vector with the corresponding coordinate functional, exactly Lee’s standard dual basis.

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

Definition/convention — dual map

FC08-C11-U004 · Ch. 11, § Covectors; source L7851 · in Mathlib

Suppose V and W are vector spaces and A $V W$ is a linear map. We define a linear map $A ^ { * } \colon W ^ { * } \to V ^ { * }$ , called the dual map or transpose of A, by \[ (A ^ {*} \omega) (v) = \omega (A v) \quad \text { for } \omega \in W ^ {*}, v \in V. \]

Formalized. Mathlib/LinearAlgebra/Dual/Defs.lean::LinearMap.dualMap, LinearMap.dualMap_apply — A.dualMap : Dual ℝ W →ₗ[ℝ] Dual ℝ V is defined by precomposition and satisfies A.dualMap ω v = ω (A v), exactly Lee’s dual map/transpose.

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

Proposition 11.4

FC08-C11-U005 · Ch. 11, § Covectors; source L7859 · in Mathlib

Proposition 11.4. The dual map satisfies the following properties: (a) $( A \circ B ) ^ { * } = B ^ { * } \circ A ^ { * }$ (b) $( \operatorname { I d } _ { V } ) ^ { * } \colon V ^ { * } \to V ^ { * }$ is the identity map of $V^{*}$.

Formalized. Mathlib/LinearAlgebra/Dual/Defs.lean::LinearMap.dualMap_comp_dualMap, LinearMap.dualMap_id — These declarations are precisely contravariance under composition and preservation of the identity, the two clauses of Proposition 11.4.

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

Corollary 11.6

FC08-C11-U006 · Ch. 11, § Covectors; source L7867 · not formalized

Corollary 11.6. The assignment that sends a vector space to its dual space and a linear map to its dual map is a contravariant functor from the category is a smooth bundle homomorphism covering the inclusion of S into M .

Not formalized. none; no complete checked declaration under strict bundle semantics — The algebraic identity and composition laws for dual maps are formalized (U004–U005), but targeted project/P/H searches found no contravariant dual functor on the category of real vector spaces/modules matching Lee’s categorical row. Generic rigid-monoidal dual functors are a different interface. Strict whole-row semantics reject proper subsets, stronger hypotheses, unbridged tangent models, and reconstruction of substantive source theorems from adjacent ingredients.

Proposition 11.8

FC08-C11-U007 · Ch. 11, § Covectors; source L7881 · in Mathlib

Proposition 11.8. For any finite-dimensional vector space V , the map $\xi \colon V \to V ^ { * * }$ is an isomorphism.

Formalized. Mathlib/LinearAlgebra/Dual/Defs.lean::Module.evalEquiv; Mathlib/LinearAlgebra/Dual/Lemmas.lean::FiniteDimensional.instIsReflexive — For finite-dimensional real vector spaces, Module.evalEquiv ℝ V is the canonical linear equivalence V ≃ₗ[ℝ] Dual ℝ (Dual ℝ V) sending v to evaluation at v, exactly Lee’s double-dual map.

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

Convention/notation — vector v

FC08-C11-U008 · Ch. 11, § Covectors; source L7891 · after FC08-C11-U007 · not formalized

Because of Proposition 11.8, the real number $\omega ( v )$ obtained by applying a covector ! to a vector v is sometimes denoted by either of the more symmetric-looking notations $\langle \omega , v \rangle$ and $\langle v , \omega \rangle$ ; both expressions can be thought of either as the action of the covector $\omega \in V ^ { * }$ on the vector $v \in V$ , or as the action of the linear functional $\xi ( v ) \in V ^ { * * }$ on the element $\omega \in V ^ { * }$ . There should be no cause for confusion with the use of the same angle bracket notation for inner products: whenever one of the arguments is a vector and the other a covector, the notation $\langle \omega , v \rangle$ is always to be interpreted as the natural pairing between vectors and covectors, not as an inner product. We typically omit any mention of the map $\xi$ , and think of $v \in V$ either as a vector or as a linear functional on $V ^ { * }$ , depending on the context.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has the evaluation pairing and double-dual equivalence, but no checked interface owns Lee’s source-level symmetric angle-bracket notation/convention. The mathematical operation is adjacent rather than a distinct formalized row. Strict whole-row semantics reject proper subsets, stronger hypotheses, unbridged tangent models, and reconstruction of substantive source theorems from adjacent ingredients.

Definition/convention — cotangent space at p

FC08-C11-U009 · Ch. 11, § Tangent Covectors on Manifolds; source L7897 · in Mathlib

Let $M$ be a smooth manifold with or without boundary. For each $p \in M$ the cotangent space at $p$, denoted $T^{*}_{p}M$, is the dual space to $T_{p}M$.

Formalized. Mathlib/LinearAlgebra/Dual/Defs.lean::Module.Dual; Mathlib/Geometry/Manifold/DerivationBundle.lean::PointDerivation — Lee’s TₚM in this source is the point-derivation model. Therefore Module.Dual ℝ (PointDerivation I p) is exactly his cotangent space Tₚ*M. /tmp/fc08-c11-witness.lean typechecks this specialization at P.

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

Definition/convention — tangent covectors at p

FC08-C11-U010 · Ch. 11, § Tangent Covectors on Manifolds; source L7903 · not formalized

Elements of $T _ { p } ^ { * } M$ are called tangent covectors at p, or just covectors at $p$.

Not formalized. none; no complete checked declaration under strict bundle semantics — Module.Dual ℝ (PointDerivation I p) realizes the cotangent space itself (U009), but no named terminology/interface for “tangent covector/covector at p” is present. This row is terminology only and is not separately owned. Strict whole-row semantics reject proper subsets, stronger hypotheses, unbridged tangent models, and reconstruction of substantive source theorems from adjacent ingredients.

Convention/notation — source terminology/construction

FC08-C11-U011 · Ch. 11, § Tangent Covectors on Manifolds; source L7905 · not formalized

Given smooth local coordinates $\left( x ^ { i } \right)$ on an open subset $U \subseteq M$ ; for each $p \in U$ the coordinate basis $\left( \partial / \partial x ^ { i } | _ { p } \right)$ gives rise to a dual basis for $T _ { p } ^ { * } M ,$ ; which we denote for the moment by $\left( \lambda ^ { i } | _ { p } \right)$ . (In a short while, we will come up with a better notation.) Any covector $\omega \in T _ { p } ^ { * } M$ can thus be written uniquely as $\omega = \omega _ { i } \lambda ^ { i } | _ { p }$ , where \[ \omega_ {i} = \omega \left(\frac {\partial}{\partial x ^ {i}} \Big | _ {p}\right). \]

Not formalized. none; no complete checked declaration under strict bundle semantics — P/H have no manifold cotangent-bundle or bundled manifold 1-form/covector-field layer. DifferentialForm is explicitly a normed-vector-space theory, while manifold mvfderiv uses the separate standard TangentSpace model. Thus coordinate covectors, the cotangent bundle, covector fields/coframes, their smoothness criteria, and the C^∞(M)-module of covector fields are not available as complete interfaces. Strict whole-row semantics reject proper subsets, stronger hypotheses, unbridged tangent models, and reconstruction of substantive source theorems from adjacent ingredients.

Definition/convention — contravariant vectors

FC08-C11-U012 · Ch. 11, § Tangent Covectors on Manifolds; source L7937 · not formalized

_ {j}. \[ Since the transformation law (11.4) for the coordinate partial derivatives follows directly from the chain rule, it can be thought of as fundamental. Thus it became customary to call tangent covectors covariant vectors because their components transform in the same way as (“vary with”) the coordinate partial derivatives, with the Jacobian matrix $\left( { \partial \widetilde { x } ^ { j } } / { \partial x ^ { i } } \right)$ multiplying the objects associated with the “new” coordinates $\left( \widetilde { x } ^ { j } \right)$ to obtain those associated with the “old” coordinates $\left( x ^ { i } \right)$ . Analogously, tangent vectors were called contravariant vectors, because their components transform in the opposite way. (Remember, it was the component n-tuples that were thought of as the objects of interest.) Admittedly, these terms do not make a lot of sense, but by now they are well entrenched, and we will see them again in Chapter 12. Note that this use of the terms covariant and contravariant has nothing to do with the covariant and contravariant functors of category theory! ## Covector Fields For any smooth manifold M with or without boundary, the disjoint union \]

Convention/notation — cotangent bundle of M

FC08-C11-U013 · Ch. 11, § Covector Fields; source L7941 · not formalized

For any smooth manifold $M$ with or without boundary, the disjoint union $T^{*}M = \coprod_{p \in M} T^{*}_{p}M$ is the cotangent bundle of $M$, with natural projection $\pi \colon T^{*}M \to M$ sending $\omega \in T^{*}_{p}M$ to $p$. Given smooth local coordinates $(x^{i})$ on an open subset $U \subseteq M$, the basis for $T^{*}_{p}M$ dual to $\left(\left.\partial/\partial x^{i}\right|_{p}\right)$ is written $\left(\left.\lambda^{i}\right|_{p}\right)$, defining $n$ maps $\lambda^{1},\dots,\lambda^{n} \colon U \to T^{*}M$, the coordinate covector fields.

Proposition 11.9

FC08-C11-U014 · Ch. 11, § Covector Fields; source L7949 · not formalized

Proposition 11.9 (The Cotangent Bundle as a Vector Bundle). Let M be a smooth n-manifold with or without boundary. With its standard projection map and the natural vector space structure on each fiber, the cotangent bundle $T ^ { * } M$ has a unique topology and smooth structure making it into a smooth rank-n vector bundle over M for which all coordinate covector fields are smooth local sections.

Comparison/convention — source terminology/construction

FC08-C11-U015 · Ch. 11, § Covector Fields; source L7967 · after FC08-C10-U030 · not formalized

Smooth local coordinates for $M$ yield smooth local coordinates for its cotangent bundle. If $(x^{i})$ are smooth coordinates on an open subset $U \subseteq M$, Corollary 10.21 shows that the map from $\pi^{-1}(U)$ to $\mathbb{R}^{2n}$ given by \[ \left.\xi_{i}\lambda^{i}\right|_{p} \mapsto (x^{1}(p),\dots,x^{n}(p),\xi_{1},\dots,\xi_{n}) \] is a smooth chart for $T^{*}M$; $(x^{i},\xi_{i})$ are the natural coordinates for $T^{*}M$ associated with $(x^{i})$. Here coordinate functions cannot all carry upper indices, since the fiber coordinates $\xi_{i}$ must have lower ones, but each summed index still appears once up and once down.

Convention/notation — covector field

FC08-C11-U016 · Ch. 11, § Covector Fields; source L7975 · not formalized

superscript and once as a subscript.) A (local or global) section of $T ^ { * } M$ is called a covector field or a (differential) $\pmb { I } { \pmb f o r m }$ . (The reason for the latter terminology will become clear in Chapter 14, when we define differential $k { \mathrm { - f o r m s } }$ for $k > 1 . )$ Like sections of other bundles, covector fields without further qualification are assumed to be merely continuous; when we make different assumptions, we use the terms rough covector field and smooth covector field with the obvious meanings. As we did with vector fields, we write the value of a covector field $\omega$ at a point $p \in M$ as $\omega _ { p }$ instead of $\omega ( p )$ to avoid conflict with the notation for the action of a covector on a vector. If ! itself has subscripts or superscripts, we usually use the notation $\omega | _ { p }$ instead. In smooth local coordinates on an open subset $U \subseteq M$ ; a (rough) covector field $\omega$ can be written in terms of the coordinate covector fields $( \lambda ^ { i } )$ as $\omega = \omega _ { i } \lambda ^ { i }$ for n functions $\omega _ { i } \colon U \mathbb { R }$ called the component functions of !. characterized by \[ \omega_ {i} (p) = \omega_ {p} \left(\frac {\partial}{\partial x ^ {i}} \Big | _ {p}\right). \]

Convention/notation — source terminology/construction

FC08-C11-U017 · Ch. 11, § Covector Fields; source L7987 · not formalized

If we write $\omega = \omega _ { i } \lambda ^ { i }$ and $X = X ^ { j } \partial / \partial x ^ { j }$ in terms of local coordinates, then $\omega ( X )$ has the local coordinate representation $\omega ( X ) = \omega _ { i } X ^ { i }$

Proposition 11.11

FC08-C11-U018 · Ch. 11, § Covector Fields; source L7991 · not formalized

Proposition 11.11 (Smoothness Criteria for Covector Fields). Let M be a smooth manifold with or without boundary, and let ! $M \to T ^ { * } M$ be a rough covector field. The following are equivalent: (a) ! is smooth. (b) In every smooth coordinate chart, the component functions of ! are smooth. (c) Each point of M is contained in some coordinate chart in which ! has smooth component functions. (d) For every smooth vector field $X \in { \mathfrak { X } } ( M )$ , the function !.X / is smooth on M . (e) For every open subset $U \subseteq M$ and every smooth vector field X on U , the function $\omega ( X ) \colon U \to \mathbb { R }$

Definition/convention — global coframe

FC08-C11-U019 · Ch. 11, § Coframes; source L8009 · not formalized

Let M be a smooth manifold with or without boundary, and let $U \subseteq M$ be an open subset. A local coframe for M over U is an ordered n-tuple of covector fields $\left( \varepsilon ^ { 1 } , \ldots , \varepsilon ^ { n } \right)$ defined on U such that $\left( \varepsilon ^ { i } | _ { p } \right)$ forms a basis for $T _ { p } ^ { * } M$ at each point $p \in U . \operatorname { I f } U = M$ ; it is called a global coframe. (A local coframe for M is just a local frame for the vector bundle $T ^ { * } M$ ; in the terminology of Chapter

Example 11.13

FC08-C11-U020 · Ch. 11, § Coframes; source L8011 · after FC08-C11-U018 · not formalized

terminology of Chapter 10.) Example 11.13 (Coordinate Coframes). For any smooth chart $\left( U , \left( x ^ { i } \right) \right)$ , the coordinate covector fields $\left( \lambda ^ { i } \right)$ defined above constitute a local coframe over U , called a coordinate coframe. By Proposition 11.11(c), every coordinate frame is smooth, because its component functions in the give $F \colon E \to E ^ { \prime }$ is a bundle homomorphism over M .

Definition/convention — dual coframe and dual frame

FC08-C11-U021 · Ch. 11, § Coframes; source L8013 · not formalized

a local frame $( E _ { 1 } , \ldots , E _ { n } )$ for TM over an open subset U , there is a uniquely determined (rough) local coframe $\left( \varepsilon ^ { 1 } , \ldots , \varepsilon ^ { n } \right)$ over U such that $\left( \varepsilon ^ { i } | _ { p } \right)$ is the dual basis to $( E _ { i } | _ { p } )$ for each $p \in U$ , or equivalently $\varepsilon ^ { i } ( E _ { j } ) = \delta _ { j } ^ { i }$ . This coframe is called the coframe dual to $( E _ { i } )$ . Conversely, if we start with a local coframe $\left( \varepsilon ^ { i } \right)$ over an open subset $U \subseteq M$ ; there is a uniquely determined local frame $( E _ { i } )$ , called the frame dual to $( \pmb \varepsilon ^ { i } )$ , determined by $\varepsilon ^ { i } ( \bar { E } _ { j } ) \overset { \cdot } { = } \delta _ { i } ^ { i }$ . For example, in a smooth chart, the coordinate frame $( \partial / \partial x ^ { i } )$ / and the coordinate coframe $\left( \lambda ^ { i } \right)$ are dual to each other. Lemma 11.14. Let M be a smooth manifold with or without boundary. $H ( E _ { i } )$ is a rough local frame over an open subset $U \subseteq M$ and $\left( \varepsilon ^ { i } \right)$ is its dual coframe, then $( E _ { i } )$ is smooth if and only $i f \left( \varepsilon ^ { i } \right)$

Lemma 11.14

FC08-C11-U022 · Ch. 11, § Coframes; source L8017 · not formalized

Lemma 11.14. Let M be a smooth manifold with or without boundary. $H ( E _ { i } )$ is a rough local frame over an open subset $U \subseteq M$ and $\left( \varepsilon ^ { i } \right)$ is its dual coframe, then $( E _ { i } )$ is smooth if and only $i f \left( \varepsilon ^ { i } \right)$ is smooth. Proof. It suffices to show that for each $p \in U$ , the frame is smooth near $p$ if and only if its dual coframe is.

Definition/convention — component functions of

FC08-C11-U023 · Ch. 11, § Coframes; source L8027 · not formalized

Given a local coframe $(\varepsilon^{i})$ over an open subset $U \subseteq M$, every rough covector field $\omega$ on $U$ can be written $\omega = \omega_{i}\varepsilon^{i}$ for functions $\omega_{1},\dots,\omega_{n} \colon U \to \mathbb{R}$, the component functions of $\omega$ with respect to that coframe, determined by $\omega_{i} = \omega(E_{i})$ where $(E_{i})$ is the dual frame.

Proposition 11.15

FC08-C11-U024 · Ch. 11, § Coframes; source L8029 · not formalized

Proposition 11.15 (Coframe Criterion for Smoothness of Covector Fields). Let M be a smooth manifold with or without boundary, and let ! be a rough covector field on M . $H \left( \varepsilon ^ { i } \right)$ is a smooth coframe on an open subset $U \subseteq M$ ; then ! is smooth on U if and only if its component functions with respect to $\left( \varepsilon ^ { i } \right)$ are smooth. Exercise 11.16. Prove the preceding proposition. We denote in a neighborhood of each point, Ker $F$ is a smooth subbundle of $E$ The next proposition illustrates another method for constructing interesting subbundles of the tangent bundle over submanifolds of $\mathbb { R } ^ { n }$ Lemma 10.35 (Orthogonal Complement Bundles).

Convention/notation — source terminology/construction

FC08-C11-U025 · Ch. 11, § Coframes; source L8033 · not formalized

Covector fields can be multiplied by smooth functions: for $f \in C^{\infty}(M)$ and $\omega \in \mathfrak{X}^{*}(M)$, the covector field $f\omega$ is defined by \[ (f\omega)_{p} = f(p)\,\omega_{p}. \tag{11.8} \] Being the space of smooth sections of a vector bundle, $\mathfrak{X}^{*}(M)$ is a module over $C^{\infty}(M)$.

Convention/notation — source terminology/construction

FC08-C11-U026 · Ch. 11, § The Differential of a Function; source L8050 · not formalized

In elementary calculus, the gradient of a smooth real-valued function f on ℝ ^n is defined as the vector field whose components are the partial derivatives of f . In our notation, this would read \[ \operatorname{grad} f = \sum_{i=1}^{n} \frac{\partial f}{\partial x^{i}}\frac{\partial}{\partial x^{i}}. \tag{11.9} \] In this form the gradient is not coordinate-independent; on a Riemannian manifold it is defined instead by raising the index of $df$.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has standard-tangent mvfderiv and extensive scalar calculus, but Lee’s tangent vectors in this corpus are point derivations and no checked PointDerivation ≃ TangentSpace bridge exists at P/H. DerivationBundle.fdifferential maps point derivations to point derivations rather than bundling df as a cotangent field, so the differential-of-a-function rows cannot be transferred wholesale. Strict whole-row semantics reject proper subsets, stronger hypotheses, unbridged tangent models, and reconstruction of substantive source theorems from adjacent ingredients.

Definition/convention — differential of f

FC08-C11-U027 · Ch. 11, § The Differential of a Function; source L8072 · not formalized

Let $f$ be a smooth real-valued function on a smooth manifold M with or without boundary. (As usual, all of this discussion applies to functions defined on an open subset $U \subseteq M$ ; simply by replacing M with $U$ throughout.) We define a covector field $d f$ , called the differential of $f$ , by \[ d f _ {p} (v) = v f \quad \mathrm{for} v \in T _ {p} M. \]

Proposition 11.18

FC08-C11-U028 · Ch. 11, § The Differential of a Function; source L8080 · not formalized

Proposition 11.18. The differential of a smooth function is a smooth covector field.

Convention/notation — source terminology/construction

FC08-C11-U029 · Ch. 11, § The Differential of a Function; source L8122 · not formalized

Thus, we have recovered the familiar classical expression for the differential of a function $f$ in coordinates. Henceforth, we abandon the notation $\lambda ^ { i }$ for the coordinate coframe, and use $d x ^ { i }$ instead.

Example 11.19

FC08-C11-U030 · Ch. 11, § The Differential of a Function; source L8124 · not formalized

Example 11.19. If $f ( x , y ) = x ^ { 2 } y$ cos x on $\mathbb { R } ^ { 2 }$ , then df is given by the formula \[ \begin{array}{c} d f = \frac {\partial (x ^ {2} y \cos x)}{\partial x} d x + \frac {\partial (x ^ {2} y \cos x)}{\partial y} d y \\ = (2 x y \cos x - x ^ {2} y \sin x) d x + x ^ {2} \cos x d y. \end{array} \]

Proposition 11.20

FC08-C11-U031 · Ch. 11, § The Differential of a Function; source L8130 · not formalized

(Properties of the Differential). Let $M$ be a smooth manifold with or without boundary and let $f, g \in C^{\infty}(M)$. (a) For constants $a$ and $b$, $d(af+bg) = a\,df + b\,dg$. (b) $d(fg) = f\,dg + g\,df$. (c) $d(f/g) = (g\,df - f\,dg)/g^{2}$ on the set where $g \neq 0$. (d) If $J \subseteq \mathbb{R}$ is an interval containing the image of $f$ and $h \colon J \to \mathbb{R}$ is smooth, then $d(h \circ f) = (h' \circ f)\,df$. (e) If $f$ is constant, then $df = 0$.

Proposition 11.22

FC08-C11-U032 · Ch. 11, § The Differential of a Function; source L8146 · not formalized

Proposition 11.22 (Functions with Vanishing Differentials). If f is a smooth real-valued function on a smooth manifold M with or without boundary, then $d f =$ 0 if and only if f is constant on each component of M .

Proposition 11.23

FC08-C11-U033 · Ch. 11, § The Differential of a Function; source L8163 · not formalized

Proposition 11.23 (Derivative of a Function Along a Curve). Suppose M is a smooth manifold with or without boundary, $\gamma \colon J \to M$ is a smooth curve, and $f \colon M \to \mathbb { R }$ is a smooth function. Then the derivative of the real-valued function $f \circ \gamma \colon J \mathbb { R }$ is given by \[ (f \circ \gamma) ^ {\prime} (t) = d f _ {\gamma (t)} \big (\gamma^ {\prime} (t) \big).\tag{11.12} \]

Definition/convention — differential

FC08-C11-U034 · Ch. 11, § Pullbacks of Covector Fields; source L8188 · not formalized

As we have seen, a smooth map yields a linear map on tangent vectors called the differential. Dualizing this leads to a linear map on covectors going in the opposite direction.

Not formalized. none; no complete checked declaration under strict bundle semantics — The ingredients “differential” and “dual map” exist separately, and U035 compiles their exact pointwise composite, but this prose transition row has no independent checked construction beyond those adjacent notions. Strict whole-row semantics reject proper subsets, stronger hypotheses, unbridged tangent models, and reconstruction of substantive source theorems from adjacent ingredients.

Construction/definition — the (pointwise) pullback by F at p

FC08-C11-U035 · Ch. 11, § Pullbacks of Covector Fields; source L8190 · in Mathlib

Let $F \colon M \to N$ be a smooth map between smooth manifolds with or without boundary and let $p \in M$. The differential $dF_{p} \colon T_{p}M \to T_{F(p)}N$ has a dual linear map \[ dF_{p}^{*} \colon T^{*}_{F(p)}N \to T^{*}_{p}M, \] the pointwise pullback by $F$ at $p$, or cotangent map of $F$, characterized by $dF_{p}^{*}(\omega)(v) = \omega(dF_{p}(v))$ for $\omega \in T^{*}_{F(p)}N$ and $v \in T_{p}M$.

Formalized. Mathlib/Geometry/Manifold/DerivationBundle.lean::fdifferential; Mathlib/LinearAlgebra/Dual/Defs.lean::LinearMap.dualMap, LinearMap.dualMap_apply — In Lee’s point-derivation tangent model the differential is fdifferential F p; dualizing it gives exactly the cotangent pullback (dFₚ)⁎. The witness compiles the defining formula (dFₚ)⁎ ω v = ω (dFₚ v) at P.

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

Construction/definition — pullback of

FC08-C11-U036 · Ch. 11, § Pullbacks of Covector Fields; source L8204 · not formalized

When we discussed vector fields, we made a point of noting that pushforwards of vector fields under smooth maps are defined only in the special cases of diffeomorphisms or Lie group homomorphisms. The surprising thing about covectors is that covector fields always pull back to covector fields. Given a smooth map $F \colon M \to N$ and a covector field $\omega$ on $N$ , define a rough covector field $F ^ { * } \omega$ on M; called the pullback of ! by $\pmb { F }$ , by \[ (F ^ {*} \omega) _ {p} = d F _ {p} ^ {*} (\omega_ {F (p)}).\tag{11.13} \] It acts f and only if both M and $F$ are compact.

Not formalized. none; no complete checked declaration under strict bundle semantics — The pointwise cotangent map is available as U035, but P/H have no manifold covector-field bundle on which to define the global pullback F*ω, prove its continuity/smoothness, or state the coordinate examples. The standard vector-space differential-form API is not a substitute for a general manifold row. Strict whole-row semantics reject proper subsets, stronger hypotheses, unbridged tangent models, and reconstruction of substantive source theorems from adjacent ingredients.

Proposition 11.25

FC08-C11-U037 · Ch. 11, § Pullbacks of Covector Fields; source L8218 · not formalized

Let $F \colon M \to N$ be a smooth map between smooth manifolds with or without boundary, $u$ a continuous real-valued function on $N$, and $\omega$ a covector field on $N$. Then \[ F^{*}(u\omega) = (u \circ F)\,F^{*}\omega, \tag{11.14} \] and if $u$ is smooth, \[ F^{*}du = d(u \circ F). \tag{11.15} \]

Proposition 11.26

FC08-C11-U038 · Ch. 11, § Pullbacks of Covector Fields; source L8242 · not formalized

Suppose $F \colon M \to N$ is a smooth map between smooth manifolds with or without boundary and $\omega$ is a covector field on $N$. Then $F^{*}\omega$ is a continuous covector field on $M$, and if $\omega$ is smooth, so is $F^{*}\omega$.

Example 11.27

FC08-C11-U039 · Ch. 11, § Pullbacks of Covector Fields; source L8262 · not formalized

R } ^ { 3 } ^ { 2 }$ be the map given by \[ (u, v) = F (x, y, z) = \left(x ^ {2} y, y \sin z\right), \] and let $\omega \in { \mathfrak { X } } ^ { * } \left( \mathbb { R } ^ { 2 } \right)$ be the covector field \[ \omega = u d v + v d u. \] According to (11.16), the pullback $F ^ { * } \omega$ is given by \[ \begin{array}{r l} & F ^ {*} \omega = (u \circ F) d (v \circ F) + (v \circ F) d (u \circ F) \\ & \qquad = \left(x ^ {2} y\right) d (y \sin z) + (y \sin z) d \left(x ^ {2} y\right) \\ & \qquad = x ^ {2} y (\sin z d y + y \cos z d z) + y \sin z \left(2 x y d x + x ^ {2} d y\right) \\ & \qquad = 2 x y ^ {2} \sin z d x + 2 x ^ {2} y \sin z d y + x ^ {2} y ^ {2} \cos z d z. \end{array} \] In other words, to compute $F ^ { * } \omega$ , all you need to do is substitute the component functions of F for the coordinate functions of N everywhere they appear in !! This also yields an easy way to remember the transformation law for a covector field under a change of coordinates. Again, an example will convey the idea better than a general formula. Example 11.28. Let $( r , \theta )$ be polar coordinates on, say, the right half-plane $H =$ $\{ ( x , y ) : x > 0 \}$ . We can think of the change of coordinates $( x , y ) = ( r \cos \theta , r \sin \theta )$ as the coordinate expression for the identity map of $H$ , but using $

Example 11.28

FC08-C11-U040 · Ch. 11, § Pullbacks of Covector Fields; source L8284 · not formalized

Example 11.28. Let $( r , \theta )$ be polar coordinates on, say, the right half-plane $H =$ $\{ ( x , y ) : x > 0 \}$ . We can think of the change of coordinates $( x , y ) = ( r \cos \theta , r \sin \theta )$ as the coordinate expression for the identity map of $H$ , but using $( r , \theta )$ as coordinates for the domain and $( x , y )$ for the codomain. Then the pullback formula (11.17) tells us that we can compute the polar coordinate expression for a covector field simply by substituting $x = r$ cos , $y = r$ sin $\theta$ and expanding. For example, \[ \begin{array}{r l} x d y - y d x & = \operatorname{Id} ^ {*} (x d y - y d x) \\ & = (r \cos \theta) d (r \sin \theta) - (r \sin \theta) d (r \cos \theta) \end{array} \] \[ \begin{array}{l} = (r \cos \theta) (\sin \theta d r + r \cos \theta d \theta) - (r \sin \theta) (\cos \theta d r - r \sin \theta d \theta) \\ = (r \cos \theta \sin \theta - r \sin \theta \cos \theta) d r + \left(r ^ {2} \cos^ {2} \theta + r ^ {2} \sin^ {2} \theta\right) d \theta \\ = r ^ {2} d \theta . \end{array}\tag{//} \]

Definition/convention — restriction of

FC08-C11-U041 · Ch. 11, § Restricting Covector Fields to Submanifolds; source L8304 · not formalized

Since $d\iota_{p} \colon T_{p}S \to T_{p}M$ is the inclusion, under the usual identification of $T_{p}S$ with a subspace of $T_{p}M$, the pullback $\iota^{*}\omega$ is the restriction of $\omega$ to vectors tangent to $S$, and is often called the restriction of $\omega$ to $S$. Note that $\iota^{*}\omega$ can vanish at a point of $S$ even where $\omega$, as a covector field on $M$, does not.

Not formalized. none; no complete checked declaration under strict bundle semantics — These rows require pullback of manifold covector fields along a submanifold inclusion. The cotangent-field layer is absent, and C05 independently established that P/H lack the general embedded/immersed submanifold package used by Lee. Strict whole-row semantics reject proper subsets, stronger hypotheses, unbridged tangent models, and reconstruction of substantive source theorems from adjacent ingredients.

Example 11.29

FC08-C11-U042 · Ch. 11, § Restricting Covector Fields to Submanifolds; source L8306 · not formalized

Let $\omega = dy$ on $\mathbb{R}^{2}$ and let $S$ be the $x$-axis, an embedded submanifold. As a covector field on $\mathbb{R}^{2}$, $\omega$ is nowhere zero, one component function being identically $1$; but its restriction to $S$ vanishes identically, since $y$ vanishes on $S$: \[ \iota^{*}\omega = \iota^{*}dy = d(y \circ \iota) = 0. \] To keep the two readings apart, one says $\omega$ vanishes along $S$, or at points of $S$, when $\omega_{p} = 0$ for every $p \in S$, and that the pullback of $\omega$ to $S$ vanishes for the weaker condition $\iota^{*}\omega = 0$.

Convention/notation — integral of

FC08-C11-U043 · Ch. 11, § Line Integrals; source L8320 · not formalized

We begin with the simplest case: an interval in the real line. Suppose $[ a , b ] \subseteq \mathbb { R }$ is a compact interval, and $\omega$ is a smooth covector field on Œa; b. (This means that the component function of $\omega$ admits a smooth extension to some neighborhood of $[ a , b ] . )$ If we let t denote the standard coordinate on R, then $\omega$ can be written $\omega _ { t } =$ $f ( t ) d t$ for some smooth function $f \colon [ a , b ] \mathbb { R }$ . The similarity between this and the usual notation $\textstyle \int f ( t ) d t$ for an integral suggests that there might be a connection between covector fields and integrals, and indeed there is. We define the integral of ! over $[ a , b ]$ to be \[ \int_ {[ a, b ]} \omega = \int_ {a} ^ {b} f (t) d t. \]

Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib has CurveIntegral for 1-forms on normed vector spaces and proves path reversal, concatenation, linearity, and the integral-as-derivative formula. It does not define line integrals of cotangent fields on arbitrary manifolds, piecewise-smooth manifold curve segments, or Lee’s manifold FTC. Without the missing manifold 1-form layer these are adjacent Euclidean results only. Strict whole-row semantics reject proper subsets, stronger hypotheses, unbridged tangent models, and reconstruction of substantive source theorems from adjacent ingredients.

Proposition 11.31

FC08-C11-U044 · Ch. 11, § Line Integrals; source L8328 · not formalized

Proposition 11.31 (Diffeomorphism Invariance of the Integral). Let ! be a smooth covector field on the compact interval $[ a , b ] \subseteq \mathbb { R }$ . If $\varphi \colon [ c , d ] [ a , b ]$ is an increasing diffeomorphism (meaning that $t _ { 1 } < t _ { 2 }$ implies $\varphi ( t _ { 1 } ) < \varphi ( t _ { 2 } ) )$ , then \[ \int_ {[ c, d ]} \varphi^ {*} \omega = \int_ {[ a, b ]} \omega . \] Proof.

Definition/convention — smooth curve segment

FC08-C11-U045 · Ch. 11, § Line Integrals; source L8346 · not formalized

Now let M be a smooth manifold with or without boundary. By a curve segment in M we mean a continuous curve $\gamma \colon [ a , b ] \to M$ whose domain is a compact interval. It is a smooth curve segment if it is smooth when $[ a , b ]$ is considered as a manifold with boundary (or, equivalently, if $\gamma$ has an extension to a smooth curve defined in a neighborhood of each endpoint). It is a piecewise smooth curve segment if there exists a finite partition $a = a _ { 0 } < a _ { 1 } < \cdots < a _ { k } = b$ of $[ a , b ]$ such that $\gamma \vert _ { [ a _ { i - 1 } , a _ { i } ] }$ is smooth for each $i$ (Fig. 11.4). Continuity of $\gamma$ means that $\gamma ( t )$ approaches the same value as t approaches any of the points $a _ { i }$ (other than $a _ { 0 }$ or $a _ { k } )$ from the left or the right. Smoothness of $\gamma$ on each subinterval means that $\gamma$ has one-sided velocity vectors at each such $a _ { i }$ when approaching from the left or the right, but these one-sided velocities need not be equ l smooth section of $E$ such that $\widetilde { v } ( p ) = v$ .

Proposition 11.33

FC08-C11-U046 · Ch. 11, § Line Integrals; source L8348 · not formalized

Proposition 11.33. If M is a connected smooth manifold with or without boundary, any two points of M can be joined by a piecewise smooth curve segment.

Definition/convention — line integral of

FC08-C11-U047 · Ch. 11, § Line Integrals; source L8361 · not formalized

If $\gamma \colon [a,b] \to M$ is a smooth curve segment and $\omega$ a smooth covector field on $M$, the line integral of $\omega$ over $\gamma$ is the real number \[ \int_{\gamma} \omega = \int_{[a,b]} \gamma^{*}\omega, \] which makes sense because $\gamma^{*}\omega$ is a smooth covector field on $[a,b]$. More generally, for piecewise smooth $\gamma$, \[ \int_{\gamma} \omega = \sum_{i=1}^{k} \int_{[a_{i-1},a_{i}]} \gamma^{*}\omega. \]

Proposition 11.34

FC08-C11-U048 · Ch. 11, § Line Integrals; source L8375 · not formalized

Proposition 11.34 (Properties of Line Integrals). Let M be a smooth manifold with or without boundary. Suppose $\gamma \colon [ a , b ] \to M$ is a piecewise smooth curve segment, and !; $\omega _ { 1 } , \omega _ { 2 } \in \mathfrak { X } ^ { * } ( M )$ (a) For any $c _ { 1 } , c _ { 2 } \in \mathbb { R }$ \[ \int_ {\gamma} (c _ {1} \omega_ {1} + c _ {2} \omega_ {2}) = c _ {1} \int_ {\gamma} \omega_ {1} + c _ {2} \int_ {\gamma} \omega_ {2}. \] $I f \gamma$ is a constant map, then $\begin{array} { r } { \int _ { \gamma } \omega = 0 } \end{array}$ (c) $I f \gamma _ { 1 } = \gamma | _ { [ a , c ] }$ and $\gamma _ { 2 } = \gamma | _ { [ c , b ] }$ with $a < c < b$ , then \[ \int_ {\gamma} \omega = \int_ {\gamma_ {1}} \omega + \int_ {\gamma_ {2}} \omega . \] (d) If $F \colon M \to N$ is any smooth map and $\eta \in { \mathfrak { X } } ^ { * } ( N )$ , then \[ \int_ {\gamma} F ^ {*} \eta = \int_ {F \circ \gamma} \eta . \]

Example 11.36

FC08-C11-U049 · Ch. 11, § Line Integrals; source L8399 · not formalized

Example 11.36. Let $M = \mathbb { R } ^ { 2 } \setminus \{ 0 \}$ , let ! be the covector field on M given by \[ \omega = \frac {x d y - y d x}{x ^ {2} + y ^ {2}}, \] and let $\gamma \colon [ 0 , 2 \pi ] \to M$ be the curve segment defined by $\gamma ( t ) = ( \cos t , \sin t )$ . Since $\gamma ^ { * } \omega$ can be computed by substituting $x = t $ and $y = \sin t$ everywhere in the formula for !, we find that \[ \int_ {\gamma} \omega = \int_ {[ 0, 2 \pi ]} \frac {\cos t (\cos t d t) - \sin t (- \sin t d t)}{\sin^ {2} t + \cos^ {2} t} = \int_ {0} ^ {2 \pi} d t = 2 \pi .\tag{//} \] One of the most significant features of line integrals is that they are independent of parametrization, in a sense we now make precise. If $\gamma \colon [ a , b ] \to M$ and $\widetilde { \gamma } \colon [ c , d ] \to M$ are piecewise smooth curve segments, we say that $\widetilde { \gamma }$ is a reparametrization of if $\widetilde \gamma = \gamma \circ \varphi$ for some diffeomorphism $\varphi \colon [ c , d ] \to [ a , b ]$ . If $\varphi$ is an increasing function, we say that $\widetilde { \gamma }$ is a forward reparametrization, and if $\varphi$ is decreasing, it is a backward reparametrization. (More generally, with obvious mo roof.

Definition/convention — source terminology/construction

FC08-C11-U050 · Ch. 11, § Line Integrals; source L8411 · not formalized

Line integrals are independent of parametrization. If $\gamma \colon [a,b] \to M$ and $\widetilde{\gamma} \colon [c,d] \to M$ are piecewise smooth curve segments, $\widetilde{\gamma}$ is a reparametrization of $\gamma$ if $\widetilde{\gamma} = \gamma \circ \varphi$ for a diffeomorphism $\varphi \colon [c,d] \to [a,b]$; it is a forward reparametrization when $\varphi$ is increasing and a backward one when $\varphi$ is decreasing, and $\varphi$ may more generally be piecewise smooth.

Proposition 11.37

FC08-C11-U051 · Ch. 11, § Line Integrals; source L8413 · not formalized

$\varphi$ to be piecewise smooth.) Proposition 11.37 (Parameter Independence of Line Integrals). Suppose M is a smooth manifold with $o r$ without boundary, $\omega \in { \mathfrak { X } } ^ { * } ( M )$ , and is a piecewise smooth curve segment in M . For any reparametrization $\tilde { \gamma } o f \gamma$ , we have \[ \int_ {\widetilde {\gamma}} \omega = \left\{ \begin{array}{l l} \int_ {\gamma} \omega & \text { if } \widetilde {\gamma} \text { is a forward reparametrization }, \\ - \int_ {\gamma} \omega & \text { if } \widetilde {\gamma} \text { is a backward reparametrization }. \end{array} \right. \]

Proposition 11.38

FC08-C11-U052 · Ch. 11, § Line Integrals; source L8429 · not formalized

If $\gamma \colon [a,b] \to M$ is a piecewise smooth curve segment, the line integral of $\omega$ over $\gamma$ can also be written as the ordinary integral \[ \int_{\gamma} \omega = \int_{a}^{b} \omega_{\gamma(t)}(\gamma'(t))\,dt. \tag{11.18} \]

Theorem 11.39

FC08-C11-U053 · Ch. 11, § Line Integrals; source L8457 · not formalized

Theorem 11.39 (Fundamental Theorem for Line Integrals). Let M be a smooth manifold with or without boundary. Suppose $f$ is a smooth real-valued function on M and $\gamma \colon [ a , b ] \to M$ is a piecewise smooth curve segment in M . Then \[ \int_ {\gamma} d f = f (\gamma (b)) - f (\gamma (a)). \]

Definition/convention — potential for

FC08-C11-U054 · Ch. 11, § Conservative Covector Fields; source L8481 · after FC08-C11-U053, FC08-C11-U032 · not formalized

Fields Theorem 11.39 shows that the line integral of any covector field that can be written as the differential of a smooth function can be computed easily once the smooth function is known. For this reason, there is a special term for covector fields with this property. A smooth covector field $\omega$ on a smooth manifold M with or without 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$ . In this case, the function $f$ is called a potential for !. The potential is not uniquely determined, but by Proposition 11.22, the difference between any two potentials for ! must be constant on each component of M .

Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned CurveIntegral/Poincare.lean formalizes exactness/closedness consequences for 1-forms on normed vector spaces, but P/H still have no manifold covector-field object or Lee-style exact/closed predicates on it. Consequently the manifold conservative/exact/closed definitions, equivalences, pullback theorem, and examples are not complete checked rows. Strict whole-row semantics reject proper subsets, stronger hypotheses, unbridged tangent models, and reconstruction of substantive source theorems from adjacent ingredients.

Definition/convention — conservative

FC08-C11-U055 · Ch. 11, § Conservative Covector Fields; source L8485 · not formalized

We say that a smooth covector field $\omega$ is conservative if the line integral of ! over every piecewise smooth closed curve segment is zero. This terminology comes from physics, where a force field is called conservative if the change in energy caused by the force acting along any closed path is zero (“energy is conserved”). (In elementary physics, force fields are usually thought of as vector fields rather than covector fields; see Problem 11-15 for the connection.)

Proposition 11.40

FC08-C11-U056 · Ch. 11, § Conservative Covector Fields; source L8489 · not formalized

A smooth covector field $\omega$ is conservative if and only if its line integrals are path-independent: $\int_{\gamma} \omega = \int_{\widetilde{\gamma}} \omega$ whenever $\gamma$ and $\widetilde{\gamma}$ are piecewise smooth curve segments with the same starting and ending points.

Theorem 11.42

FC08-C11-U057 · Ch. 11, § Conservative Covector Fields; source L8493 · not formalized

terms of smooth curves instead of piecewise smooth ones.] Theorem 11.42. Let M be a smooth manifold with or without boundary. A smooth covector field on M is conservative if and only if it is exact. P

Example 11.43

FC08-C11-U058 · Ch. 11, § Conservative Covector Fields; source L8546 · after FC08-C11-U049 · not formalized

Example 11.43. The covector field $\omega$ of Example 11.36 cannot be exact on $\mathbb { R } ^ { 2 } \setminus \bar { \{ 0 \} }$ , because it is not conservative: the computation in that example showed that $\textstyle \int _ { \gamma } \omega = 2 \pi \neq 0$ , where $\gamma$ is the unit circle traversed counter h tangent space, one through the origin and another parallel to it, and varying continuously from point to point.

Definition/convention — closed covector field

FC08-C11-U059 · Ch. 11, § Conservative Covector Fields; source L8562 · not formalized

We say that a smooth covector field $\omega$ is closed if its components in every smooth chart satisfy (11.21). The following proposition summarizes the computation above. ##

Proposition 11.44

FC08-C11-U060 · Ch. 11, § Conservative Covector Fields; source L8564 · not formalized

Proposition 11.44. Every exact covector field is closed.

Proposition 11.45

FC08-C11-U061 · Ch. 11, § Conservative Covector Fields; source L8568 · not formalized

Proposition 11.45. Let ! be a smooth covector field on a smooth manifold M with or without boundary. The following are equivalent: (a) ! is closed. (b) ! satisfies (11.21) in some smooth chart around every point. (c) For any open subset $U \subseteq M$ and smooth vector fields $X , Y \in { \mathfrak { X } } ( U )$ \[ X (\omega (Y)) - Y (\omega (X)) = \omega ([ X, Y ]).\tag{11.22} \]

Corollary 11.46

FC08-C11-U062 · Ch. 11, § Conservative Covector Fields; source L8600 · not formalized

Corollary 11.46. Suppose $F \colon M \to N$ is a local diffeomorphism. Then the pullback $F ^ { * } \colon { \mathfrak { X } } ^ { * } ( N ) \to { \mathfrak { X } } ^ { * } ( M )$ takes closed covector fields to closed covector fields, and exact ones to exact ones.

Example 11.47

FC08-C11-U063 · Ch. 11, § Conservative Covector Fields; source L8604 · after FC08-C11-U060 · not formalized

Consider the covector field $\omega = y\cos(xy)\,dx + x\cos(xy)\,dy$ on $\mathbb{R}^{2}$. Since \[ \frac{\partial(y\cos xy)}{\partial y} = \frac{\partial(x\cos xy)}{\partial x} = \cos xy - xy\sin xy, \] $\omega$ is closed. Whether a closed covector field is exact depends in a subtle way on the shape of its domain, as the next example illustrates.

Example 11.48

FC08-C11-U064 · Ch. 11, § Conservative Covector Fields; source L8632 · after FC08-C11-U049 · not formalized

Example 11.48. Look once again at the covector field $\omega$ of Example 11.36. A straightforward computation shows that ! is closed; but as we observed above, it is not exact on $\mathbb { R } ^ { 2 } \setminus \{ 0 \}$ . On the other hand, if we restrict the domain to the right half-plane $U = \{ ( x , y ) : x > 0 \}$ , a computation shows that $\omega = d \left( \tan ^ { - 1 } y / x \right)$ there. This can be seen more clearly in polar coordinates, where $\omega = d \theta$ . The problem, of course, is that there is no smooth (or even continuous) angle function on all of $\mathbb { R } ^ { 2 } \setminus \{ 0 \}$ , which is a consequence of the “hole”

Definition/convention — star-shaped subset

FC08-C11-U065 · Ch. 11, § Conservative Covector Fields; source L8634 · in Mathlib

This last example illustrates a key principle: the question of whether a particular closed covector field is exact is a global one, depending on the shape of the domain in question. This observation is the starting point for de Rham cohomology, which expresses a deep relationship between smooth structures and topology. We will define de Rham cohomology and study this relationship in Chapter 17, but for now we can prove the following result. If $\dot { V }$ is a finite-dimensional vector space, a subset $U \subseteq V$ is said to be star-shaped if there is a point $c \in U$ such that for every $x \in U$ the line segment from c to x is entirely contained in U (Fig. 11.6). For example, every convex subset is star-shaped.

Formalized. Mathlib/Analysis/Convex/Star.lean::StarConvex, starConvex_iff_segment_subset — StarConvex ℝ c U is exactly the condition that every segment from c to a point of U lies in U; existentially choosing c ∈ U is Lee’s star-shaped definition. The equivalence is compiled in the C11 witness.

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

Theorem 11.49

FC08-C11-U066 · Ch. 11, § Conservative Covector Fields; source L8636 · not formalized

Theorem 11.49 (Poincaré Lemma for Covector Fields). If U is a star-shaped open subset of $\mathbb { R } ^ { n } o r \mathbb { H } ^ { n }$ , then every closed covector field on U

Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned CurveIntegral/Poincare.lean proves a Poincaré lemma for convex subsets of normed spaces. Lee assumes only star-shaped open subsets of ℝ^n or ℍ^n; convexity is strictly stronger, and no star-shaped version was found at P or H. Whole-row semantics therefore reject the stronger-hypothesis theorem. Strict whole-row semantics reject proper subsets, stronger hypotheses, unbridged tangent models, and reconstruction of substantive source theorems from adjacent ingredients.

Corollary 11.50

FC08-C11-U067 · Ch. 11, § Conservative Covector Fields; source L8667 · not formalized

Corollary 11.50 (Local Exactness of Closed Covector Fields). Let ! be a closed covector field on a smooth manifold M with or without boundary. Then every point of M has a neighborhood on which ! is exact.

Not formalized. none; no complete checked declaration under strict bundle semantics — Local exactness would follow from a manifold Poincaré lemma, but no manifold cotangent/closed-1-form layer is present at P/H and the pinned vector-space theorem does not itself supply this general manifold corollary. Strict whole-row semantics reject proper subsets, stronger hypotheses, unbridged tangent models, and reconstruction of substantive source theorems from adjacent ingredients.

Example 11.51

FC08-C11-U068 · Ch. 11, § Conservative Covector Fields; source L8675 · not formalized

Example 11.51. Let $\omega$ be the following covector field on $\mathbb { R } ^ { 3 }$ : \[ \omega = e ^ {y ^ {2}} d x + 2 x y e ^ {y ^ {2}} d y - 2 z d z. \] You can check that ! is closed. For f to be a potential for $\omega .$ , it must satisfy = e ^ {y = 2 x y e = - 2 z. \[ Holding y and $z$ fixed and integrating the first equation with respect to x, we obtain \] f (x, y, z) = e ^ {y ^ {2}} d x = x e ^ {y ^ {2}} + C _ {1} (y, z), \[ where the “constant” of integration $C _ { 1 } ( y , z )$ may depend on the choice of $( y , z )$ Now the second equation of (11.25) implies \] 2 x {2}} = (x e ^ {y ^ {2}} + C _ {1} (y, z)) e ^ {y ^ {2}} + , \[ which forces $\partial C _ { 1 } / \partial y = 0$ , so $C _ { 1 }$ is actually a function of z only. Finally, the third equation implies \] { 2 } } - z ^ { 2 }$ . Any other potential differs from this one by a constant. You should convince yourself that the formal procedure we followed in this example is equivalent to choosing an arbitrary base point $

Not formalized. none; no complete checked declaration under strict bundle semantics — No checked declaration packages Lee’s explicit three-variable covector-field computation and potential. Generic differentiation primitives and the vector-space Poincaré machinery would require reconstructing the example. Strict whole-row semantics reject proper subsets, stronger hypotheses, unbridged tangent models, and reconstruction of substantive source theorems from adjacent ingredients.