LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Joint jet continuity characterises the weak smooth topology

Statement

Let $P$ be a topological space, let $M, Q$ be smooth manifolds, and let $Φ : P \to C^{\infty} (M, Q)$ be a map with adjoint $φ : P \times M \to Q$ , $φ (p, x) : = Φ (p) (x)$ (The exponential law: for a locally compact metric $X$ and any spaces $Z$ and $Y$ , transposition is a bijection between $C (X \times Z, Y)$ and $C (Z, C (X, Y))$ with the compact-open topology, The compact-open topology on $C (X, Y)$ for a metric domain $X$ , with subbasis $S (K, V) = {f : f [K] \subseteq V}$ ). Then:

(i) if $Φ$ is continuous for the weak compact-open $C^{\infty}$ topology, then for every chart $(U, α)$ of $M$ , every compact $K \subseteq U$ , every chart $(V, β)$ of $Q$ and every $p_{0} \in P$ with $Φ (p_{0}) (K) \subseteq V$ there are a neighbourhood $W$ of $p_{0}$ with $Φ (W) (K) \subseteq V$ and, for every multi-index $γ$ , a continuous function $(p, x) \mapsto D^{γ} (β \circ Φ (p) \circ α^{- 1}) (α (x))$ on $W \times K$ ;

(ii) conversely, if $P$ is a smooth manifold and the adjoint $φ$ is smooth, then $Φ$ is continuous for the weak $C^{\infty}$ topology; more generally, if the adjoint $φ$ is continuous and the local jet functions of (i) are jointly continuous near every point at which they are defined, then $Φ$ is continuous.

Facts & Assumptions

Given: A map $Φ : P \to C^{\infty} (M, Q)$ with adjoint $φ$ , a chart $(U, α)$ of $M$ , a compact $K \subseteq U$ , a chart $(V, β)$ of $Q$ , and a point $p_{0}$ with $Φ (p_{0}) (K) \subseteq V$ .

[F1]

The weak compact-open $C^{\infty}$ topology on $C^{\infty} (M, Q)$ has as basic open sets the families determined by finitely many charts, compact pieces $K_{i}$ , integers $r_{i}$ and tolerances $ε_{i}$ , constraining the derivatives of order at most $r_{i}$ of $β_{i} \circ g \circ α_{i}^{- 1}$ on $α_{i} (K_{i})$ to lie within $ε_{i}$ of those of a reference map (The weak compact-open C-infinity topology on mapping spaces).

[L1]

Compact subsets admit finite ambient open subcovers (A subspace is compact exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it), and coordinate balls have compact closures inside prescribed neighbourhoods (Coordinate balls form a basis of a topological manifold). Finite intersections of open sets are open, and continuity is local (Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous).

[L2]

If $P$ is a smooth manifold and $φ : P \times M \to Q$ is smooth, then all derivatives $D^{γ} (β \circ φ \circ ({i d}_{P} \times α)^{- 1})$ exist and are continuous on their domains (Smooth manifolds and their smooth charts, Smooth families of maps and their evaluation maps).

Proof

technique · direct

1.1F1L1givenconstruct

Suppose $Φ$ is continuous. Choose a compact neighbourhood $K^{'}$ of $K$ inside $U \cap Φ (p_{0})^{- 1} (V)$ , using finitely many small closed coordinate balls from [L1]. The zeroth-order weak neighbourhood requiring the image of $K^{'}$ to remain in $V$ pulls back to a neighbourhood $W$ of $p_{0}$ . This single $W$ works for every derivative order.

1.2F1L1given

Conversely assume the adjoint and its local jet functions are jointly continuous. Fix $p_{0}$ and finite weak-neighbourhood data. Joint continuity of the adjoint and compactness of each $K_{i}$ first give a parameter neighbourhood on which its image stays in the target chart: take finitely many product neighbourhoods covering ${p_{0}} \times K_{i}$ and intersect their parameter factors. On that neighbourhood the maximum $G_{i} (p, x)$ of the finitely many derivative errors through order $r_{i}$ is continuous and vanishes when $p = p_{0}$ . For each $x \in K_{i}$ , choose a product neighbourhood on which $G_{i} < ε_{i}$ ; finitely many source factors cover $K_{i}$ , and the intersection of their parameter factors makes this inequality hold on all of $K_{i}$ . Intersect also over the finitely many $i$ . The resulting neighbourhood maps into the specified weak neighbourhood. This finite-cover argument works for every topological $P$ ; no first-countability or sequential argument is used.

2.1F1step 1.1algebra

Fix any multi-index $γ$ and any $(p_{1}, x_{1}) \in W \times α (K)$ . Continuity of $Φ$ at $p_{1}$ supplies, for every $ε > 0$ , a parameter neighbourhood on which the $γ$ -derivative differs uniformly on $α (K^{'})$ from that of $Φ (p_{1})$ by less than $ε / 2$ . The latter derivative is continuous in $x$ , since $Φ (p_{1})$ is smooth, and differs from its value at $x_{1}$ by less than $ε / 2$ near $x_{1}$ . The triangle inequality proves joint continuity at $(p_{1}, x_{1})$ . Hence (i) holds on $W$ , for all orders.

3.1L2step 2.1step 1.2∎

If $P$ is smooth and the adjoint is smooth, then its local $x$ -derivatives are jointly continuous by [L2], so step 1.2 applies. Empty compact pieces impose no conditions. This proves (ii) and completes both implications.

Depends on

Used by

Dependency tree · two levels

44 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

John Francis, The h-Principle, Lecture 3: Immersion theory (notes by O. Gwilliam), PDF pp. 1–4: the flexible-sheaf discussion and the compact-open C^infinity topology (standard reference, not scraped)
Morris W. Hirsch, Differential Topology, Ch. 2 §1, pp. 34–36 (the weak and strong C^r topologies and their chartwise description) (standard reference, not scraped)