Smooth families of manifold-valued maps are continuous

A jointly C^n map P × M → N between manifolds is a family of C^n maps M → N indexed by P, and this file proves that the family is continuous for the weak Whitney topology on C^n⟮I, M; J, N⟯. This is the direction that turns the object a proof produces, a smooth map on a product, into the object a homotopy-theoretic statement needs, a map into a function space. Nothing is claimed in the reverse direction: an arbitrary continuous family into the map space need not be smooth on the product.

A weak Whitney basic set only constrains a map where it meets a fixed target chart, so the coordinate representative of the family is defined only on the open set of parameters and chart points at which the family is visible in that chart. The representative is differentiated there by ContMDiff.continuousOn_iteratedFDerivWithin_extChartAt, and the continuity statement then follows from a tube lemma turning pointwise membership in a derivative test into a parameter neighbourhood. When both source and target are normed spaces, this topology is identified with the global-derivative topology by ContMDiffMap.manifoldWeakWhitneyTopology_self.

Use open scoped TauCeti.ManifoldWeakWhitney to select the topology these statements are about.

Main results

• Continuous.isOpen_setOf_mem_extChartAt_source: the parameters and chart points at which a continuous map on P × M is visible in a target chart form an open set.
• ContMDiff.continuousOn_iteratedFDerivWithin_extChartAt: there the coordinate derivative of the family depends continuously on the parameter and the chart point jointly.
• ContMDiff.continuous_manifoldWeakWhitney: joint C^n regularity gives continuity into the weak Whitney topology.
• ContMDiffMap.manifoldWeakWhitneyCurry: the resulting continuous family, bundled.

The weak topology convention follows M. Hirsch, Differential Topology, GTM 33, Chapter 2, §1.

theorem Continuous.isOpen_setOf_mem_extChartAt_source {𝕜 : 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] {P : Type u_7} [TopologicalSpace P] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_9} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [TopologicalSpace N] [ChartedSpace G N] {g : P × M → N} (hg : Continuous g) (x : M) (y : N) : IsOpen {z : P × ↑(extChartAt I x).target | g (z.1, ↑(extChartAt I x).symm ↑z.2) ∈ (extChartAt J y).source}

The parameters and source-chart points at which a continuous map on P × M, read as a family of maps M → N, is visible in the extended chart around y form an open set. Exactly there is the coordinate representative of the family, and hence the derivative tested by ContMDiffMap.chartJetSet, defined.

theorem ContMDiff.continuousOn_iteratedFDerivWithin_extChartAt {𝕜 : 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'} {P : Type u_7} [TopologicalSpace P] [ChartedSpace H' P] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_9} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold I' n P] [IsManifold J n N] {g : P × M → N} (hg : ContMDiff (I'.prod I) J n g) (x : M) (y : N) (m : ℕ) (hm : ↑m ≤ n) : ContinuousOn (fun (z : P × ↑(extChartAt I x).target) => iteratedFDerivWithin 𝕜 m (fun (b : E) => ↑(extChartAt J y) (g (z.1, ↑(extChartAt I x).symm b))) (extChartAt I x).target ↑z.2) {z : P × ↑(extChartAt I x).target | g (z.1, ↑(extChartAt I x).symm ↑z.2) ∈ (extChartAt J y).source}

On the open set where a jointly C^n map on P × M, read as a family of maps M → N, is visible in the extended chart around y, the m-th coordinate derivative of the family depends continuously on the parameter and the source-chart point jointly. The derivative is taken within the whole extended source chart target, as the weak Whitney tests take it, so boundary and corner points are covered.

theorem ContMDiff.continuous_manifoldWeakWhitney {𝕜 : 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'} {P : Type u_7} [TopologicalSpace P] [ChartedSpace H' P] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_9} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold I' n P] [IsManifold J n N] {f : P → ContMDiffMap I J M N n} (hf : ContMDiff (I'.prod I) J n fun (z : P × M) => (f z.1) z.2) : Continuous f

Joint C^n regularity gives continuity into the weak Whitney topology on manifold-valued C^n maps. Neither compactness nor absence of boundary is required of the parameter, the source or the target.

noncomputable def ContMDiffMap.manifoldWeakWhitneyCurry {𝕜 : 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'} {P : Type u_7} [TopologicalSpace P] [ChartedSpace H' P] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_9} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold I' n P] [IsManifold J n N] (f : ContMDiffMap (I'.prod I) J (P × M) N n) : C(P, ContMDiffMap I J M N n)

Curry a jointly C^n map on a product of manifolds into a continuous family of C^n maps, for the weak Whitney topology on the space of manifold-valued C^n maps.

Equations

• f.manifoldWeakWhitneyCurry = { toFun := fun (p : P) => ⟨fun (x : M) => f (p, x), ⋯⟩, continuous_toFun := ⋯ }

@[simp]

theorem ContMDiffMap.manifoldWeakWhitneyCurry_apply {𝕜 : 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'} {P : Type u_7} [TopologicalSpace P] [ChartedSpace H' P] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_9} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold I' n P] [IsManifold J n N] (f : ContMDiffMap (I'.prod I) J (P × M) N n) (p : P) (x : M) : (f.manifoldWeakWhitneyCurry p) x = f (p, x)

Evaluating the curried family at p and x recovers f (p, x).