Regularity of differential forms in charts #
The fibre coordinate of a fixed-coefficient form in the alternating-map bundle is its pullback along the inverse extended chart. This transfers smooth-section regularity to the flat regularity needed for exterior differentiation, including within subsets at boundary points.
Conversely, flat regularity of a coordinate expression gives regularity of the section. The
manifold exterior derivative takes
C^p sections to C^n sections whenever n + 1 ≤ p, on any manifold of class C² over any
model with corners.
In particular it maps smooth k-forms to smooth (k+1)-forms. A form supported compactly inside
a chart extends by zero with the same regularity within the model range, and exterior
differentiation commutes with this extension.
Main declarations #
TauCeti.RoughForm.contDiffWithinAt_inChartAt: aC^nsection hasC^nchart expressions.TauCeti.RoughForm.contDiffWithinAt_of_contMDiffWithinAt_modelSpace: over the model space, aC^nsection within a set is aC^nfunction within that set.TauCeti.RoughForm.contDiffWithinAt_inChartAt_of_contDiffWithinAt_inChartAt: on aC^(n+1)manifold,C^nregularity of chart expressions transfers between overlapping charts;TauCeti.IsSmoothForm.contDiffOn_inChartAt_interior_targetandTauCeti.IsSmoothForm.inChartAt_mextDeriv_eq_extDerivdeduceContDiffOnand ordinary flatextDerivon the interior of any preferred chart target.TauCeti.contMDiffAt_mpullback_extChartAt: a flat form that isC^nwithin the model range pulls back along a chart to aC^nsection.TauCeti.contMDiffOn_mextDerivWithin,TauCeti.isSmoothBundleForm_mextDeriv,TauCeti.isSmoothForm_mextDeriv: the exterior derivative lowers regularity by one.TauCeti.mextDeriv_mem_smoothBundleForms: the exterior derivative preserves smooth forms.TauCeti.exists_mextDeriv_eq_of_forall_eventuallyEq_add_const: a global function which near every point differs by a constant from a local primitive of a1-form is itself a primitive.TauCeti.mextDerivₗ: the exterior derivative as a linear map on smooth fixed-coefficient forms.TauCeti.contMDiffAt_ofFunction_iff,TauCeti.isSmoothForm_ofFunction_iff: the0-form of a function is as regular as the function, pointwise and globally.TauCeti.mdifferentiableAt_ofFunction: the0-form of a differentiable function is a differentiable section.TauCeti.mdifferentiableAt_form_of_differentiableWithinAt_inChartAt_self: a form whose coordinate expression in its own preferred chart is differentiable is a differentiable section.
References #
- John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Chapter 14.
- Mathlib's alternating-bundle coordinates (
ContinuousAlternatingMap.inCoordinates) and inverse tangent coordinates (TangentBundle.symmL_trivializationAt).
The alternating-bundle fibre coordinate of a form is its inverse-chart pullback.
A differentiable section has a differentiable coordinate expression in the preferred chart, with derivatives taken within the inverse image of the subset intersected with the model range.
A section differentiable at x has a coordinate expression in the chart centred at x
that is differentiable within the model range at the chart image of x.
On a boundaryless manifold, a section differentiable at x has a coordinate expression in the
chart centred at x that is differentiable at the chart image of x.
Section regularity within a subset implies flat regularity in the chart centred at the point. The derivative set is the inverse image of the subset intersected with the model range.
A C^n section has a C^n coordinate expression in the chart centred at x, within the
model range at the chart image of x.
Near the chart point, the coordinate expression of mextDerivWithin φ s in the chart centred
at x is the flat exterior derivative of the coordinate expression of φ within the coordinate
set. The form is C¹ as a section on s, which has unique derivatives and is contained in the
closure of its interior.
The exterior derivative within a subset costs one derivative: if φ is a C^(n+1) section on
s, then mextDerivWithin φ s is a C^n section on s. The subset has unique derivatives and is
contained in the closure of its interior; it may contain boundary and corner points.
The exterior derivative takes C^p fixed-coefficient forms to C^n forms when n + 1 ≤ p,
including infinite regularity, over any model with corners.
The exterior derivative takes C^p forms to C^n forms when n + 1 ≤ p.
The exterior derivative of a C¹ form is a continuous section.
The exterior derivative of a smooth fixed-coefficient form is smooth.
In the form's own preferred chart, its section regularity is its coordinate regularity within the model range at the chart center.
Exterior differentiation commutes with finite sums of C1 forms. The differentiability hypotheses ensure additivity of the coordinate derivatives.
Coordinate regularity of a form transfers between preferred charts: regularity within the
model range in the chart at β, at the image of a point of the overlap, gives the same regularity
in the chart at α. The coordinate change and its derivative must have one more order of
regularity, so the manifold is C^(n+1).
A C1 form has C1 coefficients at every point of each preferred chart target on a C2 manifold. The coordinate cocycle transports both the form and the chart derivative.
On a C² manifold, the actual exterior derivative read in any preferred chart is the
flat exterior derivative of the original coordinate expression.
On a C^(n+1) manifold, a C^n form has C^n coordinate expression in any preferred chart on
the interior of the chart target.
On the interior of a preferred chart target on a C² manifold, the manifold exterior derivative
of a C¹ form read in that chart is the ordinary flat exterior derivative extDeriv.
Regularity of a form's coordinate expression in its own preferred chart implies pointwise regularity of its bundle section, including within the full model range at boundary points.
Differentiability of a form's coordinate expression in its own preferred chart, within the full model range, implies differentiability of its bundle section at the point.
Regularity of a form's coordinate expression in any preferred chart, at the image of a point of its source, implies regularity of the bundle section at that point.
The pullback of a flat form along a preferred extended chart is C^n at a point of the chart
source when the flat form is C^n within the model range at the chart image of the point. The flat
form need not be regular on a neighbourhood in the model space, which matters at boundary
points.
A C^r form α on an open set s intersected with the model range, pulled back along the
chart at x and cut off by a C^r function supported where the chart lands in s, is a C^r
form on all of M.
Regularity of the coordinate expression in each point's own preferred chart implies regularity of the differential-form section.
The 0-form of a function is a C^n section at x exactly when the function is C^n at
x.
The 0-form of a function is a C^n form exactly when the function is C^n.
The 0-form of a function differentiable at a point is a section differentiable there.
Local primitives glue to a global one. If near every point x the function f differs by
a constant from a function g which is C^r at x (r ≠ 0) with d g = φ at x, then the
0-form of f is a C^r primitive of φ.
Every zero-dimensional form is smooth: its coordinate functions have singleton domain.
Over the model space 𝓘(ℝ, E), a form is a C^n section exactly when it is a C^n
function into the space of alternating maps.
Over the model space 𝓘(ℝ, E), a form that is a C^n section within s at x is a C^n
function into the space of alternating maps within s at x.
The exterior derivative as a real linear map on smooth fixed-coefficient forms.
Instances For
The bundled derivative has the usual rough exterior derivative as its underlying form.
The exterior derivative of a smooth function, regarded as a 0-form, evaluated on a tangent
vector, is the derivative of the function applied to that vector.
The 0-form of a smooth function, as a smooth form.
Instances For
The rough form underlying the smooth 0-form of a function is its rough 0-form.
Evaluating the smooth 0-form of a function on the empty tuple of tangent vectors recovers the
function.
The exterior derivative of a smooth form is a smooth section.
The exterior derivative commutes with transport across an equality of degrees.
The exterior derivative of a one-form, evaluated on two tangent vectors, is the bilinear form
of the two-form dα.
A coordinate form supported compactly inside the chart extends with the same regularity within the model range. Regularity outside the model range is unnecessary.
For a form supported inside one chart, exterior differentiation of its zero extension is the zero extension of its actual manifold exterior derivative, throughout the model range.
A compact chart-supported C¹ form whose support avoids the boundary has a globally C¹
coordinate extension by zero. No integration or finite-dimensional hypothesis is required.