Differentiability of models with corners and (extended) charts #
In this file, we analyse the differentiability of charts, models with corners and extended charts. We show that
- models with corners are differentiable
- charts are differentiable on their source
mdifferentiableOn_extChartAt
:extChartAt
is differentiable on its source
Suppose a partial homeomorphism e
is differentiable. This file shows
PartialHomeomorph.MDifferentiable.mfderiv
: its derivative is a continuous linear equivalencePartialHomeomorph.MDifferentiable.mfderiv_bijective
: its derivative is bijective; there are also spelling with trivial kernel and full range
In particular, (extended) charts have bijective differential.
Tags #
charts, differentiable, bijective
Model with corners #
The derivative of the chart at a base point is the chart of the tangent bundle, composed with the identification between the tangent bundle of the model space and the product space.
The derivative of the inverse of the chart at a base point is the inverse of the chart of the tangent bundle, composed with the identification between the tangent bundle of the model space and the product space.
Differentiable partial homeomorphisms #
The derivative of a differentiable partial homeomorphism, as a continuous linear equivalence
between the tangent spaces at x
and e x
.