Locality and linear pullback of the exterior derivative #
The exterior derivative extDerivWithin Ο s x of a differential form on a normed space is the
alternatization of fderivWithin π Ο s x, so, like the derivative, it only sees the set s
near x. These are the exterior-derivative versions of fderivWithin_congr_set' and
fderivWithin_congr_set; they are what makes the exterior derivative of forms on manifolds,
computed in charts, insensitive to the set away from the base point.
ContinuousLinearMap.extDerivWithin_pullback also proves naturality under a fixed linear map
using only within-set differentiability, with no second derivative or interior-density hypothesis.
Its global form ContinuousLinearMap.extDeriv_pullback holds at each point where the form is
differentiable, so pullback along a continuous linear map preserves closedness
(ContinuousLinearMap.extDeriv_pullback_eq_zero), and it preserves regularity on the preimage of
the domain (TauCeti.contDiffOn_pullback_continuousLinearMap).
ContinuousLinearMap.extDerivWithin_compContinuousAlternatingMap is the corresponding naturality
in the coefficient space, and TauCeti.extDerivWithin_smul_field extends extDerivWithin_smul to
scalars, such as β, that act on the coefficients but not on the domain, and
TauCeti.extDerivWithin_function_smul is the Leibniz rule for multiplication by a scalar
function. DifferentiableAt.extDerivWithin is the exterior-derivative version of
DifferentiableAt.fderivWithin, and TauCeti.tsupport_extDeriv_subset and
HasCompactSupport.extDeriv are the versions of tsupport_fderiv_subset and
HasCompactSupport.fderiv. TauCeti.extDerivWithin_of_isOpen is the version of
fderivWithin_of_isOpen. TauCeti.extDeriv_apply_pair_eq_sum writes the exterior derivative of a
one-form βα΅’ Οα΅’ dxα΅’ on ΞΉ β π as βα΅’ dΟα΅’ β§ dxα΅’.
The alternatization of a continuous linear map into one-forms, on an ordered pair:
alternatizeUncurryFin f (v, w) = f v (w) - f w (v).
The exterior derivative of a form vanishes at a point where the form is not differentiable,
because fderiv takes the junk value 0 there.
The exterior derivative of a one-form on an ordered pair is the alternating part of its FrΓ©chet derivative. This formula also respects the derivative's junk-value convention.
The exterior derivative of a zero-form on a single vector is its FrΓ©chet derivative in that direction. This formula also respects the derivative's junk-value convention.
The exterior derivative of a one-form differentiable at x, on an ordered pair, in terms of
the derivatives of its coefficient functions Ο(w) and Ο(v). This is the two-vector case of
extDeriv_apply; it is the curl identity that turns the divergence theorem into Stokes' formula
on a rectangle.
The exterior derivative of a one-form Ο = βα΅’ Οα΅’ dxα΅’ on ΞΉ β π, differentiable at x, in
terms of its coefficient functions Οα΅’ = Ο(eα΅’) on the standard basis: dΟ = βα΅’ dΟα΅’ β§ dxα΅’.
The exterior derivative of a difference of two forms differentiable at x is the difference of
their exterior derivatives.
Where a differential form is not differentiable, its exterior derivative is 0, by the junk
value convention of the FrΓ©chet derivative.
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 the base point (punctured at y).
The exterior derivative within a set only depends on the germ of the set at the base point.
The exterior derivative within a neighbourhood of the base point is the exterior derivative.
The exterior derivative within an open set containing the base point is the exterior derivative.
Iterating the exterior derivative within a set still depends only on the germ of that set.
The exterior derivative within a set commutes with multiplication of the coefficients by a
scalar from a division semiring acting on the coefficient space, such as β acting on a complex
space regarded over β. No differentiability is needed.
The exterior derivative commutes with multiplication of the coefficients by a scalar from a division semiring acting on the coefficient space.
The Leibniz rule for the exterior derivative within a set of a form multiplied by a
scalar function: d (c β’ Ο) = c β’ dΟ + dc β§ Ο. The term dc β§ Ο is the alternatization of
v β¦ dc(v) β’ Ο, which evaluates as β i, (-1) ^ i β’ dc(vα΅’) β’ Ο(vβ, β¦, vΜα΅’, β¦, vβ).
The Leibniz rule for the exterior derivative of a form multiplied by a scalar function:
d (c β’ Ο) = c β’ dΟ + dc β§ Ο, where dc β§ Ο is the alternatization of v β¦ dc(v) β’ Ο.
The exterior derivative of a form vanishes wherever the form vanishes near the point, so its topological support lies in that of the form.
The exterior derivative of a compactly supported form is compactly supported.
The exterior derivative within a set of a form differentiable at a point of unique differentiability is its exterior derivative.
The exterior derivative of a continuous linear differential form is its alternatization.
Exterior differentiation commutes with pullback by a continuous linear map, with only within-set differentiability of the form.
Exterior differentiation commutes with pullback along a continuous linear map A, for a form
differentiable at A x.
Pulling back along a continuous linear map A a form that is differentiable and closed at
A x gives a form closed at x.
Pulling a C^r form on t back along a continuous linear map A gives a C^r form on
A β»ΒΉ' t.
Exterior differentiation commutes with a fixed continuous linear map of coefficients, for a form differentiable within the set.
Exterior differentiation commutes with a fixed continuous linear map of coefficients, for a differentiable form.