Interactions between differentiability, smoothness and manifold derivatives #
We give the relation between MDifferentiable, ContMDiff, mfderiv, tangentMap
and related notions.
Main statements #
ContMDiffOn.contMDiffOn_tangentMapWithinstates that the bundled derivative of aCⁿfunction in a domain isCᵐwhenm + 1 ≤ n.ContMDiff.contMDiff_tangentMapstates that the bundled derivative of aCⁿfunction isCᵐwhenm + 1 ≤ n.
Definition of smooth functions between manifolds #
The derivative of a smooth function is smooth #
The function that sends x to the y-derivative of f(x,y) at g(x) is C^m at x₀,
where the derivative is taken as a continuous linear map.
We have to assume that f is C^n at (x₀, g(x₀)) for n ≥ m + 1 and g is C^m at x₀.
We have to insert a coordinate change from x₀ to x to make the derivative sensible.
This result is used to show that maps into the 1-jet bundle and cotangent bundle are smooth.
ContMDiffAt.mfderiv_const is a special case of this.
This result should be generalized to a ContMDiffWithinAt for mfderivWithin.
If we do that, we can deduce ContMDiffOn.contMDiffOn_tangentMapWithin from this.
The derivative D_yf(y) is C^m at x₀, where the derivative is taken as a continuous
linear map. We have to assume that f is C^n at x₀ for some n ≥ m + 1.
We have to insert a coordinate change from x₀ to x to make the derivative sensible.
This is a special case of ContMDiffAt.mfderiv where f does not contain any parameters and
g = id.
The function that sends x to the y-derivative of f(x,y) at g(x) applied to g₂(x) is
C^n at x₀, where the derivative is taken as a continuous linear map.
We have to assume that f is C^(n+1) at (x₀, g(x₀)) and g is C^n at x₀.
We have to insert a coordinate change from x₀ to g₁(x) to make the derivative sensible.
This is similar to ContMDiffAt.mfderiv, but where the continuous linear map is applied to a
(variable) vector.
The tangent map of a smooth function is smooth #
If a function is C^n with 1 ≤ n on a domain with unique derivatives, then its bundled
derivative is continuous. In this auxiliary lemma, we prove this fact when the source and target
space are model spaces in models with corners. The general fact is proved in
ContMDiffOn.continuousOn_tangentMapWithin
If a function is C^n on a domain with unique derivatives, then its bundled derivative is
C^m when m+1 ≤ n. In this auxiliary lemma, we prove this fact when the source and target space
are model spaces in models with corners. The general fact is proved in
ContMDiffOn.contMDiffOn_tangentMapWithin
If a function is C^n on a domain with unique derivatives, then its bundled derivative
is C^m when m+1 ≤ n.
If a function is C^n on a domain with unique derivatives, with 1 ≤ n, then its bundled
derivative is continuous there.
If a function is C^n, then its bundled derivative is C^m when m+1 ≤ n.
If a function is C^n, with 1 ≤ n, then its bundled derivative is continuous.
The derivative of the zero section of the tangent bundle maps ⟨x, v⟩ to ⟨⟨x, 0⟩, ⟨v, 0⟩⟩.
Note that, as currently framed, this is a statement in coordinates, thus reliant on the choice of the coordinate system we use on the tangent bundle.
However, the result itself is coordinate-dependent only to the extent that the coordinates determine a splitting of the tangent bundle. Moreover, there is a canonical splitting at each point of the zero section (since there is a canonical horizontal space there, the tangent space to the zero section, in addition to the canonical vertical space which is the kernel of the derivative of the projection), and this canonical splitting is also the one that comes from the coordinates on the tangent bundle in our definitions. So this statement is not as crazy as it may seem.
TODO define splittings of vector bundles; state this result invariantly.