Pullback of forms along local diffeomorphisms #
Pullback along a map f only sees the value of a form at f x through the derivative of f
at x. When that derivative is surjective, the pullback at x therefore determines the form at
f x (TauCeti.mpullback_apply_eq_mpullback_apply_iff), so pullback along a surjective local
diffeomorphism is injective (IsLocalDiffeomorph.mpullback_injective).
Regularity transfers in both directions as well. Near f x, a form ω is the pullback of
f^* ω along a local inverse of f, so ω is C^m near f x exactly when f^* ω is C^m
near x, for a C^n local diffeomorphism with m + 1 ≤ n
(IsLocalDiffeomorphAt.contMDiffAt_mpullback_form_iff). For a surjective local diffeomorphism
this gives IsLocalDiffeomorph.isSmoothForm_mpullback_iff, and, since pullback commutes with the
exterior derivative, a smooth form is closed exactly when its pullback is
(IsLocalDiffeomorph.isClosed_mpullback_iff).
These facts are what let forms on a covering space whose deck group acts transitively on each
fibre descend to the base when they are invariant under the deck group. Given a family of
self-maps of the source lying over f and transitive on its fibres, a form invariant under the
family is basic for f (IsLocalDiffeomorph.isBasic_of_mpullback_eq), so it is the pullback of
its descent TauCeti.RoughForm.descendedForm. Hence a form is a pullback along f exactly
when it is invariant under the family (IsLocalDiffeomorph.exists_mpullback_eq_iff). For a
surjective smooth local diffeomorphism the descended form of a smooth form is smooth
(IsLocalDiffeomorph.exists_smoothForm_mpullback_eq_iff).
A pullback identity between coordinate expressions in a chart is carried to the manifold by
conjugating with the chart
(TauCeti.RoughForm.exists_partialDiffeomorph_mpullback_eq_of_inChartAt). Its flat counterpart
conjugates by a partial diffeomorphism Θ of normed spaces: if a partial diffeomorphism Ψ
pulls Θ^* ω₁ back to Θ^* ω₀, then Θ ∘ Ψ ∘ Θ⁻¹ pulls ω₁ back to ω₀
(TauCeti.exists_partialDiffeomorph_compContinuousLinearMap_fderiv_eq_of_conj).
Main results #
IsLocalDiffeomorph.mpullback_injective: pullback along a surjective local diffeomorphism is injective.IsLocalDiffeomorphAt.mpullback_apply_eq_zero_iff: a pullback along a local diffeomorphism vanishes at a point exactly when the form vanishes at its image.IsLocalDiffeomorphAt.contMDiffAt_mpullback_form_iff,IsLocalDiffeomorph.isSmoothForm_mpullback_iff: a form isC^mexactly when its pullback along a (surjective)C^nlocal diffeomorphism is, form + 1 ≤ n.IsLocalDiffeomorph.isClosed_mpullback_iff: a smooth form is closed exactly when its pullback along a surjective smooth local diffeomorphism is.IsLocalDiffeomorph.isBasic_of_mpullback_eq: a form invariant under a family of maps over a local diffeomorphism that is transitive on its fibres is basic for it.IsLocalDiffeomorph.exists_mpullback_eq_iff,IsLocalDiffeomorph.exists_smoothForm_mpullback_eq_iff: a (smooth) form is the pullback of a (smooth) form along a local diffeomorphism exactly when it is invariant under a family of maps over it that is transitive on its fibres.TauCeti.RoughForm.exists_partialDiffeomorph_mpullback_eq_of_inChartAt: a partial diffeomorphism of the model space relating the coordinate expressions of two forms in a chart gives a partial diffeomorphism of the manifold relating the forms.TauCeti.exists_partialDiffeomorph_compContinuousLinearMap_fderiv_eq_of_conj: conjugating a pullback identity of flatk-forms by a partial diffeomorphism.
References #
- John M. Lee, Introduction to Smooth Manifolds, second edition, Graduate Texts in Mathematics 218, Springer, 2013, Chapter 14 (pullbacks of differential forms).
Pullback along a surjective C^n local diffeomorphism, n ≠ 0, is injective on rough
forms.
A form pulled back along a C^n local diffeomorphism at x, n ≠ 0, vanishes at x exactly
when the form vanishes at f x.
Let f be a C^n local diffeomorphism, n ≠ 0, and let σ be a family of self-maps of M
over f (f ∘ σ i = f) that is transitive on the fibres of f. Then a form invariant under every
σ i is basic for f. No differentiability of σ is assumed: where σ i is not differentiable
its derivative is the junk value 0, and invariance then forces the form to vanish there (in
positive degree).
Descent of forms along a local diffeomorphism. Let f be a C^n local diffeomorphism,
n ≠ 0, and let σ be a family of differentiable self-maps of M over f (f ∘ σ i = f) that
is transitive on the fibres of f: two points with the same image are equal or are related by
some σ i. Then a form on M is the pullback of a form on M' exactly when it is invariant
under every σ i. For a covering map whose deck transformations act transitively on each fibre,
one can take the σ i to be the deck transformations.
For a C^n local diffeomorphism f at x and m + 1 ≤ n, a form is a C^m section near
f x exactly when its pullback along f is a C^m section near x.
For a surjective C^n local diffeomorphism f and m + 1 ≤ n, a form is C^m exactly when
its pullback along f is.
Descent of smooth forms along a surjective local diffeomorphism. For a surjective smooth
local diffeomorphism f and a family of smooth self-maps σ i of M over f that is transitive
on the fibres of f, a smooth form on M is the pullback of a smooth form on M' exactly when it
is invariant under every σ i.
For a surjective smooth local diffeomorphism f, a smooth form is closed exactly when its
pullback along f is.
Conjugating a pullback identity by a coordinate change. Let Θ be a C^r partial
diffeomorphism from F to E, and let Ψ be a C^r partial diffeomorphism of F whose
source contains an open set O ⊆ Θ.source, which maps O into Θ.source and pulls Θ^* ω₁
back to Θ^* ω₀ on O. Then the conjugate Θ ∘ Ψ ∘ Θ⁻¹, defined on Θ '' O, is a C^r
partial diffeomorphism of E which pulls ω₁ back to ω₀ on its source.
Transport through a chart. Let φ be the preferred chart at x₀, and let Φf be a C^n
partial diffeomorphism of the model space, 1 ≤ n, which pulls the coordinate expression of ω₁
in φ back to that of ω₀ on its source. Then φ⁻¹ ∘ Φf ∘ φ, defined where φ and Φf take
values in the interior of the chart target, is a C^n partial diffeomorphism of M which pulls
ω₁ back to ω₀ on its source.