Pullback of test forms and pushforward of currents #
Let Ω ⊆ E and Ω' ⊆ E' be open subsets of real normed spaces, and let Φ : E → E' be smooth
on Ω and proper from Ω to Ω': the set Ω ∩ Φ ⁻¹' K is compact for every compact
K ⊆ Ω'. The pullback of a test k-form ω on Ω' is the test k-form on Ω
(Φ^* ω) x = ω (Φ x) ∘ (DΦ x, …, DΦ x) for x ∈ Ω, extended by zero off Ω. Nothing is
assumed about Φ off Ω, so Φ may be a chart transition or a smooth map defined only on Ω.
The pullback TestFunction.pullbackCLM is continuous for the LF topology of test functions. So
the pushforward of a current T on Ω (a continuous linear functional on test forms) is the
current Φ_# T = T ∘ Φ^* on Ω'. Pullback commutes with the exterior derivative, hence
pushforward commutes with the boundary ∂T = T ∘ d. A bound ‖DΦ‖ ≤ L on Ω gives
M(Φ_# T) ≤ L ^ k M(T).
Multiplying by a test function χ on Ω removes the need for properness: the pullback with a
cutoff χ Φ^* ω is a test form supported in tsupport χ for every map Φ smooth on Ω. It is
used to push forward currents whose support is compact, see
TauCeti.Analysis.Distribution.CutoffPushforward.
Main declarations #
TestFunction.pullbackCLM: the pullback of test forms along a smooth map proper fromΩtoΩ', as a continuous linear map.TestFunction.pullbackCLM_apply_of_mem,TestFunction.pullbackCLM_apply_of_notMem: its values.TestFunction.tsupport_pullbackCLM_subset:supp Φ^* ω ⊆ Ω ∩ Φ ⁻¹' supp ω.TestFunction.pullbackCLM_id,TestFunction.pullbackCLM_comp: functoriality; the identity map pulls back by extension by zero.TestFunction.extDerivCLM_pullbackCLM:d (Φ^* ω) = Φ^* (d ω).ContinuousLinearMap.comp_pullbackCLM_comp_extDerivCLM:∂ (Φ_# T) = Φ_# (∂ T).Distribution.mass_comp_pullbackCLM_le:M(Φ_# T) ≤ L ^ k M(T)when‖DΦ‖ ≤ LonΩ.Distribution.HasLocallyFiniteMass.comp_pullbackCLM: pushforward preserves locally finite mass.TestFunction.cutoffPullbackCLM: the pullback with a cutoffω ↦ χ Φ^* ω, as a continuous linear map, with its valuesTestFunction.cutoffPullbackCLM_apply.TestFunction.extDerivCLM_cutoffPullbackCLM_apply:d (χ Φ^* ω) = χ Φ^* (d ω)at every point near whichχ = 1.TestFunction.cutoffPullbackCLM_cutoffPullbackCLM: composition of pullbacks with cutoffs.
Implementation notes #
Continuity is checked on each space of tests supported in a fixed compact K ⊆ Ω', whose
pullbacks are supported in the compact set Ω ∩ Φ ⁻¹' K. There the derivatives of Φ^* ω are
bounded by those of ω, through the Leibniz bound norm_iteratedFDerivWithin_clm_apply and the
Faà di Bruno bound norm_iteratedFDerivWithin_comp_le. The pointwise naturality of the exterior
derivative is Mathlib's extDeriv_pullback.
References #
- H. Federer, Geometric Measure Theory, §4.1.7 (the pushforward of a current).
- L. Simon, Introduction to Geometric Measure Theory, Chapter 6, §2.
The pullback of test k-forms along a map Φ that is smooth on Ω and proper from Ω
to Ω' (the set Ω ∩ Φ ⁻¹' K is compact for every compact K ⊆ Ω'), as a continuous linear
map. On Ω it is (Φ^* ω) x = ω (Φ x) ∘ (DΦ x, …, DΦ x), see
TestFunction.pullbackCLM_apply_of_mem, and it vanishes off Ω. Precomposing a current on Ω
with it gives the pushforward current on Ω'.
Instances For
The pullback of a test form is the pointwise pullback, extended by zero off Ω.
On Ω, the pullback is (Φ^* ω) x = ω (Φ x) ∘ (DΦ x, …, DΦ x).
Off Ω, the pullback vanishes.
The support of a pullback lies over the support of the form.
The pointwise norm of a pullback of a k-form is at most ‖ω (Φ x)‖ ‖DΦ x‖ ^ k.
Pulling back along the identity of E from Ω' ⊆ Ω is extension by zero.
Functoriality of pullback: (Ψ ∘ Φ)^* = Φ^* ∘ Ψ^* when Φ maps Ω into Ω'.
Naturality of the exterior derivative: d (Φ^* ω) = Φ^* (d ω).
Naturality of the exterior derivative, as an identity of continuous linear maps.
Pullback with a cutoff #
A test function χ on Ω localizes the pullback: χ Φ^* ω is supported in the compact set
tsupport χ whatever Φ does, so no properness of Φ is needed. Precomposing a current on Ω
with this map gives its pushforward along Φ when χ = 1 on a neighborhood of the current's
support.
The pullback with a cutoff ω ↦ χ Φ^* ω of test k-forms on Ω' along a map Φ smooth
on Ω, where χ is a test function on Ω: its value at x is
χ x • ω (Φ x) ∘ (DΦ x, …, DΦ x) (TestFunction.cutoffPullbackCLM_apply). It is supported in
tsupport χ, so Φ need not be proper, and nothing is assumed about where Φ maps Ω. For a
current T on Ω whose support lies in the interior of {χ = 1}, T ∘ (χ Φ^*) is the
pushforward of T along Φ; it does not depend on such χ and agrees with T ∘ Φ^* when Φ is
proper (see TauCeti.Analysis.Distribution.CutoffPushforward).
Instances For
The pullback with a cutoff is x ↦ χ x • ω (Φ x) ∘ (DΦ x, …, DΦ x).
The support of a pullback with a cutoff lies in the support of the cutoff, over the support of the form.
The pointwise norm of a pullback of a k-form with a cutoff is at most
|χ x| ‖ω (Φ x)‖ ‖DΦ x‖ ^ k.
Naturality of the exterior derivative where the cutoff is one:
d (χ Φ^* ω) = χ Φ^* (d ω) near every point at which χ is eventually equal to one.
Composition of pullbacks with cutoffs: χ Φ^* (χ' Ψ^* ω) = (χ' ∘ Φ) χ (Ψ ∘ Φ)^* ω. Where
Φ x ∉ Ω' both sides vanish, since χ' is supported in Ω'.
Pushforward commutes with the boundary: for a current T on Ω, the pushforward
Φ_# T = T ∘ Φ^* satisfies ∂ (Φ_# T) = Φ_# (∂ T), where ∂ T = T ∘ d.
The mass of a pushforward: if ‖DΦ‖ ≤ L on Ω, then the pushforward T ∘ Φ^* of a
k-current T has mass at most L ^ k times the mass of T.
Pushforward preserves locally finite mass. If a map T on test k-forms on Ω has
locally finite mass, so does its pushforward T ∘ Φ^* on Ω'. On a compact K ⊆ Ω' its
order-zero bound is that of T on the compact set Ω ∩ Φ ⁻¹' K, times a bound for ‖DΦ‖ ^ k
there.