Constancy from a vanishing manifold differential

A differentiable map with zero differential on an open subset of a real manifold is locally constant there. Both manifolds may have boundary or corners, and neither needs to be finite dimensional. On a preconnected source the map is constant. Conversely, a locally constant map is smooth (IsLocallyConstant.contMDiff).

These results turn infinitesimal independence of a parameter into independence of that parameter itself, for example when separating the factors of a product isometry. The argument applies Mathlib's Convex.is_const_of_fderivWithin_eq_zero in source and target charts, on a ball intersected with the convex range of the source model.

theorem MDifferentiableOn.eventuallyEq_const_of_mfderiv_eq_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {H : Type u_3} {G : Type u_4} [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners ℝ E H} {J : ModelWithCorners ℝ F G} {M : Type u_5} {N : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold I 1 M] [IsManifold J 1 N] {f : M → N} {s : Set M} (hf : MDiff[s] f) (hs : IsOpen s) (hzero : ∀ y ∈ s, mfderiv% f y = 0) {x : M} (hx : x ∈ s) : f =ᶠ[nhds x] fun (x_1 : M) => f x

A differentiable map with zero differential on an open set agrees locally with its value at each point of that set. Both manifolds may have boundary or corners.

theorem MDifferentiable.isLocallyConstant_of_mfderiv_eq_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {H : Type u_3} {G : Type u_4} [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners ℝ E H} {J : ModelWithCorners ℝ F G} {M : Type u_5} {N : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold I 1 M] [IsManifold J 1 N] {f : M → N} (hf : MDiff f) (hzero : ∀ (x : M), mfderiv% f x = 0) : IsLocallyConstant f

A differentiable map from a real manifold with zero differential is locally constant. The source may have boundary or corners.

theorem MDifferentiable.apply_eq_of_mfderiv_eq_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {H : Type u_3} {G : Type u_4} [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners ℝ E H} {J : ModelWithCorners ℝ F G} {M : Type u_5} {N : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold I 1 M] [IsManifold J 1 N] {f : M → N} [PreconnectedSpace M] (hf : MDiff f) (hzero : ∀ (x : M), mfderiv% f x = 0) (x y : M) : f x = f y

A differentiable map with zero differential on a preconnected real manifold takes the same value at every two points.

theorem IsLocallyConstant.contMDiff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} {G : Type u_5} [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} {N : Type u_7} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {f : M → N} (hf : IsLocallyConstant f) {n : WithTop ℕ∞} : ContMDiff I J n f

Conversely, a locally constant map between manifolds is C^n for every n: near each point it agrees with a constant map.