Smooth bundles of continuous alternating maps #
Continuous alternating maps between two smooth vector bundles form a smooth vector bundle. This equips the bundles underlying differential forms with smooth coordinate changes, without changing Mathlib's topology, trivializations, or atlas.
Mathlib's Mathlib.Geometry.Manifold.VectorBundle.ContinuousAlternatingMap provides the
same construction over characteristic-zero fields, together with the fibre-coordinate
regularity criteria such as contMDiffAt_continuousAlternatingMap_bundle. The results here
remove the characteristic-zero assumption.
A family of alternating maps of two vectors whose values are given by a C^n section of the
bundle of bilinear maps is itself a C^n section of the alternating-map bundle
(TauCeti.contMDiffAt_continuousAlternatingMap_bundle_of_bilinear). This lets a two-form be
built from a smooth bilinear tensor field without repeating a coordinate computation.
The coordinate-change proof follows Floris van Doorn's smooth Hom-bundle construction
in Mathlib.Geometry.Manifold.VectorBundle.Hom, using the topological alternating-map
bundle of Yury Kudryashov, Heather Macbeth, and Floris van Doorn. Its domain pullback is
smooth, while its codomain postcomposition is continuous linear. The construction
works over every nontrivially normed field at finite orders and ā. At the analytic
order Ļ, the construction assumes a nonzero arity factorial, automatically including
characteristic-zero fields. Models with corners are arbitrary, with no dimension or
completeness assumptions.
Coordinate changes of the alternating-map bundle have the same regularity as the
coordinate changes of its domain and codomain bundles, provided the arity factorial is
nonzero in š at the analytic order Ļ. Finite orders and ā have no characteristic
restriction.
Mathlib's alternating-map vector prebundle has smooth coordinate changes.
The analytic order Ļ requires a nonzero arity factorial in š.
When the arity factorial is nonzero in š, the alternating-map prebundle has C^n
coordinate changes at every order n, including Ļ.
Smooth coordinate changes of Mathlib's alternating-map prebundle induce a C^n
vector bundle with its existing topology and atlas.
Coordinate changes of the alternating-map bundle are differentiable when the domain and
codomain bundles have C^1 coordinate changes.
At finite orders and ā, alternating-map coordinate changes are smooth in every
characteristic.
A family of alternating maps of two vectors whose values are given by a C^n section of
the bundle of bilinear maps is a C^n section of the alternating-map bundle.