The exterior derivative of differential forms on manifolds #
A rough form φ : RoughForm I M F k with values in a fixed normed space is read in the
preferred extended chart at x₀ as the flat form φ.inChartAt x₀ : E → E [⋀^Fin k]→L[ℝ] F:
its pullback along (extChartAt I x₀).symm, with derivatives taken within range I. The
exterior derivative mextDerivWithin φ s x is Mathlib's flat exterior derivative
extDerivWithin of the coordinate expression in the chart at x itself, taken within
(extChartAt I x).symm ⁻¹' s ∩ range I at the chart point of x; tangent vectors at x are
read in that same chart. mextDeriv φ is the version on the whole manifold. This is the
construction of Mathlib's manifold Lie bracket VectorField.mlieBracketWithin, transposed to
forms. Like mfderiv, both are total, with junk values where the form is not differentiable;
the real hypotheses are carried by the theorems. Working within range I makes the
definition meaningful at boundary and corner points.
The file proves the basic calculus of this operator: locality in the set and in the form,
additivity and homogeneity, agreement with Mathlib's extDerivWithin over the model space
𝓘(ℝ, E), and the identification of the exterior derivative of the 0-form of a function with
the manifold derivative mvfderivWithin of the function. Consequently the 0-form of a
differentiable function is closed exactly when the function is locally constant.
Main declarations #
TauCeti.RoughForm.inChartAt: the coordinate expression of a rough form in a chart.TauCeti.mextDerivWithin,TauCeti.mextDeriv: the exterior derivative of a rough form.TauCeti.mextDerivWithin_congr_of_eventuallyEq,TauCeti.mextDerivWithin_congr_set: locality.TauCeti.mextDerivWithin_add,TauCeti.mextDerivWithin_smul: linearity.TauCeti.mextDerivWithin_eq_extDerivWithin,TauCeti.mextDeriv_eq_extDeriv: over the model space, the manifold exterior derivative is the flat one.TauCeti.mextDerivWithin_ofFunction,TauCeti.mextDeriv_ofFunction,TauCeti.mextDeriv_ofFunction_apply: the exterior derivative of a function is its manifold derivative.TauCeti.mextDeriv_ofFunction_eq_zero_iff: the0-form of a differentiable function is closed exactly when the function is locally constant.TauCeti.mextDeriv_ofFunction_snd_apply: the differential of the second coordinate ofM × Freads the second coordinate of a tangent vector.TauCeti.mextDeriv_eq_zero_of_finrank_le: on a manifold of dimension at mostk, the exterior derivative of everyk-form vanishes.
References #
- John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Graduate Texts in Mathematics 218, Springer, 2013, Chapter 14.
The coordinate expression of a form in a chart #
The coordinate expression of a rough form in the preferred extended chart at x₀: its
pullback along (extChartAt I x₀).symm, with the derivative taken within range I. At a
chart coordinate z, tangent vectors at (extChartAt I x₀).symm z are thus fed to the form in
the coordinates of the chart at x₀. Outside the chart target the value is junk.
Instances For
The coordinate expression commutes with scalar multiplication of the coefficients, by any scalars acting continuously on the coefficient space and commuting with the real action.
Scalar localization of a form multiplies its coordinate expression by the pulled-back scalar.
At the centre of its own chart, the coordinate expression of a form is its value there.
The exterior derivative #
The exterior derivative of a rough form within a set s, at a point x: the flat exterior
derivative of the coordinate expression of the form in the chart at x, within
(extChartAt I x).symm ⁻¹' s ∩ range I at the chart point of x. Tangent vectors at x are
read in the chart at x. Total, with junk values where the form is not differentiable.
Instances For
The exterior derivative of a rough form.
Instances For
Locality #
The exterior derivative within a set does not change when the set is modified away from a
point y, as long as it is unchanged near x (punctured at y).
The exterior derivative within a set only depends on the germ of the set.
The exterior derivative within a set only depends on the form near the point within the set, and at the point.
The exterior derivative only depends on the germ of the form.
Linearity #
The exterior derivative is additive on forms whose coordinate expressions in the chart at the point are differentiable there.
The exterior derivative is additive on forms whose coordinate expressions in the chart at the
point are differentiable within range I there.
The exterior derivative commutes with scalar multiplication of the coefficients wherever
derivatives within the set are unique; no differentiability of the form is needed. The scalars
are those of a division semiring acting continuously on the coefficient space and commuting with
the real action, such as ℝ itself or ℂ on complex coefficients.
The exterior derivative commutes with scalar multiplication of the coefficients by a division semiring acting continuously and commuting with the real action.
The exterior derivative within a set is subtractive on forms whose coordinate expressions in the chart at the point are differentiable there, wherever derivatives within the set are unique.
Swapping two tangent vectors negates the exterior derivative of a one-form.
The exterior derivative of a one-form, evaluated on two tangent vectors, is linear in the first vector.
The model space #
Over the model space 𝓘(ℝ, E), the coordinate expression of a form is the form itself.
Over the model space 𝓘(ℝ, E), the manifold exterior derivative within a set is the flat
exterior derivative extDerivWithin.
Over the model space 𝓘(ℝ, E), the manifold exterior derivative is the flat exterior
derivative extDeriv.
The manifold exterior derivative of a constant form on its self-model space vanishes.
Functions #
The coordinate expression of the 0-form of a function is the 0-form of the function
written in the chart.
The exterior derivative of the 0-form of a function is its manifold derivative, read as a
1-form.
The exterior derivative of the 0-form of a function is its manifold derivative, read as a
1-form.
The exterior derivative of the 0-form of a function, evaluated on a tangent vector, is the
manifold derivative of the function applied to that vector.
The chain rule for the exterior derivative of a 0-form. If f is differentiable at x
and g has derivative g' at f x, then d (g ∘ f) = g' • df at x.
A function which near x differs by a constant from a function g differentiable at x has
the same exterior derivative at x as g.
The exterior derivative of the 0-form of a function vanishes at a point exactly when the
manifold derivative of the function does.
The exterior derivative of the 0-form of the zero function vanishes.
The 0-form of a differentiable function is closed exactly when the function is locally
constant. The manifold may have boundary or corners.
The exterior derivative of the 0-form of a sum of differentiable functions is the sum of
their exterior derivatives.
On a product M × F with a normed space F, the exterior derivative of the second coordinate
reads the second coordinate of a tangent vector.
Forms of top degree #
On a manifold of finite dimension at most k, the exterior derivative of every rough k-form
vanishes, since there are no nonzero (k + 1)-forms. In particular, top-degree forms are closed.