The weak Whitney topology in one global chart

For maps between normed spaces, the weak Whitney C^n topology is the initial topology for all iterated derivatives of order at most n, each regarded as a continuous map with the compact-open topology. Thus a family converges precisely when every derivative converges uniformly on compact sets (in the compact-open sense).

This is the global-chart building block for the weak Whitney topology on smooth maps between manifolds. On a manifold, the same construction is applied to coordinate representatives on compact subsets of chart domains. In particular, the n = ∞ instance below supplies the chart-level topology used to topologize diffeomorphism groups.

We also characterize continuity of arbitrary families by their compact-open derivative maps. When E is locally compact, this is equivalent to joint continuity of every spatial derivative; no differentiability in the parameter is required for this characterization.

Main definitions

• ContMDiffMap.iteratedFDerivContinuousMap: the kth derivative of a bundled C^n map, bundled as a continuous map.
• ContMDiffMap.weakWhitneyJet: the family of all compact-open-valued derivatives through order n.
• ContMDiffMap.weakWhitneyTopology: the initial topology induced by the compact-open topologies of all derivatives through order n.

Main results

• ContMDiffMap.continuous_iteratedFDerivContinuousMap: every derivative projection is continuous for the weak Whitney topology.
• ContMDiffMap.continuous_toContinuousMap: forgetting differentiability continuously maps the weak Whitney topology to the compact-open topology.
• ContMDiffMap.isInducing_weakWhitneyJet: the weak Whitney topology is exactly the topology induced by the full jet.
• ContMDiffMap.isEmbedding_weakWhitneyJet: the full jet realizes the weak Whitney map space as a subspace of the product of compact-open map spaces.
• ContMDiffMap.tendsto_weakWhitney_iff: convergence is equivalent to compact-open convergence of every derivative through order n.
• ContMDiffMap.tendsto_weakWhitney_iff_eventually_mapsTo: the same criterion in terms of the compact-open subbasic sets.

The construction follows M. Hirsch, Differential Topology, Graduate Texts in Mathematics 33, Chapter 2, §1, specialized to maps whose source and target each have one global chart.

noncomputable def ContMDiffMap.iteratedFDerivContinuousMap {k : Type u_1} [NontriviallyNormedField k] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace k E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace k F] {n : WithTop ℕ∞} (f : ContMDiffMap (modelWithCornersSelf k E) (modelWithCornersSelf k F) E F n) (m : ℕ) (hm : ↑m ≤ n) : C(E, E [×m]→L[k] F)

The mth derivative of a bundled C^n map between normed spaces, bundled as a continuous map. The bound m ≤ n is exactly what makes this derivative continuous.

Equations

• f.iteratedFDerivContinuousMap m hm = { toFun := fun (x : E) => iteratedFDeriv k m (⇑f) x, continuous_toFun := ⋯ }

@[simp]

theorem ContMDiffMap.iteratedFDerivContinuousMap_apply {k : Type u_1} [NontriviallyNormedField k] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace k E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace k F] {n : WithTop ℕ∞} (f : ContMDiffMap (modelWithCornersSelf k E) (modelWithCornersSelf k F) E F n) (m : ℕ) (hm : ↑m ≤ n) (x : E) : (f.iteratedFDerivContinuousMap m hm) x = iteratedFDeriv k m (⇑f) x

noncomputable def ContMDiffMap.weakWhitneyJet {k : Type u_1} [NontriviallyNormedField k] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace k E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace k F] {n : WithTop ℕ∞} (f : ContMDiffMap (modelWithCornersSelf k E) (modelWithCornersSelf k F) E F n) (m : { m : ℕ // ↑m ≤ n }) : C(E, E [×↑m]→L[k] F)

The weak Whitney C^n jet of a bundled map is the family of its derivatives of every order at most n, each bundled as a continuous map with the compact-open topology.

Equations

• f.weakWhitneyJet m = f.iteratedFDerivContinuousMap ↑m ⋯

@[simp]

theorem ContMDiffMap.weakWhitneyJet_apply {k : Type u_1} [NontriviallyNormedField k] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace k E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace k F] {n : WithTop ℕ∞} (f : ContMDiffMap (modelWithCornersSelf k E) (modelWithCornersSelf k F) E F n) (m : { m : ℕ // ↑m ≤ n }) : f.weakWhitneyJet m = f.iteratedFDerivContinuousMap ↑m ⋯

@[instance_reducible]

noncomputable def ContMDiffMap.weakWhitneyTopology {k : Type u_1} [NontriviallyNormedField k] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace k E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace k F] {n : WithTop ℕ∞} : TopologicalSpace (ContMDiffMap (modelWithCornersSelf k E) (modelWithCornersSelf k F) E F n)

The weak Whitney C^n topology on bundled C^n maps between normed spaces. It is the coarsest topology making the compact-open-valued derivative maps of every order m ≤ n continuous.

Equations

• ContMDiffMap.weakWhitneyTopology = TopologicalSpace.induced ContMDiffMap.weakWhitneyJet inferInstance

@[instance_reducible]

noncomputable instance ContMDiffMap.instTopologicalSpaceWeakWhitney {k : Type u_1} [NontriviallyNormedField k] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace k E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace k F] {n : WithTop ℕ∞} : TopologicalSpace (ContMDiffMap (modelWithCornersSelf k E) (modelWithCornersSelf k F) E F n)

Bundled C^n maps between normed spaces carry the weak Whitney topology.

Equations

• ContMDiffMap.instTopologicalSpaceWeakWhitney = ContMDiffMap.weakWhitneyTopology

theorem ContMDiffMap.continuous_weakWhitneyJet {k : Type u_1} [NontriviallyNormedField k] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace k E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace k F] {n : WithTop ℕ∞} : Continuous weakWhitneyJet

The full weak Whitney jet is continuous.

theorem ContMDiffMap.continuous_iteratedFDerivContinuousMap {k : Type u_1} [NontriviallyNormedField k] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace k E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace k F] {n : WithTop ℕ∞} (m : ℕ) (hm : ↑m ≤ n) : Continuous fun (f : ContMDiffMap (modelWithCornersSelf k E) (modelWithCornersSelf k F) E F n) => f.iteratedFDerivContinuousMap m hm

The mth derivative map from the weak Whitney C^n topology to the compact-open topology is continuous.

theorem ContMDiffMap.continuous_toContinuousMap {k : Type u_1} [NontriviallyNormedField k] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace k E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace k F] {n : WithTop ℕ∞} : Continuous fun (f : ContMDiffMap (modelWithCornersSelf k E) (modelWithCornersSelf k F) E F n) => ↑f

Forgetting the derivatives is a continuous map from the weak Whitney C^n topology to the compact-open topology on continuous maps. This is the order-zero derivative projection, followed by the canonical identification of zero-linear maps with their values.

theorem ContMDiffMap.weakWhitneyJet_injective {k : Type u_1} [NontriviallyNormedField k] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace k E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace k F] {n : WithTop ℕ∞} : Function.Injective weakWhitneyJet

The weak Whitney jet remembers the original map: its derivative of order zero is the map itself, viewed as a zero-linear map.

theorem ContMDiffMap.isInducing_weakWhitneyJet {k : Type u_1} [NontriviallyNormedField k] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace k E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace k F] {n : WithTop ℕ∞} : Topology.IsInducing weakWhitneyJet

The weak Whitney topology is exactly the topology induced by the full jet.

theorem ContMDiffMap.isEmbedding_weakWhitneyJet {k : Type u_1} [NontriviallyNormedField k] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace k E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace k F] {n : WithTop ℕ∞} : Topology.IsEmbedding weakWhitneyJet

The full jet is a topological embedding of the weak Whitney map space into the product of its compact-open derivative spaces.

instance ContMDiffMap.instT2SpaceWeakWhitney {k : Type u_1} [NontriviallyNormedField k] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace k E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace k F] {n : WithTop ℕ∞} : T2Space (ContMDiffMap (modelWithCornersSelf k E) (modelWithCornersSelf k F) E F n)

The weak Whitney topology on C^n maps between normed spaces is Hausdorff.

theorem ContMDiffMap.tendsto_weakWhitney_iff {k : Type u_1} [NontriviallyNormedField k] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace k E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace k F] {n : WithTop ℕ∞} {X : Type u_4} {l : Filter X} {f : X → ContMDiffMap (modelWithCornersSelf k E) (modelWithCornersSelf k F) E F n} {g : ContMDiffMap (modelWithCornersSelf k E) (modelWithCornersSelf k F) E F n} : Filter.Tendsto f l (nhds g) ↔ ∀ (m : ℕ) (hm : ↑m ≤ n), Filter.Tendsto (fun (x : X) => (f x).iteratedFDerivContinuousMap m hm) l (nhds (g.iteratedFDerivContinuousMap m hm))

A family of C^n maps converges in the weak Whitney topology exactly when every derivative through order n converges in the compact-open topology.

theorem ContMDiffMap.tendsto_weakWhitney_iff_eventually_mapsTo {k : Type u_1} [NontriviallyNormedField k] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace k E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace k F] {n : WithTop ℕ∞} {X : Type u_4} {l : Filter X} {f : X → ContMDiffMap (modelWithCornersSelf k E) (modelWithCornersSelf k F) E F n} {g : ContMDiffMap (modelWithCornersSelf k E) (modelWithCornersSelf k F) E F n} : Filter.Tendsto f l (nhds g) ↔ ∀ (m : ℕ) (hm : ↑m ≤ n) (K : Set E), IsCompact K → ∀ (U : Set (E [×m]→L[k] F)), IsOpen U → Set.MapsTo (⇑(g.iteratedFDerivContinuousMap m hm)) K U → ∀ᶠ (x : X) in l, Set.MapsTo (⇑((f x).iteratedFDerivContinuousMap m hm)) K U

The weak Whitney convergence criterion written using compact-open subbasic sets: for every derivative order, compact set, and open target containing the limiting derivative on that compact, the derivatives of the family eventually have the same containment.