Unique derivative sets in manifolds

In this file, we prove various properties of unique derivative sets in manifolds.

• image_denseRange: suppose f is differentiable on s and its derivative at every point of s has dense range. If s has the unique differential property, then so does f '' s.
• uniqueMDiffOn_preimage: the unique differential property is preserved by local diffeomorphisms
• uniqueDiffOn_target_inter: the unique differential property is preserved by pullbacks of extended charts
• tangentBundle_proj_preimage: if s has the unique differential property, its preimage under the tangent bundle projection also has

Unique derivative sets in manifolds

theorem UniqueMDiffWithinAt.image_denseRange {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {s : Set M} {x : M} (hs : UniqueMDiffWithinAt I s x) {f : M → M'} {f' : E →L[𝕜] E'} (hf : HasMFDerivWithinAt I I' f s x f') (hd : DenseRange ⇑f') : UniqueMDiffWithinAt I' (f '' s) (f x)

If s has the unique differential property at x, f is differentiable within s at xand its derivative has dense range, thenf '' shas the unique differential property atf x`.

theorem UniqueMDiffOn.image_denseRange' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {s : Set M} (hs : UniqueMDiffOn I s) {f : M → M'} {f' : M → E →L[𝕜] E'} (hf : ∀ x ∈ s, HasMFDerivWithinAt I I' f s x (f' x)) (hd : ∀ x ∈ s, DenseRange ⇑(f' x)) : UniqueMDiffOn I' (f '' s)

If s has the unique differential property, f is differentiable on s and its derivative at every point of s has dense range, then f '' s has the unique differential property. This version uses the HasMFDerivWithinAt predicate.

theorem UniqueMDiffOn.image_denseRange {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {s : Set M} (hs : UniqueMDiffOn I s) {f : M → M'} (hf : MDifferentiableOn I I' f s) (hd : ∀ x ∈ s, DenseRange ⇑(mfderivWithin I I' f s x)) : UniqueMDiffOn I' (f '' s)

If s has the unique differential property, f is differentiable on s and its derivative at every point of s has dense range, then f '' s has the unique differential property.

theorem UniqueMDiffWithinAt.preimage_partialHomeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {s : Set M} {x : M} (hs : UniqueMDiffWithinAt I s x) {e : PartialHomeomorph M M'} (he : PartialHomeomorph.MDifferentiable I I' e) (hx : x ∈ e.source) : UniqueMDiffWithinAt I' (e.target ∩ ↑e.symm ⁻¹' s) (↑e x)

theorem UniqueMDiffOn.uniqueMDiffOn_preimage {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {s : Set M} (hs : UniqueMDiffOn I s) {e : PartialHomeomorph M M'} (he : PartialHomeomorph.MDifferentiable I I' e) : UniqueMDiffOn I' (e.target ∩ ↑e.symm ⁻¹' s)

If a set has the unique differential property, then its image under a local diffeomorphism also has the unique differential property.

theorem UniqueMDiffOn.uniqueDiffOn_target_inter {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} [SmoothManifoldWithCorners I M] (hs : UniqueMDiffOn I s) (x : M) : UniqueDiffOn 𝕜 ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)

If a set in a manifold has the unique derivative property, then its pullback by any extended chart, in the vector space, also has the unique derivative property.

theorem UniqueMDiffOn.uniqueDiffOn_inter_preimage {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M'' : Type u_8} [TopologicalSpace M''] [ChartedSpace H' M''] {s : Set M} [SmoothManifoldWithCorners I M] (hs : UniqueMDiffOn I s) (x : M) (y : M'') {f : M → M''} (hf : ContinuousOn f s) : UniqueDiffOn 𝕜 ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))

When considering functions between manifolds, this statement shows up often. It entails the unique differential of the pullback in extended charts of the set where the function can be read in the charts.

theorem Trivialization.mdifferentiable {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_9} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {Z : M → Type u_10} [TopologicalSpace (Bundle.TotalSpace F Z)] [(b : M) → TopologicalSpace (Z b)] [(b : M) → AddCommMonoid (Z b)] [(b : M) → Module 𝕜 (Z b)] [FiberBundle F Z] [VectorBundle 𝕜 F Z] [SmoothVectorBundle F Z I] (e : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] : PartialHomeomorph.MDifferentiable (I.prod (modelWithCornersSelf 𝕜 F)) (I.prod (modelWithCornersSelf 𝕜 F)) e.toPartialHomeomorph

theorem UniqueMDiffWithinAt.smooth_bundle_preimage {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {F : Type u_9} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {Z : M → Type u_10} [TopologicalSpace (Bundle.TotalSpace F Z)] [(b : M) → TopologicalSpace (Z b)] [(b : M) → AddCommMonoid (Z b)] [(b : M) → Module 𝕜 (Z b)] [FiberBundle F Z] [VectorBundle 𝕜 F Z] [SmoothVectorBundle F Z I] {p : Bundle.TotalSpace F Z} (hs : UniqueMDiffWithinAt I s p.proj) : UniqueMDiffWithinAt (I.prod (modelWithCornersSelf 𝕜 F)) (Bundle.TotalSpace.proj ⁻¹' s) p

theorem UniqueMDiffWithinAt.smooth_bundle_preimage' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {F : Type u_9} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (Z : M → Type u_10) [TopologicalSpace (Bundle.TotalSpace F Z)] [(b : M) → TopologicalSpace (Z b)] [(b : M) → AddCommMonoid (Z b)] [(b : M) → Module 𝕜 (Z b)] [FiberBundle F Z] [VectorBundle 𝕜 F Z] [SmoothVectorBundle F Z I] {b : M} (hs : UniqueMDiffWithinAt I s b) (x : Z b) : UniqueMDiffWithinAt (I.prod (modelWithCornersSelf 𝕜 F)) (Bundle.TotalSpace.proj ⁻¹' s) { proj := b, snd := x }

theorem UniqueMDiffOn.smooth_bundle_preimage {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {F : Type u_9} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (Z : M → Type u_10) [TopologicalSpace (Bundle.TotalSpace F Z)] [(b : M) → TopologicalSpace (Z b)] [(b : M) → AddCommMonoid (Z b)] [(b : M) → Module 𝕜 (Z b)] [FiberBundle F Z] [VectorBundle 𝕜 F Z] [SmoothVectorBundle F Z I] (hs : UniqueMDiffOn I s) : UniqueMDiffOn (I.prod (modelWithCornersSelf 𝕜 F)) (Bundle.TotalSpace.proj ⁻¹' s)

In a smooth fiber bundle, the preimage under the projection of a set with unique differential in the basis also has unique differential.