Smoothness of maps into an open submanifold

A map into an open submanifold U ⊆ M is C^n exactly when its composition with the inclusion U → M is C^n: the charts of U are restrictions of the charts of M, so smoothness is insensitive to whether the codomain is read in the submanifold or in the ambient manifold.

Mathlib records this through ContMDiffWithinAt.subtypeVal_comp_iff within a set and through ContMDiffAt.subtypeVal_comp_iff at a point, both at regularity ∞. Since smoothness into a manifold is a local invariant property at every regularity, the same characterizations hold for arbitrary n; this file supplies them. In a convex open subset of a normed real space, these characterizations show that the clamped affine segment is C^n on [0, 1] at every regularity.

Main results

• TauCeti.ContMDiffWithinAt.subtypeVal_comp_iff, TauCeti.ContMDiffAt.subtypeVal_comp_iff, TauCeti.ContMDiffOn.subtypeVal_comp_iff, and TauCeti.ContMDiff.subtypeVal_comp_iff: a map into an open submanifold is C^n (within a set, at a point, on a set, globally) iff its composition with the inclusion is.
• TopologicalSpace.Opens.contMDiffOn_convexSegment: the affine segment in a convex open subset of a normed real space is smooth on [0, 1] at every regularity.

References

• Used to lift ambient curves (e.g. straight segments) to C¹ curves in open submanifolds; see TauCeti.Geometry.Manifold.Riemannian.Convex.

@[simp]

theorem TauCeti.ContMDiffWithinAt.subtypeVal_comp_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : WithTop ℕ∞} (U : TopologicalSpace.Opens M') (f : M → ↥U) (s : Set M) (x : M) : ContMDiffWithinAt I I' n (Subtype.val ∘ f) s x ↔ ContMDiffWithinAt I I' n f s x

A map into an open submanifold is C^n within a set at a point iff its composition with the inclusion is, at every regularity: smoothness is a local invariant property and the charts agree.

@[simp]

theorem TauCeti.ContMDiffAt.subtypeVal_comp_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : WithTop ℕ∞} (U : TopologicalSpace.Opens M') (f : M → ↥U) (x : M) : ContMDiffAt I I' n (Subtype.val ∘ f) x ↔ ContMDiffAt I I' n f x

A map into an open submanifold is C^n at a point iff its composition with the inclusion is, at every regularity.

@[simp]

theorem TauCeti.ContMDiffOn.subtypeVal_comp_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : WithTop ℕ∞} (U : TopologicalSpace.Opens M') (f : M → ↥U) (s : Set M) : ContMDiffOn I I' n (Subtype.val ∘ f) s ↔ ContMDiffOn I I' n f s

A map into an open submanifold is C^n on a set iff its composition with the inclusion is, at every regularity.

@[simp]

theorem TauCeti.ContMDiff.subtypeVal_comp_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : WithTop ℕ∞} (U : TopologicalSpace.Opens M') (f : M → ↥U) : ContMDiff I I' n (Subtype.val ∘ f) ↔ ContMDiff I I' n f

A map into an open submanifold is C^n iff its composition with the inclusion is, at every regularity.

theorem TopologicalSpace.Opens.contMDiffOn_convexSegment {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (U : Opens F) {n : WithTop ℕ∞} (hU : Convex ℝ ↑U) (x y : ↥U) : ContMDiffOn (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ F) n ((↑U).convexSegment hU x y) (Set.Icc 0 1)

The clamped affine segment in a convex open subset is C^n on [0, 1] for every n.