The weak Whitney topology for manifold-valued maps

A compact derivative test fixes source and target charts, a compact subset of the source chart target, a derivative order, and an open set of multilinear maps. A map passes the test when it carries the compact set into the target chart and its coordinate derivative lies in the prescribed open set. The topology generated by these tests is the weak Whitney topology. Derivatives are taken within the extended source chart target, including at boundary and corner points; values outside the target chart never enter a test.

For maps between normed spaces, this agrees with the global weak Whitney topology. Evaluation is continuous, so the map space is Hausdorff when the target is Hausdorff. The topology is not a global function-space instance; use open scoped TauCeti.ManifoldWeakWhitney to select it, which also supplies the Hausdorff instance.

The construction follows M. Hirsch, Differential Topology, GTM 33, Chapter 2, §1, pp. 34–36: the compact-open tests on each derivative generate the weak topology. On compact source manifolds this is also the strong Whitney topology.

def ContMDiffMap.chartJetSet {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] [hI : IsManifold I n M] [hJ : IsManifold J n N] (x : M) (y : N) (m : ℕ) (K : Set ↑(extChartAt I x).target) (V : Set (E [×m]→L[𝕜] F)) : Set (ContMDiffMap I J M N n)

A chart derivative test. Each tested point must map into the chosen target chart; only there is its coordinate derivative used. Compactness and openness are imposed when these sets generate the weak Whitney topology.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContMDiffMap.mem_chartJetSet {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] [IsManifold I n M] [IsManifold J n N] {x : M} {y : N} {m : ℕ} {K : Set ↑(extChartAt I x).target} {V : Set (E [×m]→L[𝕜] F)} {f : ContMDiffMap I J M N n} : f ∈ chartJetSet x y m K V ↔ ∀ z ∈ K, f (↑(extChartAt I x).symm ↑z) ∈ (extChartAt J y).source ∧ iteratedFDerivWithin 𝕜 m (↑(extChartAt J y) ∘ ⇑f ∘ ↑(extChartAt I x).symm) (extChartAt I x).target ↑z ∈ V

Membership in a chart derivative test records both chart validity and derivative control.

@[instance_reducible]

noncomputable def ContMDiffMap.manifoldWeakWhitneyTopology {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] [IsManifold I n M] [IsManifold J n N] : TopologicalSpace (ContMDiffMap I J M N n)

The weak Whitney topology on manifold-valued C^n maps, generated by compact-open coordinate-derivative tests of every finite order at most n.

Equations

• One or more equations did not get rendered due to their size.

theorem ContMDiffMap.isOpen_chartJetSet {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] [IsManifold I n M] [IsManifold J n N] (x : M) (y : N) (m : ℕ) (hm : ↑m ≤ n) {K : Set ↑(extChartAt I x).target} (hK : IsCompact K) {V : Set (E [×m]→L[𝕜] F)} (hV : IsOpen V) : IsOpen (chartJetSet x y m K V)

Compact chart derivative tests with open targets are open in the weak Whitney topology.

theorem ContMDiffMap.continuous_manifoldWeakWhitney_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] [IsManifold I n M] [IsManifold J n N] {P : Type u_8} [TopologicalSpace P] {g : P → ContMDiffMap I J M N n} : Continuous g ↔ ∀ (x : M) (y : N) (m : ℕ), ↑m ≤ n → ∀ (K : Set ↑(extChartAt I x).target), IsCompact K → ∀ (V : Set (E [×m]→L[𝕜] F)), IsOpen V → IsOpen (g ⁻¹' chartJetSet x y m K V)

A family is Whitney-continuous exactly when the inverse image of every compact chart derivative test is open.

theorem ContMDiffMap.tendsto_manifoldWeakWhitney_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] [IsManifold I n M] [IsManifold J n N] {P : Type u_8} {l : Filter P} {g : P → ContMDiffMap I J M N n} {f : ContMDiffMap I J M N n} : Filter.Tendsto g l (nhds f) ↔ ∀ (x : M) (y : N) (m : ℕ), ↑m ≤ n → ∀ (K : Set ↑(extChartAt I x).target), IsCompact K → ∀ (V : Set (E [×m]→L[𝕜] F)), IsOpen V → f ∈ chartJetSet x y m K V → ∀ᶠ (p : P) in l, g p ∈ chartJetSet x y m K V

Convergence is eventual membership in every compact chart derivative test passed by the limiting map.

theorem ContMDiffMap.continuous_eval_const_manifoldWeakWhitney {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] [IsManifold I n M] [IsManifold J n N] (x : M) : Continuous fun (f : ContMDiffMap I J M N n) => f x

Evaluation at a fixed source point is continuous for the manifold weak Whitney topology.

theorem ContMDiffMap.t2Space_manifoldWeakWhitney {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] [IsManifold I n M] [IsManifold J n N] [T2Space N] : T2Space (ContMDiffMap I J M N n)

A Hausdorff target gives a Hausdorff weak Whitney map space.

theorem ContMDiffMap.chartJetSet_self_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [IsManifold I n M] (x : M) (y : F) (m : ℕ) (hm : ↑m ≤ n) (K : Set ↑(extChartAt I x).target) (V : Set (E [×m]→L[𝕜] F)) : chartJetSet x y m K V = {f : ContMDiffMap I (modelWithCornersSelf 𝕜 F) M F n | Set.MapsTo (⇑(f.chartIteratedFDeriv x m hm)) K V}

For a vector-space target, chart tests are exactly compact-open tests on the existing source-chart derivative maps.

@[simp]

theorem ContMDiffMap.manifoldWeakWhitneyTopology_self {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] : manifoldWeakWhitneyTopology = weakWhitneyTopology

On maps between normed spaces, the manifold weak Whitney topology agrees with the existing topology defined using global iterated derivatives.