Transport of distributions through diffeomorphisms #
A partial diffeomorphism transports local frames and involutivity between its source and target, while a global diffeomorphism transports smooth constant-rank distributions. This allows regularity and involutivity to be checked in local or global coordinate models when constructing integral manifolds. In particular, the pullback of a smooth distribution is smooth, and a distribution is involutive if and only if its pullback by a diffeomorphism is involutive.
The vector-field pullback and Lie-bracket naturality APIs are provided by Mathlib.
TauCeti.IsDistributionFrameOn.comap_mfderivWithin pulls a local frame back through partial
coordinates. TauCeti.IsDistributionFrameOn.comap_mfderiv is its global specialization, and
TauCeti.IsContMDiffDistribution.comap_mfderiv pulls back a smooth distribution.
PartialDiffeomorph.isInvolutiveDistributionOn transports local involutivity,
TauCeti.IsInvolutiveDistribution.diffeomorph is its global specialization, and
Diffeomorph.isInvolutiveDistribution_iff gives the equivalence for identified distributions.
Diffeomorph.isInvolutiveDistribution_comap_mfderiv_iff gives the pullback characterization.
PartialDiffeomorph.isInvolutiveDistributionOn_comap_mfderivWithin shows that the pullback of a
distribution involutive on the target is involutive on the source.
The distributions remain families of tangent subspaces, and their pullback is expressed by
Submodule.comap along the differential. Pulling back a C^m frame through a C^n
diffeomorphism requires m + 1 โค n, because the vector-field pullback contains the inverse
differential. Involutivity requires the diffeomorphism to be at least Cยฒ over the reals
(minSmoothness ๐ 2 over a general scalar field), so that pullbacks of differentiable vector
fields are differentiable and their Lie brackets transform naturally.
Pulling a local frame back through partial coordinates gives a frame on the part of the coordinate source mapping into the original frame domain. The loss of one derivative comes from the inverse differential in the vector-field pullback.
Pulling a local frame back through a diffeomorphism gives a local frame for the pullback distribution. The loss of one derivative comes from the inverse differential in the vector-field pullback.
The pullback of a C^m distribution through a C^n diffeomorphism is a C^m
distribution of the same rank when m + 1 โค n.
The differential of a partial diffeomorphism carries a family of subspaces onto its pullback through the inverse.
A partial diffeomorphism whose differential identifies two distributions transports involutivity from its source to its target. The tangent-space identification is stated as membership equivalence, so it applies directly to both images and preimages of subspaces under the differential.
The pullback of a distribution through the differential of a partial diffeomorphism is involutive on the source when the distribution is involutive on the target.
A diffeomorphism whose differential identifies two distributions transports involutivity. The tangent-space identification is stated as membership equivalence, so it applies directly to both images and preimages of subspaces under the differential.
Involutivity is invariant under a diffeomorphism identifying tangent distributions.
A distribution is involutive exactly when its pullback by a diffeomorphism is involutive. This form expresses the transported distribution directly as the preimage of each tangent subspace under the differential.