Testing smooth bundle homomorphisms on sections #

A section of a hom bundle with finite-dimensional source fibres is smooth if and only if it sends every globally smooth section to a smooth section. This turns smoothness of tensorial operations on sections into smoothness of the associated tensor field, by applying the criterion once for each argument.

The criterion applies over arbitrary smooth finite-dimensional manifolds, including noncompact manifolds and manifolds with boundary, and places no finite-dimensionality assumption on the target fibres.

Composition of differentiable Hom-bundle sections is differentiable, including within parameter sets (MDifferentiableWithinAt.clm_bundle_comp).

The file also records that pulling back a fixed continuous bilinear form on the model fibre along a trivialization gives a C^n field of bilinear forms over its base set (TauCeti.Manifold.contMDiffOn_trivializationAt_pullbackForm), conversely that a field of bilinear forms which is C^n at a point reads in the trivialization at that point as a family of bilinear forms on the model fibre which is C^n there (TauCeti.Manifold.exists_contMDiffAt_apply_eq_apply_symm). Over the whole base set of an atlas trivialization of a C^n vector bundle, a C^n field of bilinear forms reads as a C^n family of bilinear forms on the model fibre (Bundle.Trivialization.contMDiffOn_compl₁₂_symmₗ). Fibrewise inversion preserves smoothness of a hom-bundle section at every point where the section is invertible (ContMDiffWithinAt.clm_bundle_inverse and its variants). The latter is the bundle form of the smoothness of inversion of continuous linear maps between Banach spaces. A constant bilinear pairing between trivial bundles is a smooth hom-bundle section (TauCeti.contMDiff_const_bundlePairing). A hom-bundle section whose coordinate expressions are constant on the common frame domains is smooth (TauCeti.contMDiff_hom_bundle_of_inCoordinates_eq_const).

Fibrewise composition preserves joint Cⁿ regularity along any common base map (ContMDiff.clm_bundle_comp). The corresponding native section operation is ContMDiffSection.clmComp; it requires no finite rank or completeness assumption.

Negation of a hom-bundle section along any base map preserves its regularity (ContMDiff.clm_bundle_neg). Interchanging the inputs of a smooth bilinear bundle map preserves smoothness (ContMDiffWithinAt.clm_bundle_flip), without a choice of fibre norms. This permits contraction of a smooth tensor in any input slot.

Finally, a family of fibrewise linear maps with finite-dimensional model source is a C^n section of the hom bundle exactly when the map of total spaces it induces is C^n (TauCeti.contMDiff_hom_bundle_iff, with a pointwise version TauCeti.contMDiffAt_hom_bundle_iff); this needs neither bundle to be a C^n vector bundle. The same holds for families depending on a parameter in a manifold P, as sections along the projection P × B → B and maps P × TotalSpace F₁ E₁ → TotalSpace F₂ E₂ (TauCeti.contMDiff_hom_bundle_prod_iff, TauCeti.contMDiffAt_hom_bundle_prod_iff). Combined with fibrewise inversion, a C^n family of fibrewise linear equivalences therefore induces a C^n diffeomorphism of total spaces, TauCeti.bundleDiffeomorph, whose inverse is automatically C^n. Over the model 𝓘(ℂ, EB) with n = ∞, these are the holomorphic bundle morphisms and equivalences of holomorphic vector bundles. They are the C^n counterparts of TauCeti.continuous_hom_bundle_iff and TauCeti.bundleHomeomorph. A family of fibrewise linear maps is realized by a C^n diffeomorphism of total spaces exactly when its total-space map is C^n and its fibre maps are bijective (TauCeti.exists_bundleDiffeomorph_iff).