The bundle of continuous alternating maps is a C^n vector bundle #
Category: 1-Mathlib (CSD-free; upstream target
Mathlib.Geometry.Manifold.VectorBundle, beside Hom.lean).
Mathlib has the bundle of continuous alternating
maps as a topological vector bundle (Topology/VectorBundle/ContinuousAlternatingMap.lean)
and it has Hom.lean doing the smooth case for the bundle of continuous linear maps. It has
nothing alternating anywhere under Geometry/Manifold/.
MATHLIB-ABSENT(ContMDiffVectorBundle.continuousAlternatingMap)
- ★
contMDiffOn_continuousAlternatingMapCoordChange— the coordinate change isC^n; - ★★
ContMDiffVectorBundle.continuousAlternatingMap— the instance: the alternating-map bundle of twoC^nvector bundles is aC^nvector bundle.
The proof mirrors Hom.lean exactly once the coordinate change is available, and the
coordinate change decomposes — by rfl — as postcomposition after pullback:
compContinuousAlternatingMapCLM (e₂.coordChangeL b)
∘L compContinuousLinearMapCLM (e₁'.coordChangeL b)
with both factors smooth by
Analysis/Normed/Module/Alternating/Pullback.lean.
⚠️ The elaboration trap, recorded because it cost a full attempt #
The first attempt at the coordinate-change lemma failed and was recorded — wrongly — as an
"instance-path mismatch" needing plumbing. It is not that. The two topologies on a
continuous-linear-map space are the same instance
(inferInstance = ContinuousLinearMap.topologicalSpace
by rfl, checked). What fails is elaboration order: writing
have h : ContDiff 𝕜 n (fun L : F₂ →L[𝕜] F₂ => (compContinuousAlternatingMapCLM L : … →L[𝕜] …))
re-synthesises the instances from the ascription and lands on the normed path, while the
term carries the topological-module path; the application check then runs at reducible
transparency and does not unfold them. Stating the same fact through the term —
ContDiff 𝕜 n ⇑(compContinuousAlternatingMapCLM …) — typechecks immediately. That is the whole
fix, and it is why this module states its two ContDiff hypotheses in that shape.
Honest scope #
⚠️ What remains of step (2a) is the last mile, and it is not this. With this instance,
differential forms on a manifold as smooth sections
(ContMDiffSection I _ n fun x ↦ TangentSpace I x [⋀^ι]→L[𝕜] Bundle.Trivial M G x) are one
definition away — but that definition needs the total-space topology instance to synthesise
for the specific (tangent bundle, trivial bundle) pair, which it does not do out of the box.
Not built here, and the row stays open until it is.
⚠️ Still no exterior derivative. That is step (2b), upstream's own TODO, and nothing here touches it. And as with steps (0) and (1): no physics waits on any of this.
Provenance and references. The Mathlib-gaps register; the backlog (XL, "Manifold exterior
calculus");
Mathlib/Geometry/Manifold/VectorBundle/Hom.lean (the template);
CsdLean4/Mathlib/Analysis/Normed/Module/Alternating/Pullback.lean (both factors).