The pullback of a continuous alternating map is jointly analytic

Category: 1-Mathlib (CSD-free; upstream targets Mathlib.Topology.Algebra.Module.Alternating for the alternatization and Mathlib.Analysis.Analytic.CPolynomial for the pullback, beside its multilinear twin).

The lemma differential forms on a manifold need first. Making them into smooth sections needs a ContMDiffVectorBundle instance for the alternating-map bundle, whose crux is smoothness of the coordinate change — and that reduces to smoothness of the pullback (g, ω) ↦ ω ∘ g in both arguments jointly.

⚠️ At the pin upstream has that for the multilinear pullback (ContinuousMultilinearMap.analyticAt_uncurry_compContinuousLinearMap, Analysis/Analytic/CPolynomial.lean) and, for the alternating one, only continuity and the first derivative (Analysis/Calculus/FDeriv/ContinuousAlternatingMap.lean). The obvious reduction fails: the alternating pullback is the DIAGONAL restriction of the multilinear one — degree card ι in g, not linear — so it is not itself a continuous multilinear map, and the existing continuity proof reflects along an inducing embedding, an argument that does not carry to ContDiff. MATHLIB-ABSENT(ContinuousAlternatingMap.analyticAt_uncurry_compContinuousLinearMap)

What unlocks it is a left inverse. Alternatization sends a continuous multilinear map to a continuous alternating one, and on an already-alternating map it multiplies by (card ι)! — so in characteristic zero it is a continuous linear retraction of the inclusion. Analyticity then reflects for free: the alternating pullback is that retraction applied to the multilinear pullback of the inclusion, along the diagonal.

Contents

• ContinuousMultilinearMap.continuous_alternatization and ★ ContinuousMultilinearMap.alternatizationCLM — alternatization as a continuous linear map. Upstream has it only as an AddMonoidHom (ContinuousMultilinearMap.alternatization), which is the reason the retraction argument was not available; MATHLIB-ABSENT(ContinuousMultilinearMap.alternatizationCLM)
• alternatizationCLM_of_alternating — on an alternating map it is (card ι)!;
• compContinuousLinearMap_eq_smul_alternatization — the pullback written through the retraction, which is the whole idea in one equation;
• ★★ ContinuousAlternatingMap.analyticAt_uncurry_compContinuousLinearMap — the pullback is jointly analytic, and
• ★ contDiffAt_uncurry_compContinuousLinearMap / contDiff_uncurry_compContinuousLinearMap — the ContDiff corollaries, which is the form the bundle instance consumes;
• ContinuousAlternatingMap.compContinuousLinearMap_apply_pair — the degree-2 evaluation (ω ∘ L) ⦃a, b⦄ = ω ⦃L a, L b⦄, which is how a pulled-back 2-form is read off a pair of tangent vectors.

Honest scope

⚠️ This unblocks step (2a); it does not perform it. What still has to be built on top: the ContMDiffOn lemma for the alternating bundle's coordinate change, the ContMDiffVectorBundle instance (the analogue of Geometry/Manifold/VectorBundle/Hom.lean), and only then differential forms on a manifold as smooth sections.

⚠️⚠️ CORRECTION (same day): the note below was DIAGNOSED WRONG, and both remaining layers have since landed in Mathlib/Geometry/Manifold/VectorBundle/AlternatingMap.lean. It is not an instance-path mismatch: the two topologies on a continuous-linear-map space are the same instance (inferInstance = ContinuousLinearMap.topologicalSpace by rfl, checked). The real cause is elaboration order — a type ascription re-synthesises the instances down the normed path while the term carries the topological-module path, and the application check runs at reducible transparency. Stating the ContDiff fact through the term (ContDiff 𝕜 n ⇑f) rather than through an ascription fixes it outright. The original note is kept below because the lesson is worth more than the mistake: a failure at the instance layer is not automatically an instance-diamond problem, and the cheapest test — are these the same instance? — was one rfl away and was not run.

⚠️ The original, incorrect note. The coordinate change of the alternating bundle decomposes as compContinuousAlternatingMapCLM 𝕜 _ _ _ ι (e₂.coordChangeL b) ∘L compContinuousLinearMapCLM (e₁'.coordChangeL b) — and that decomposition is rfl, checked. With contDiff_compContinuousLinearMapCLM and Mathlib's ContinuousLinearMap.compContinuousAlternatingMapCLM (until 2026-09-16 this file re-built it as compContinuousAlternatingMapL) the ContMDiffOn proof is then the same three lines as Hom.lean's. What blocks it is an instance-path mismatch: feeding those bundled maps to ContinuousLinearMap.contDiff elaborates the operator and alternating spaces on the topological-module instances (ContinuousLinearMap.topologicalSpace, ContinuousAlternatingMap.topologicalSpace) where the normed path is wanted. The two are mathematically the same topology; reconciling them is instance plumbing, not a theorem, and it is deliberately not attempted here rather than papered over.

⚠️ Characteristic zero is essential, not incidental. The retraction divides by (card ι)!; over a field of positive characteristic the argument fails at exactly that step, and nothing here says whether the conclusion survives.

⚠️ contDiffAt_… needs [CompleteSpace G], inherited from AnalyticAt.contDiffAt. The analyticity statement itself does not.

Provenance and references. The Mathlib-gaps register (Kahler / symplectic manifold API, step (2a)); the backlog (XL, "Manifold exterior calculus"); Mathlib/Analysis/Analytic/CPolynomial.lean (the multilinear twin this reflects from); Mathlib/Topology/Algebra/Module/Alternating/Basic.lean (alternatization, the AddMonoidHom this upgrades).

theorem ContinuousMultilinearMap.continuous_alternatization {𝕜 : Type u_1} {ι : Type u_2} {M : Type u_3} {N : Type u_4} [NontriviallyNormedField 𝕜] [Fintype ι] [DecidableEq ι] [NormedAddCommGroup M] [NormedSpace 𝕜 M] [NormedAddCommGroup N] [NormedSpace 𝕜 N] : Continuous ⇑alternatization

Alternatization is continuous: it is a finite signed sum of index permutations, and the topology on the alternating maps is induced from the multilinear ones.

noncomputable def ContinuousMultilinearMap.alternatizationCLM {𝕜 : Type u_1} {ι : Type u_2} {M : Type u_3} {N : Type u_4} [NontriviallyNormedField 𝕜] [Fintype ι] [DecidableEq ι] [NormedAddCommGroup M] [NormedSpace 𝕜 M] [NormedAddCommGroup N] [NormedSpace 𝕜 N] : ContinuousMultilinearMap 𝕜 (fun (x : ι) => M) N →L[𝕜] M [⋀^ι]→L[𝕜] N

★ Alternatization as a continuous linear map. Upstream has this only as an AddMonoidHom; the scalar action and the continuity are what make it usable as a retraction.

Equations

• ContinuousMultilinearMap.alternatizationCLM = { toFun := ⇑ContinuousMultilinearMap.alternatization, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

theorem ContinuousMultilinearMap.alternatizationCLM_of_alternating {𝕜 : Type u_1} {ι : Type u_2} {M : Type u_3} {N : Type u_4} [NontriviallyNormedField 𝕜] [Fintype ι] [DecidableEq ι] [NormedAddCommGroup M] [NormedSpace 𝕜 M] [NormedAddCommGroup N] [NormedSpace 𝕜 N] (ω : M [⋀^ι]→L[𝕜] N) : alternatizationCLM ω.toContinuousMultilinearMap = (Fintype.card ι).factorial • ω

Alternatizing something already alternating multiplies it by (card ι)! — so in characteristic zero alternatizationCLM is a continuous linear retraction of the inclusion of alternating maps into multilinear ones.

theorem ContinuousAlternatingMap.compContinuousLinearMap_eq_smul_alternatization {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [NontriviallyNormedField 𝕜] [Fintype ι] [DecidableEq ι] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [CharZero 𝕜] (g : E →L[𝕜] F) (ω : F [⋀^ι]→L[𝕜] G) : ω.compContinuousLinearMap g = (↑(Fintype.card ι).factorial)⁻¹ • ContinuousMultilinearMap.alternatizationCLM (ω.compContinuousLinearMap fun (x : ι) => g)

The idea, in one equation. The pullback of an alternating map is the retraction applied to the pullback of its inclusion — so anything true of the multilinear pullback and stable under continuous linear maps transfers.

noncomputable def ContinuousAlternatingMap.pullbackPairCLM {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] : (E →L[𝕜] F) × F [⋀^ι]→L[𝕜] G →L[𝕜] (ι → E →L[𝕜] F) × ContinuousMultilinearMap 𝕜 (fun (x : ι) => F) G

The bundled linear reindexing used in the analyticity proof.

Equations

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

theorem ContinuousAlternatingMap.analyticAt_uncurry_compContinuousLinearMap {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [NontriviallyNormedField 𝕜] [Fintype ι] [DecidableEq ι] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [CharZero 𝕜] (q : (E →L[𝕜] F) × F [⋀^ι]→L[𝕜] G) : AnalyticAt 𝕜 (fun (p : (E →L[𝕜] F) × F [⋀^ι]→L[𝕜] G) => p.2.compContinuousLinearMap p.1) q

★ The missing lemma. The pullback of a continuous alternating map along a continuous linear map is analytic in both arguments jointly.

theorem ContinuousAlternatingMap.contDiffAt_uncurry_compContinuousLinearMap {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [NontriviallyNormedField 𝕜] [Fintype ι] [DecidableEq ι] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [CharZero 𝕜] [CompleteSpace G] {n : WithTop ℕ∞} (q : (E →L[𝕜] F) × F [⋀^ι]→L[𝕜] G) : ContDiffAt 𝕜 n (fun (p : (E →L[𝕜] F) × F [⋀^ι]→L[𝕜] G) => p.2.compContinuousLinearMap p.1) q

★ The ContDiffAt corollary — the form a smooth-bundle instance consumes.

theorem ContinuousAlternatingMap.contDiff_uncurry_compContinuousLinearMap {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [NontriviallyNormedField 𝕜] [Fintype ι] [DecidableEq ι] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [CharZero 𝕜] [CompleteSpace G] {n : WithTop ℕ∞} : ContDiff 𝕜 n fun (p : (E →L[𝕜] F) × F [⋀^ι]→L[𝕜] G) => p.2.compContinuousLinearMap p.1

★ The ContDiff corollary.

The operator-valued form, and postcomposition

What a smooth-bundle instance actually consumes is not the application (g, ω) ↦ ω ∘ g but the operator-valued map g ↦ (ω ↦ ω ∘ g), together with its postcomposition partner. Both are here. ⚠️ See the honest-scope note at the top of the file for where the next layer stops.

theorem ContinuousAlternatingMap.compContinuousLinearMapCLM_eq {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [NontriviallyNormedField 𝕜] [Fintype ι] [DecidableEq ι] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [CharZero 𝕜] (g : E →L[𝕜] F) : compContinuousLinearMapCLM g = ((↑(Fintype.card ι).factorial)⁻¹ • ContinuousMultilinearMap.alternatizationCLM) ∘SL ((ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear 𝕜 (fun (x : ι) => E) (fun (x : ι) => F) G) fun (x : ι) => g) ∘SL toContinuousMultilinearMapCLM 𝕜

The retraction identity in operator form.

theorem ContinuousAlternatingMap.contDiff_compContinuousLinearMapCLM {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [NontriviallyNormedField 𝕜] [Fintype ι] [DecidableEq ι] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [CharZero 𝕜] {n : WithTop ℕ∞} : ContDiff 𝕜 n fun (g : E →L[𝕜] F) => compContinuousLinearMapCLM g

★ The pullback operator is smooth in the linear map. This is the form the coordinate change of an alternating-map bundle is built from.

theorem ContinuousAlternatingMap.compContinuousLinearMap_apply_pair {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (alt : F [⋀^Fin 2]→L[𝕜] G) (L : E →L[𝕜] F) (a b : E) : (alt.compContinuousLinearMap L) ![a, b] = alt ![L a, L b]

The pullback of a 2-form, read on a pair of vectors: (ω ∘ L) ⦃a, b⦄ = ω ⦃L a, L b⦄. The Matrix.cons notation does not reduce under the composition on its own, so this is the lemma every degree-2 pullback computation starts with.