Regularity and functoriality of pullback bundles #
A map into the total space of a pullback bundle is smooth exactly when its projection to the new base and its lift to the original total space are smooth. This is the smooth analogue of the initial-topology description of a pullback bundle.
The criterion lets a map into a pullback bundle be checked without unfolding the pulled-back trivializations. It is particularly useful for tangent maps whose base points agree through a commuting square.
The criterion applies to fibre bundles with a normed model fibre; the fibres themselves need only be nonempty topological spaces, without an additive or vector-space structure.
Along a local diffeomorphism f, regularity of sections can be read upstairs: a section σ of
E is C^m at f x exactly when its pullback y ↦ σ (f y), a section of f *ᵖ E, is C^m at
x (IsLocalDiffeomorphAt.contMDiffAt_section_iff_pullback), and for a surjective local
diffeomorphism, such as the orbit projection of a free properly discontinuous action, a section
is C^m exactly when its pullback is (IsLocalDiffeomorph.contMDiff_section_iff_pullback).
The file also records the functoriality of Mathlib's pullback f *ᵖ E in C^n maps f, on its
own carrier. The canonical map Pullback.lift f to the total space of E is C^n
(Bundle.Pullback.contMDiff_lift), and a family of fibrewise maps inducing a C^n map of total
spaces pulls back along a C^n map to one that does too (Bundle.Pullback.contMDiff_fiberwise).
When the model fibre is finite-dimensional over a complete field 𝕜, TauCeti.bundleDiffeomorph
and the fibre instances of TauCeti.Topology.VectorBundle.Pullback therefore make the pullback
x ↦ e (f x) of a C^n family e of fibrewise linear equivalences again a C^n bundle
equivalence. The pullback along the identity is C^n diffeomorphic to E
(Bundle.Pullback.idDiffeomorph), and the pullback along a composite g ∘ f to the iterated
pullback f *ᵖ (g *ᵖ E) (Bundle.Pullback.compDiffeomorph), whatever the regularity of the
maps pulled back along. Both comparisons are the identity on every fibre, so for vector bundles
they are fibrewise linear, and over a complex model at n = ∞ they are holomorphic bundle
equivalences between holomorphic vector bundles, which Mathlib's ContMDiffVectorBundle.pullback
makes f *ᵖ E when E is one.
References #
- D. Husemoller, Fibre Bundles, 3rd ed., Graduate Texts in Mathematics 20, Springer, 1994, Chapter 2 (induced bundles).
The native Hom section between two pullbacks by the same map is Cⁿ exactly when its original
Hom field along that map is Cⁿ (Bundle.Pullback.contMDiff_hom_section_iff). This dictionary
requires neither finite rank nor a smooth bundle structure on the fibres.
A map into a pullback bundle is C^n at a point exactly when its base projection and its
lift to the original total space are C^n there.
A map into a pullback bundle is C^n exactly when its base projection and its lift to the
original total space are C^n.
The canonical map Pullback.lift f from the total space of a pullback bundle to the original
total space is C^n at every point over which f is C^n.
The canonical map Pullback.lift f from the total space of a pullback bundle to the original
total space is C^n when f is.
Pulling back is natural: if a family φ of fibrewise maps from E to E' induces a C^n map
of total spaces, then so does the family x ↦ φ (f x) pulled back along a C^n map f, from
f *ᵖ E to f *ᵖ E'. The fibrewise maps need not be linear.
The pullback of a bundle along the identity is the bundle itself: the canonical map
Pullback.lift is a C^n diffeomorphism of total spaces, the identity on every fibre. Over a
complex model at n = ∞ this is a biholomorphism of total spaces.
Instances For
Pulling back along a composite is pulling back in two steps: for C^m maps
f : B'' → B' and g : B' → B, the total spaces of (g ∘ f) *ᵖ E and f *ᵖ (g *ᵖ E) are
C^n diffeomorphic, for any m and n, by the identity on every fibre E (g (f x)).
Instances For
Under compDiffeomorph, the canonical map of the composite pullback is the composite of the
canonical maps of the two steps.
If f is a C^n local diffeomorphism at x and m ≤ n, a section σ of E is C^m at
f x exactly when its pullback y ↦ σ (f y), a section of f *ᵖ E, is C^m at x.
If f is a surjective C^n local diffeomorphism and m ≤ n, a section σ of E is C^m
exactly when its pullback y ↦ σ (f y), a section of f *ᵖ E, is C^m.
A section of Hom between two pullbacks is Cⁿ exactly when its field of maps along the
base map is Cⁿ in the original hom bundle. No rank or smooth-bundle assumption is needed.