C^n families of continuous alternating maps

A family of continuous alternating maps f : M → E [⋀^ι]→L[𝕜] F on a finite-dimensional space E, parametrized by a manifold, is C^n exactly when each evaluation y ↦ f y v is C^n. This is the alternating counterpart of Mathlib's contDiffWithinAt_clm_apply for continuous linear maps. It reduces the regularity of a differential form, read in a trivialization of the alternating bundle, to the regularity of its values on fixed tuples of model vectors.

The converse direction expands an alternating map as ∑ₜ c t (·) • f y (b ∘ t) over all tuples t of basis indices, with scalar coefficient forms c t that do not depend on f. This is a continuous linear function of the evaluations, so the coefficient space F may be infinite-dimensional.

theorem TauCeti.contMDiffWithinAt_continuousAlternatingMap_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {EM : Type u_2} {HM : Type u_3} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] [TopologicalSpace HM] {I : ModelWithCorners 𝕜 EM HM} {M : Type u_4} [TopologicalSpace M] [ChartedSpace HM M] {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_7} [Fintype ι] {n : WithTop ℕ∞} {f : M → E [⋀^ι]→L[𝕜] F} {s : Set M} {x : M} : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (E [⋀^ι]→L[𝕜] F)) n f s x ↔ ∀ (v : ι → E), ContMDiffWithinAt I (modelWithCornersSelf 𝕜 F) n (fun (y : M) => (f y) v) s x

A family of continuous alternating maps on a finite-dimensional space is C^n within a set at a point if and only if all its evaluations are.

theorem TauCeti.contMDiffAt_continuousAlternatingMap_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {EM : Type u_2} {HM : Type u_3} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] [TopologicalSpace HM] {I : ModelWithCorners 𝕜 EM HM} {M : Type u_4} [TopologicalSpace M] [ChartedSpace HM M] {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_7} [Fintype ι] {n : WithTop ℕ∞} {f : M → E [⋀^ι]→L[𝕜] F} {x : M} : ContMDiffAt I (modelWithCornersSelf 𝕜 (E [⋀^ι]→L[𝕜] F)) n f x ↔ ∀ (v : ι → E), ContMDiffAt I (modelWithCornersSelf 𝕜 F) n (fun (y : M) => (f y) v) x

A family of continuous alternating maps on a finite-dimensional space is C^n at a point if and only if all its evaluations are.