The bundle of alternating maps between C^n vector bundles over the same base space is C^n

Here we show that the bundle of continuous alternating linear maps is a C^n vector bundle, when the base field has characteristic zero.

We also show that applying a smooth family of alternating maps to smooth families of vectors gives a smooth result, in several versions.

Note that, in positive characteristic, the result is true in finite dimension, but not in general for n = ω. See https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/bundles.20of.20alternating.20maps/near/630597041 For now, we only implement the characteristic zero case as it is the most important.

theorem contMDiffOn_continuousAlternatingMapCoordChange {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {ι : Type u_6} {n : WithTop ℕ∞} [Fintype ι] {E₁ : B → Type u_7} {E₂ : B → Type u_8} [NontriviallyNormedField 𝕜] [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B) → TopologicalSpace (E₁ x)] [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → TopologicalSpace (E₂ x)] {EB : Type u_9} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_10} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] {e₁ e₁' : Bundle.Trivialization F₁ Bundle.TotalSpace.proj} {e₂ e₂' : Bundle.Trivialization F₂ Bundle.TotalSpace.proj} [CharZero 𝕜] [ContMDiffVectorBundle n F₁ E₁ IB] [ContMDiffVectorBundle n F₂ E₂ IB] [MemTrivializationAtlas e₁] [MemTrivializationAtlas e₁'] [MemTrivializationAtlas e₂] [MemTrivializationAtlas e₂'] : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F₁ [⋀^ι]→L[𝕜] F₂ →L[𝕜] F₁ [⋀^ι]→L[𝕜] F₂)) n (Bundle.Pretrivialization.continuousAlternatingMapCoordChange 𝕜 ι e₁ e₁' e₂ e₂') (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))

@[simp]

theorem chartAt_continuousAlternatingMap {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {ι : Type u_6} [Fintype ι] {E₁ : B → Type u_7} {E₂ : B → Type u_8} [NontriviallyNormedField 𝕜] [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B) → TopologicalSpace (E₁ x)] [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → TopologicalSpace (E₂ x)] {HB : Type u_10} [TopologicalSpace HB] [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] (y₀ y : Bundle.TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (b : B) => E₁ b [⋀^ι]→L[𝕜] E₂ b) : ↑(chartAt (ModelProd HB (F₁ [⋀^ι]→L[𝕜] F₂)) y₀) y = (↑(chartAt HB y₀.proj) y.proj, ContinuousAlternatingMap.inCoordinates F₁ F₂ y₀.proj y.proj y₀.proj y.proj y.snd)

theorem contMDiffWithinAt_continuousAlternatingMap_bundle {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {M : Type u_5} {ι : Type u_6} {n : WithTop ℕ∞} [Fintype ι] {E₁ : B → Type u_7} {E₂ : B → Type u_8} [NontriviallyNormedField 𝕜] [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B) → TopologicalSpace (E₁ x)] [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → TopologicalSpace (E₂ x)] {EB : Type u_9} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_10} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_11} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_12} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] (f : M → Bundle.TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (b : B) => E₁ b [⋀^ι]→L[𝕜] E₂ b) {s : Set M} {x₀ : M} : ContMDiffWithinAt IM (IB.prod (modelWithCornersSelf 𝕜 (F₁ [⋀^ι]→L[𝕜] F₂))) n f s x₀ ↔ ContMDiffWithinAt IM IB n (fun (x : M) => (f x).proj) s x₀ ∧ ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 (F₁ [⋀^ι]→L[𝕜] F₂)) n (fun (x : M) => ContinuousAlternatingMap.inCoordinates F₁ F₂ (f x₀).proj (f x).proj (f x₀).proj (f x).proj (f x).snd) s x₀

theorem contMDiffAt_continuousAlternatingMap_bundle {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {M : Type u_5} {ι : Type u_6} {n : WithTop ℕ∞} [Fintype ι] {E₁ : B → Type u_7} {E₂ : B → Type u_8} [NontriviallyNormedField 𝕜] [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B) → TopologicalSpace (E₁ x)] [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → TopologicalSpace (E₂ x)] {EB : Type u_9} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_10} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_11} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_12} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] (f : M → Bundle.TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (b : B) => E₁ b [⋀^ι]→L[𝕜] E₂ b) {x₀ : M} : ContMDiffAt IM (IB.prod (modelWithCornersSelf 𝕜 (F₁ [⋀^ι]→L[𝕜] F₂))) n f x₀ ↔ ContMDiffAt IM IB n (fun (x : M) => (f x).proj) x₀ ∧ ContMDiffAt IM (modelWithCornersSelf 𝕜 (F₁ [⋀^ι]→L[𝕜] F₂)) n (fun (x : M) => ContinuousAlternatingMap.inCoordinates F₁ F₂ (f x₀).proj (f x).proj (f x₀).proj (f x).proj (f x).snd) x₀

theorem mdifferentiableOn_continuousAlternatingMapCoordChange {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {ι : Type u_6} [Fintype ι] {E₁ : B → Type u_7} {E₂ : B → Type u_8} [NontriviallyNormedField 𝕜] [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B) → TopologicalSpace (E₁ x)] [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → TopologicalSpace (E₂ x)] {EB : Type u_9} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_10} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] {e₁ e₁' : Bundle.Trivialization F₁ Bundle.TotalSpace.proj} {e₂ e₂' : Bundle.Trivialization F₂ Bundle.TotalSpace.proj} [CharZero 𝕜] [ContMDiffVectorBundle 1 F₁ E₁ IB] [ContMDiffVectorBundle 1 F₂ E₂ IB] [MemTrivializationAtlas e₁] [MemTrivializationAtlas e₁'] [MemTrivializationAtlas e₂] [MemTrivializationAtlas e₂'] : MDiff[e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)] (Bundle.Pretrivialization.continuousAlternatingMapCoordChange 𝕜 ι e₁ e₁' e₂ e₂')

theorem mdifferentiableWithinAt_continuousAlternatingMap_bundle {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {M : Type u_5} {ι : Type u_6} [Fintype ι] {E₁ : B → Type u_7} {E₂ : B → Type u_8} [NontriviallyNormedField 𝕜] [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B) → TopologicalSpace (E₁ x)] [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → TopologicalSpace (E₂ x)] {EB : Type u_9} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_10} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_11} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_12} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] (f : M → Bundle.TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (b : B) => E₁ b [⋀^ι]→L[𝕜] E₂ b) {s : Set M} {x₀ : M} : MDiffAt[s] f x₀ ↔ (MDiffAt[s] fun (x : M) => (f x).proj) x₀ ∧ (MDiffAt[s] fun (x : M) => ContinuousAlternatingMap.inCoordinates F₁ F₂ (f x₀).proj (f x).proj (f x₀).proj (f x).proj (f x).snd) x₀

theorem mdifferentiableAt_continuousAlternatingMap_bundle {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {M : Type u_5} {ι : Type u_6} [Fintype ι] {E₁ : B → Type u_7} {E₂ : B → Type u_8} [NontriviallyNormedField 𝕜] [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B) → TopologicalSpace (E₁ x)] [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → TopologicalSpace (E₂ x)] {EB : Type u_9} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_10} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_11} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_12} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] (f : M → Bundle.TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (b : B) => E₁ b [⋀^ι]→L[𝕜] E₂ b) {x₀ : M} : MDiffAt f x₀ ↔ (MDiffAt fun (x : M) => (f x).proj) x₀ ∧ (MDiffAt fun (x : M) => ContinuousAlternatingMap.inCoordinates F₁ F₂ (f x₀).proj (f x).proj (f x₀).proj (f x).proj (f x).snd) x₀

instance Bundle.ContinuousAlternatingMap.vectorPrebundle.isContMDiff {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {ι : Type u_6} {n : WithTop ℕ∞} [Fintype ι] {E₁ : B → Type u_7} {E₂ : B → Type u_8} [NontriviallyNormedField 𝕜] [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (TotalSpace F₁ E₁)] [(x : B) → TopologicalSpace (E₁ x)] [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (TotalSpace F₂ E₂)] [(x : B) → TopologicalSpace (E₂ x)] {EB : Type u_9} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_10} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] [CharZero 𝕜] [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] [ContMDiffVectorBundle n F₁ E₁ IB] [ContMDiffVectorBundle n F₂ E₂ IB] : VectorPrebundle.IsContMDiff IB (vectorPrebundle 𝕜 ι F₁ E₁ F₂ E₂) n

instance ContMDiffVectorBundle.continuousAlternatingMap {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {ι : Type u_6} {n : WithTop ℕ∞} [Fintype ι] {E₁ : B → Type u_7} {E₂ : B → Type u_8} [NontriviallyNormedField 𝕜] [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B) → TopologicalSpace (E₁ x)] [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → TopologicalSpace (E₂ x)] {EB : Type u_9} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_10} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] [CharZero 𝕜] [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] [ContMDiffVectorBundle n F₁ E₁ IB] [ContMDiffVectorBundle n F₂ E₂ IB] : ContMDiffVectorBundle n (F₁ [⋀^ι]→L[𝕜] F₂) (fun (b : B) => E₁ b [⋀^ι]→L[𝕜] E₂ b) IB

theorem ContMDiffWithinAt.continuousAlternatingMap_apply_of_inCoordinates {𝕜 : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {B₁ : Type u_4} {B₂ : Type u_5} {M : Type u_6} {ι : Type u_7} [Fintype ι] {E₁ : B₁ → Type u_8} {E₂ : B₂ → Type u_9} [NontriviallyNormedField 𝕜] [(x : B₁) → AddCommGroup (E₁ x)] [(x : B₁) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B₁) → TopologicalSpace (E₁ x)] [(x : B₂) → AddCommGroup (E₂ x)] [(x : B₂) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B₂) → TopologicalSpace (E₂ x)] {EB₁ : Type u_10} [NormedAddCommGroup EB₁] [NormedSpace 𝕜 EB₁] {HB₁ : Type u_11} [TopologicalSpace HB₁] {IB₁ : ModelWithCorners 𝕜 EB₁ HB₁} [TopologicalSpace B₁] [ChartedSpace HB₁ B₁] {EB₂ : Type u_12} [NormedAddCommGroup EB₂] [NormedSpace 𝕜 EB₂] {HB₂ : Type u_13} [TopologicalSpace HB₂] {IB₂ : ModelWithCorners 𝕜 EB₂ HB₂} [TopologicalSpace B₂] [ChartedSpace HB₂ B₂] {EM : Type u_14} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_15} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] {n : WithTop ℕ∞} [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] {b₁ : M → B₁} {b₂ : M → B₂} {m₀ : M} {ϕ : (m : M) → E₁ (b₁ m) [⋀^ι]→L[𝕜] E₂ (b₂ m)} {v : ι → (m : M) → E₁ (b₁ m)} {s : Set M} (hϕ : ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 (F₁ [⋀^ι]→L[𝕜] F₂)) n (fun (m : M) => ContinuousAlternatingMap.inCoordinates F₁ F₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) s m₀) (hv : ∀ (i : ι), ContMDiffWithinAt IM (IB₁.prod (modelWithCornersSelf 𝕜 F₁)) n (fun (m : M) => ⟨b₁ m, v i m⟩) s m₀) (hb₂ : ContMDiffWithinAt IM IB₂ n b₂ s m₀) : ContMDiffWithinAt IM (IB₂.prod (modelWithCornersSelf 𝕜 F₂)) n (fun (m : M) => ⟨b₂ m, (ϕ m) fun (i : ι) => v i m⟩) s m₀

Consider C^n maps v₁, ..., vᵢ : M → E₁ to a vector bundle, over a base map b₁ : M → B₁, and another base map b₂ : M → B₂. Given alternating maps ϕ m : E₁ (b₁ m) [⋀^ι]→L[𝕜] E₂ (b₂ m) depending smoothly on m, one can apply ϕ m to (v₁ m, ..., vᵢ m), and the resulting map is C^n.

Note that the smoothness of ϕ cannot always be stated as smoothness of a map into a manifold, as the pullback bundles b₁ *ᵖ E₁ and b₂ *ᵖ E₂ are smooth manifolds only when b₁ and b₂ are globally smooth, but we want to apply this lemma with only local information. Therefore, we formulate it using smoothness of ϕ read in coordinates.

Version for ContMDiffWithinAt. We also give a version for ContMDiffAt, but no version for ContMDiffOn or ContMDiff as our assumption, written in coordinates, only makes sense around a point.

For a version with B₁ = B₂ and b₁ = b₂, in which smoothness can be expressed without inCoordinates, see ContMDiffWithinAt.continuousAlternatingMap_bundle_apply.

theorem ContMDiffAt.continuousAlternatingMap_apply_of_inCoordinates {𝕜 : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {B₁ : Type u_4} {B₂ : Type u_5} {M : Type u_6} {ι : Type u_7} [Fintype ι] {E₁ : B₁ → Type u_8} {E₂ : B₂ → Type u_9} [NontriviallyNormedField 𝕜] [(x : B₁) → AddCommGroup (E₁ x)] [(x : B₁) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B₁) → TopologicalSpace (E₁ x)] [(x : B₂) → AddCommGroup (E₂ x)] [(x : B₂) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B₂) → TopologicalSpace (E₂ x)] {EB₁ : Type u_10} [NormedAddCommGroup EB₁] [NormedSpace 𝕜 EB₁] {HB₁ : Type u_11} [TopologicalSpace HB₁] {IB₁ : ModelWithCorners 𝕜 EB₁ HB₁} [TopologicalSpace B₁] [ChartedSpace HB₁ B₁] {EB₂ : Type u_12} [NormedAddCommGroup EB₂] [NormedSpace 𝕜 EB₂] {HB₂ : Type u_13} [TopologicalSpace HB₂] {IB₂ : ModelWithCorners 𝕜 EB₂ HB₂} [TopologicalSpace B₂] [ChartedSpace HB₂ B₂] {EM : Type u_14} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_15} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] {n : WithTop ℕ∞} [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] {b₁ : M → B₁} {b₂ : M → B₂} {m₀ : M} {ϕ : (m : M) → E₁ (b₁ m) [⋀^ι]→L[𝕜] E₂ (b₂ m)} {v : ι → (m : M) → E₁ (b₁ m)} (hϕ : ContMDiffAt IM (modelWithCornersSelf 𝕜 (F₁ [⋀^ι]→L[𝕜] F₂)) n (fun (m : M) => ContinuousAlternatingMap.inCoordinates F₁ F₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀) (hv : ∀ (i : ι), ContMDiffAt IM (IB₁.prod (modelWithCornersSelf 𝕜 F₁)) n (fun (m : M) => ⟨b₁ m, v i m⟩) m₀) (hb₂ : ContMDiffAt IM IB₂ n b₂ m₀) : ContMDiffAt IM (IB₂.prod (modelWithCornersSelf 𝕜 F₂)) n (fun (m : M) => ⟨b₂ m, (ϕ m) fun (i : ι) => v i m⟩) m₀

Consider a C^n map v : M → E₁ to a vector bundle, over a base map b₁ : M → B₁, and another base map b₂ : M → B₂. Given linear maps ϕ m : E₁ (b₁ m) → E₂ (b₂ m) depending smoothly on m, one can apply ϕ m to v m, and the resulting map is C^n.

Note that the smoothness of ϕ cannot always be stated as smoothness of a map into a manifold, as the pullback bundles b₁ *ᵖ E₁ and b₂ *ᵖ E₂ are smooth manifolds only when b₁ and b₂ are globally smooth, but we want to apply this lemma with only local information. Therefore, we formulate it using smoothness of ϕ read in coordinates.

Version for ContMDiffAt. We also give a version for ContMDiffWithinAt, but no version for ContMDiffOn or ContMDiff as our assumption, written in coordinates, only makes sense around a point.

For a version with B₁ = B₂ and b₁ = b₂, in which smoothness can be expressed without inCoordinates, see ContMDiffAt.continuousAlternatingMap_bundle_apply.

theorem MDifferentiableWithinAt.continuousAlternatingMap_apply_of_inCoordinates {𝕜 : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {B₁ : Type u_4} {B₂ : Type u_5} {M : Type u_6} {ι : Type u_7} [Fintype ι] {E₁ : B₁ → Type u_8} {E₂ : B₂ → Type u_9} [NontriviallyNormedField 𝕜] [(x : B₁) → AddCommGroup (E₁ x)] [(x : B₁) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B₁) → TopologicalSpace (E₁ x)] [(x : B₂) → AddCommGroup (E₂ x)] [(x : B₂) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B₂) → TopologicalSpace (E₂ x)] {EB₁ : Type u_10} [NormedAddCommGroup EB₁] [NormedSpace 𝕜 EB₁] {HB₁ : Type u_11} [TopologicalSpace HB₁] {IB₁ : ModelWithCorners 𝕜 EB₁ HB₁} [TopologicalSpace B₁] [ChartedSpace HB₁ B₁] {EB₂ : Type u_12} [NormedAddCommGroup EB₂] [NormedSpace 𝕜 EB₂] {HB₂ : Type u_13} [TopologicalSpace HB₂] {IB₂ : ModelWithCorners 𝕜 EB₂ HB₂} [TopologicalSpace B₂] [ChartedSpace HB₂ B₂] {EM : Type u_14} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_15} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] {b₁ : M → B₁} {b₂ : M → B₂} {m₀ : M} {ϕ : (m : M) → E₁ (b₁ m) [⋀^ι]→L[𝕜] E₂ (b₂ m)} {v : ι → (m : M) → E₁ (b₁ m)} {s : Set M} (hϕ : (MDiffAt[s] fun (m : M) => ContinuousAlternatingMap.inCoordinates F₁ F₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀) (hv : ∀ (i : ι), (MDiffAt[s] fun (m : M) => ⟨b₁ m, v i m⟩) m₀) (hb₂ : MDiffAt[s] b₂ m₀) : (MDiffAt[s] fun (m : M) => ⟨b₂ m, (ϕ m) fun (i : ι) => v i m⟩) m₀

Consider differentiable maps v₁, ..., vᵢ : M → E₁ to a vector bundle, over a base map b₁ : M → B₁, and another base map b₂ : M → B₂. Given alternating maps ϕ m : E₁ (b₁ m) [⋀^ι]→L[𝕜] E₂ (b₂ m) depending differentiably on m, one can apply ϕ m to (v₁ m, ..., vᵢ m), and the resulting map is differentiable.

Note that the differentiability of ϕ cannot always be stated as differentiability of a map into a manifold, as the pullback bundles b₁ *ᵖ E₁ and b₂ *ᵖ E₂ are smooth manifolds only when b₁ and b₂ are globally smooth, but we want to apply this lemma with only local information. Therefore, we formulate it using differentiability of ϕ read in coordinates.

Version for MDifferentiableWithinAt. We also give a version for MDifferentiableAt, but no version for MDifferentiableOn or MDifferentiable as our assumption, written in coordinates, only makes sense around a point.

For a version with B₁ = B₂ and b₁ = b₂, in which smoothness can be expressed without inCoordinates, see MDifferentiableWithinAt.continuousAlternatingMap_bundle_apply.

theorem MDifferentiableAt.continuousAlternatingMap_apply_of_inCoordinates {𝕜 : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {B₁ : Type u_4} {B₂ : Type u_5} {M : Type u_6} {ι : Type u_7} [Fintype ι] {E₁ : B₁ → Type u_8} {E₂ : B₂ → Type u_9} [NontriviallyNormedField 𝕜] [(x : B₁) → AddCommGroup (E₁ x)] [(x : B₁) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B₁) → TopologicalSpace (E₁ x)] [(x : B₂) → AddCommGroup (E₂ x)] [(x : B₂) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B₂) → TopologicalSpace (E₂ x)] {EB₁ : Type u_10} [NormedAddCommGroup EB₁] [NormedSpace 𝕜 EB₁] {HB₁ : Type u_11} [TopologicalSpace HB₁] {IB₁ : ModelWithCorners 𝕜 EB₁ HB₁} [TopologicalSpace B₁] [ChartedSpace HB₁ B₁] {EB₂ : Type u_12} [NormedAddCommGroup EB₂] [NormedSpace 𝕜 EB₂] {HB₂ : Type u_13} [TopologicalSpace HB₂] {IB₂ : ModelWithCorners 𝕜 EB₂ HB₂} [TopologicalSpace B₂] [ChartedSpace HB₂ B₂] {EM : Type u_14} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_15} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] {b₁ : M → B₁} {b₂ : M → B₂} {m₀ : M} {ϕ : (m : M) → E₁ (b₁ m) [⋀^ι]→L[𝕜] E₂ (b₂ m)} {v : ι → (m : M) → E₁ (b₁ m)} (hϕ : (MDiffAt fun (m : M) => ContinuousAlternatingMap.inCoordinates F₁ F₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀) (hv : ∀ (i : ι), (MDiffAt fun (m : M) => ⟨b₁ m, v i m⟩) m₀) (hb₂ : MDiffAt b₂ m₀) : (MDiffAt fun (m : M) => ⟨b₂ m, (ϕ m) fun (i : ι) => v i m⟩) m₀

Consider differentiable maps v₁, ..., vᵢ : M → E₁ to a vector bundle, over a base map b₁ : M → B₁, and another base map b₂ : M → B₂. Given alternating maps ϕ m : E₁ (b₁ m) [⋀^ι]→L[𝕜] E₂ (b₂ m) depending differentiably on m, one can apply ϕ m to (v₁ m, ..., vᵢ m), and the resulting map is differentiable.

Note that the differentiability of ϕ cannot always be stated as differentiability of a map into a manifold, as the pullback bundles b₁ *ᵖ E₁ and b₂ *ᵖ E₂ are smooth manifolds only when b₁ and b₂ are globally smooth, but we want to apply this lemma with only local information. Therefore, we formulate it using differentiability of ϕ read in coordinates.

Version for MDifferentiableAt. We also give a version for MDifferentiableWithinAt, but no version for MDifferentiableOn or MDifferentiable as our assumption, written in coordinates, only makes sense around a point.

For a version with B₁ = B₂ and b₁ = b₂, in which smoothness can be expressed without inCoordinates, see MDifferentiableAt.continuousAlternatingMap_bundle_apply.

theorem ContMDiffWithinAt.continuousAlternatingMap_bundle_apply {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {M : Type u_6} {ι : Type u_7} [Fintype ι] [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E₁ : B → Type u_8} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_9} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → TopologicalSpace (E₂ x)] {EB : Type u_11} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_12} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_13} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_14} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] {b : M → B} {v : ι → (x : M) → E₁ (b x)} {s : Set M} {x : M} [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] {ϕ : (x : M) → E₁ (b x) [⋀^ι]→L[𝕜] E₂ (b x)} (hϕ : ContMDiffWithinAt IM (IB.prod (modelWithCornersSelf 𝕜 (F₁ [⋀^ι]→L[𝕜] F₂))) n (fun (m : M) => ⟨b m, ϕ m⟩) s x) (hv : ∀ (i : ι), ContMDiffWithinAt IM (IB.prod (modelWithCornersSelf 𝕜 F₁)) n (fun (m : M) => ⟨b m, v i m⟩) s x) : ContMDiffWithinAt IM (IB.prod (modelWithCornersSelf 𝕜 F₂)) n (fun (m : M) => ⟨b m, (ϕ m) fun (i : ι) => v i m⟩) s x

Consider C^n maps vᵢ : M → E₁ to a vector bundle, over a base map b : M → B, and alternating linear maps ϕ m : E₁ (b m) [⋀^ι]→ E₂ (b m) depending smoothly on m. One can apply ϕ m to (v₁ m, ..., vᵢ m), and the resulting map is C^n.

We give here a version of this statement within a set at a point.

theorem ContMDiffAt.continuousAlternatingMap_bundle_apply {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {M : Type u_6} {ι : Type u_7} [Fintype ι] [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E₁ : B → Type u_8} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_9} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → TopologicalSpace (E₂ x)] {EB : Type u_11} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_12} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_13} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_14} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] {b : M → B} {v : ι → (x : M) → E₁ (b x)} {x : M} [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] {ϕ : (x : M) → E₁ (b x) [⋀^ι]→L[𝕜] E₂ (b x)} (hϕ : ContMDiffAt IM (IB.prod (modelWithCornersSelf 𝕜 (F₁ [⋀^ι]→L[𝕜] F₂))) n (fun (m : M) => ⟨b m, ϕ m⟩) x) (hv : ∀ (i : ι), ContMDiffAt IM (IB.prod (modelWithCornersSelf 𝕜 F₁)) n (fun (m : M) => ⟨b m, v i m⟩) x) : ContMDiffAt IM (IB.prod (modelWithCornersSelf 𝕜 F₂)) n (fun (m : M) => ⟨b m, (ϕ m) fun (i : ι) => v i m⟩) x

Consider C^n maps vᵢ : M → E₁ to a vector bundle, over a base map b : M → B, and alternating linear maps ϕ m : E₁ (b m) [⋀^ι]→ E₂ (b m) depending smoothly on m. One can apply ϕ m to (v₁ m, ..., vᵢ m), and the resulting map is C^n.

We give here a version of this statement at a point.

theorem ContMDiffOn.continuousAlternatingMap_bundle_apply {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {M : Type u_6} {ι : Type u_7} [Fintype ι] [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E₁ : B → Type u_8} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_9} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → TopologicalSpace (E₂ x)] {EB : Type u_11} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_12} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_13} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_14} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] {b : M → B} {v : ι → (x : M) → E₁ (b x)} {s : Set M} [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] {ϕ : (x : M) → E₁ (b x) [⋀^ι]→L[𝕜] E₂ (b x)} (hϕ : ContMDiffOn IM (IB.prod (modelWithCornersSelf 𝕜 (F₁ [⋀^ι]→L[𝕜] F₂))) n (fun (m : M) => ⟨b m, ϕ m⟩) s) (hv : ∀ (i : ι), ContMDiffOn IM (IB.prod (modelWithCornersSelf 𝕜 F₁)) n (fun (m : M) => ⟨b m, v i m⟩) s) : ContMDiffOn IM (IB.prod (modelWithCornersSelf 𝕜 F₂)) n (fun (m : M) => ⟨b m, (ϕ m) fun (i : ι) => v i m⟩) s

Consider C^n maps vᵢ : M → E₁ to a vector bundle, over a base map b : M → B, and alternating linear maps ϕ m : E₁ (b m) [⋀^ι]→ E₂ (b m) depending smoothly on m. One can apply ϕ m to (v₁ m, ..., vᵢ m), and the resulting map is C^n.

We give here a version of this statement on a set.

theorem ContMDiff.continuousAlternatingMap_bundle_apply {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {M : Type u_6} {ι : Type u_7} [Fintype ι] [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E₁ : B → Type u_8} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_9} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → TopologicalSpace (E₂ x)] {EB : Type u_11} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_12} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_13} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_14} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] {b : M → B} {v : ι → (x : M) → E₁ (b x)} [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] {ϕ : (x : M) → E₁ (b x) [⋀^ι]→L[𝕜] E₂ (b x)} (hϕ : ContMDiff IM (IB.prod (modelWithCornersSelf 𝕜 (F₁ [⋀^ι]→L[𝕜] F₂))) n fun (m : M) => ⟨b m, ϕ m⟩) (hv : ∀ (i : ι), ContMDiff IM (IB.prod (modelWithCornersSelf 𝕜 F₁)) n fun (m : M) => ⟨b m, v i m⟩) : ContMDiff IM (IB.prod (modelWithCornersSelf 𝕜 F₂)) n fun (m : M) => ⟨b m, (ϕ m) fun (i : ι) => v i m⟩

Consider C^n maps vᵢ : M → E₁ to a vector bundle, over a base map b : M → B, and alternating linear maps ϕ m : E₁ (b m) [⋀^ι]→ E₂ (b m) depending smoothly on m. One can apply ϕ m to (v₁ m, ..., vᵢ m), and the resulting map is C^n.

theorem MDifferentiableWithinAt.continuousAlternatingMap_bundle_apply {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {M : Type u_6} {ι : Type u_7} [Fintype ι] [NontriviallyNormedField 𝕜] {E₁ : B → Type u_8} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_9} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → TopologicalSpace (E₂ x)] {EB : Type u_11} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_12} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_13} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_14} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] {b : M → B} {v : ι → (x : M) → E₁ (b x)} {s : Set M} {x : M} [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] {ϕ : (x : M) → E₁ (b x) [⋀^ι]→L[𝕜] E₂ (b x)} (hϕ : (MDiffAt[s] fun (m : M) => ⟨b m, ϕ m⟩) x) (hv : ∀ (i : ι), (MDiffAt[s] fun (m : M) => ⟨b m, v i m⟩) x) : (MDiffAt[s] fun (m : M) => ⟨b m, (ϕ m) fun (i : ι) => v i m⟩) x

Consider differentiable maps vᵢ : M → E₁ to a vector bundle, over a base map b : M → B, and alternating linear maps ϕ m : E₁ (b m) [⋀^ι]→ E₂ (b m) depending differentiably on m. One can apply ϕ m to (v₁ m, ..., vᵢ m), and the resulting map is differentiable.

We give here a version of this statement within a set at a point.

theorem MDifferentiableAt.continuousAlternatingMap_bundle_apply {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {M : Type u_6} {ι : Type u_7} [Fintype ι] [NontriviallyNormedField 𝕜] {E₁ : B → Type u_8} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_9} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → TopologicalSpace (E₂ x)] {EB : Type u_11} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_12} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_13} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_14} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] {b : M → B} {v : ι → (x : M) → E₁ (b x)} {x : M} [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] {ϕ : (x : M) → E₁ (b x) [⋀^ι]→L[𝕜] E₂ (b x)} (hϕ : (MDiffAt fun (m : M) => ⟨b m, ϕ m⟩) x) (hv : ∀ (i : ι), (MDiffAt fun (m : M) => ⟨b m, v i m⟩) x) : (MDiffAt fun (m : M) => ⟨b m, (ϕ m) fun (i : ι) => v i m⟩) x

Consider differentiable maps vᵢ : M → E₁ to a vector bundle, over a base map b : M → B, and alternating linear maps ϕ m : E₁ (b m) [⋀^ι]→ E₂ (b m) depending differentiably on m. One can apply ϕ m to (v₁ m, ..., vᵢ m), and the resulting map is differentiable.

We give here a version of this statement at a point.

theorem MDifferentiableOn.continuousAlternatingMap_bundle_apply {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {M : Type u_6} {ι : Type u_7} [Fintype ι] [NontriviallyNormedField 𝕜] {E₁ : B → Type u_8} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_9} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → TopologicalSpace (E₂ x)] {EB : Type u_11} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_12} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_13} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_14} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] {b : M → B} {v : ι → (x : M) → E₁ (b x)} {s : Set M} [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] {ϕ : (x : M) → E₁ (b x) [⋀^ι]→L[𝕜] E₂ (b x)} (hϕ : MDiff[s] fun (m : M) => ⟨b m, ϕ m⟩) (hv : ∀ (i : ι), MDiff[s] fun (m : M) => ⟨b m, v i m⟩) : MDiff[s] fun (m : M) => ⟨b m, (ϕ m) fun (i : ι) => v i m⟩

Consider differentiable maps vᵢ : M → E₁ to a vector bundle, over a base map b : M → B, and alternating linear maps ϕ m : E₁ (b m) [⋀^ι]→ E₂ (b m) depending differentiably on m. One can apply ϕ m to (v₁ m, ..., vᵢ m), and the resulting map is differentiable.

We give here a version of this statement on a set.

theorem MDifferentiable.continuousAlternatingMap_bundle_apply {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {M : Type u_6} {ι : Type u_7} [Fintype ι] [NontriviallyNormedField 𝕜] {E₁ : B → Type u_8} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_9} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → TopologicalSpace (E₂ x)] {EB : Type u_11} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_12} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_13} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_14} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] {b : M → B} {v : ι → (x : M) → E₁ (b x)} [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] {ϕ : (x : M) → E₁ (b x) [⋀^ι]→L[𝕜] E₂ (b x)} (hϕ : MDiff fun (m : M) => ⟨b m, ϕ m⟩) (hv : ∀ (i : ι), MDiff fun (m : M) => ⟨b m, v i m⟩) : MDiff fun (m : M) => ⟨b m, (ϕ m) fun (i : ι) => v i m⟩

Consider differentiable maps vᵢ : M → E₁ to a vector bundle, over a base map b : M → B, and alternating linear maps ϕ m : E₁ (b m) [⋀^ι]→ E₂ (b m) depending differentiably on m. One can apply ϕ m to (v₁ m, ..., vᵢ m), and the resulting map is differentiable.