Invertible manifold derivatives of composites

If f has invertible manifold derivative at x and g has invertible manifold derivative at f x, then g ∘ f has invertible manifold derivative at x. No differentiability hypothesis is needed, since an invertible derivative forces differentiability (mdifferentiableAt_of_isInvertible_mfderiv), and no finite-dimensionality or smoothness of the manifolds is assumed.

Between manifolds modelled on finite-dimensional spaces of the same dimension over a complete field, an injective manifold derivative is invertible (isInvertible_mfderiv_of_injective). Conversely to the first statement, if the middle manifold is modelled on a finite-dimensional space and the target model has the same dimension, and a composite of differentiable maps has invertible manifold derivative, then so do both factors (isInvertible_mfderiv_of_isInvertible_mfderiv_comp); neither completeness of the field nor finite-dimensionality of the source or target model is assumed (the target is a quotient of the middle space).

If the source is modelled on a finite-dimensional space over a complete field and the derivative carries a tangent basis b onto a basis b', then it is the continuous linear equivalence mapping b to b' (exists_coe_eq_mfderiv_of_basis), so it is invertible (isInvertible_mfderiv_of_basis).

theorem TauCeti.isInvertible_mfderiv_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {H' : Type u_6} {M' : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] {E'' : Type u_8} {H'' : Type u_9} {M'' : Type u_10} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} [TopologicalSpace M''] [ChartedSpace H'' M''] {f : M → M'} {g : M' → M''} {x : M} (hdg : (mfderiv% g (f x)).IsInvertible) (hdf : (mfderiv% f x).IsInvertible) : (mfderiv% (g ∘ f) x).IsInvertible

A composite of maps with invertible manifold derivatives at x and f x has invertible manifold derivative at x.

theorem TauCeti.isInvertible_mfderiv_of_injective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {H' : Type u_6} {M' : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [CompleteSpace 𝕜] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 E'] {f : M → M'} {x : M} (hdim : Module.finrank 𝕜 E = Module.finrank 𝕜 E') (hinj : Function.Injective ⇑(mfderiv% f x)) : (mfderiv% f x).IsInvertible

Between manifolds modelled on finite-dimensional spaces of the same dimension over a complete field, an injective manifold derivative is invertible.

theorem TauCeti.isInvertible_mfderiv_of_isInvertible_mfderiv_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {H' : Type u_6} {M' : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] {E'' : Type u_8} {H'' : Type u_9} {M'' : Type u_10} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} [TopologicalSpace M''] [ChartedSpace H'' M''] [FiniteDimensional 𝕜 E'] {f : M → M'} {g : M' → M''} {x : M} (hdim : Module.finrank 𝕜 E' = Module.finrank 𝕜 E'') (hg : MDiffAt g (f x)) (hf : MDiffAt f x) (h : (mfderiv% (g ∘ f) x).IsInvertible) : (mfderiv% f x).IsInvertible ∧ (mfderiv% g (f x)).IsInvertible

Between manifolds whose middle model is finite-dimensional and whose target model has the same dimension, if a composite of differentiable maps has invertible manifold derivative, then so do both factors. The source and target models need not be assumed finite-dimensional (the target is a quotient of the middle space), and the field need not be complete.

theorem TauCeti.exists_coe_eq_mfderiv_of_basis {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {H' : Type u_6} {M' : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [CompleteSpace 𝕜] [FiniteDimensional 𝕜 E] {ι : Type u_11} {f : M → M'} {x : M} (b : Module.Basis ι 𝕜 (TangentSpace I x)) (b' : Module.Basis ι 𝕜 (TangentSpace I' (f x))) (hbb' : ∀ (i : ι), (mfderiv% f x) (b i) = b' i) : ∃ (e : TangentSpace I x ≃L[𝕜] TangentSpace I' (f x)), ↑e = mfderiv% f x ∧ b.map ↑e = b'

If the source is modelled on a finite-dimensional space over a complete field and the derivative at x carries a basis b of the tangent space at x to a basis b' of the tangent space at f x, then the derivative is a continuous linear equivalence mapping b to b'.

theorem TauCeti.isInvertible_mfderiv_of_basis {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {H' : Type u_6} {M' : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [CompleteSpace 𝕜] [FiniteDimensional 𝕜 E] {ι : Type u_11} {f : M → M'} {x : M} (b : Module.Basis ι 𝕜 (TangentSpace I x)) (b' : Module.Basis ι 𝕜 (TangentSpace I' (f x))) (hbb' : ∀ (i : ι), (mfderiv% f x) (b i) = b' i) : (mfderiv% f x).IsInvertible

If the source is modelled on a finite-dimensional space over a complete field and the derivative at x carries a basis b of the tangent space at x to a basis b' of the tangent space at f x, then it is invertible.