Smooth pullback of continuous alternating maps

Mathlib's multilinear pullback is polynomial in the continuous linear map used on the domain. For finite orders and ∞, smoothness follows from Mathlib's continuous multilinear pullback and reflection through the closed isometric inclusion. At the analytic order ω, normalized alternatization recovers the alternating output when the arity factorial is nonzero. The result is operator-valued, so it controls smooth coordinate changes of alternating-map bundles.

The regularity parameter includes the analytic order ω, as well as finite orders and ∞. The polynomial construction proves the analytic case under the factorial hypothesis.

The underlying polynomial is Mathlib's ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear.

theorem ContinuousAlternatingMap.contDiff_compContinuousLinearMapCLM {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {ι : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (n : WithTop ℕ∞) (hn : n = ⊤ → ↑(Fintype.card ι).factorial ≠ 0 := by intro h first | exact NeZero.ne _ | cases h) : ContDiff 𝕜 n compContinuousLinearMapCLM

Pullback on continuous alternating maps is smooth, as an operator-valued function of the continuous linear map on the domain. Only the analytic order ω carries a factorial hypothesis; finite orders and ∞ have no characteristic restriction. No completeness or finite dimensionality is needed.