Homs of C^n vector bundles over the same base space #
Here we show that the bundle of continuous linear maps is a C^n vector bundle. We also show
that applying a smooth family of linear maps to a smooth family of vectors gives a smooth
result, in several versions.
Note that we only do this for bundles of linear maps, not for bundles of arbitrary semilinear maps.
Indeed, semilinear maps are typically not smooth. For instance, complex conjugation is not
ℂ-differentiable.
theorem
contMDiffOn_continuousLinearMapCoordChange
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{n : WithTop ℕ∞}
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[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_8}
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
{HB : Type u_9}
[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₁' : Trivialization F₁ Bundle.TotalSpace.proj}
{e₂ e₂' : Trivialization F₂ Bundle.TotalSpace.proj}
[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
(Pretrivialization.continuousLinearMapCoordChange (RingHom.id 𝕜) e₁ e₁' e₂ e₂')
(e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
@[deprecated contMDiffOn_continuousLinearMapCoordChange (since := "2024-11-21")]
theorem
smoothOn_continuousLinearMapCoordChange
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{n : WithTop ℕ∞}
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[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_8}
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
{HB : Type u_9}
[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₁' : Trivialization F₁ Bundle.TotalSpace.proj}
{e₂ e₂' : Trivialization F₂ Bundle.TotalSpace.proj}
[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
(Pretrivialization.continuousLinearMapCoordChange (RingHom.id 𝕜) e₁ e₁' e₂ e₂')
(e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
theorem
hom_chart
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[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_9}
[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)
:
theorem
contMDiffWithinAt_hom_bundle
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{M : Type u_5}
{n : WithTop ℕ∞}
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[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_8}
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
{HB : Type u_9}
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
{EM : Type u_10}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_11}
[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) =>
ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ (f x₀).proj (f x).proj (f x₀).proj (f x).proj (f x).snd)
s x₀
theorem
contMDiffAt_hom_bundle
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{M : Type u_5}
{n : WithTop ℕ∞}
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[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_8}
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
{HB : Type u_9}
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
{EM : Type u_10}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_11}
[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) =>
ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ (f x₀).proj (f x).proj (f x₀).proj (f x).proj (f x).snd)
x₀
@[deprecated contMDiffAt_hom_bundle (since := "2024-11-21")]
theorem
smoothAt_hom_bundle
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{M : Type u_5}
{n : WithTop ℕ∞}
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[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_8}
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
{HB : Type u_9}
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
{EM : Type u_10}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_11}
[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) =>
ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ (f x₀).proj (f x).proj (f x₀).proj (f x).proj (f x).snd)
x₀
Alias of contMDiffAt_hom_bundle.
instance
Bundle.ContinuousLinearMap.vectorPrebundle.isContMDiff
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{n : WithTop ℕ∞}
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[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_8}
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
{HB : Type u_9}
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB 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)]
[ContMDiffVectorBundle n F₁ E₁ IB]
[ContMDiffVectorBundle n F₂ E₂ IB]
:
VectorPrebundle.IsContMDiff IB (vectorPrebundle (RingHom.id 𝕜) F₁ E₁ F₂ E₂) n
@[deprecated Bundle.ContinuousLinearMap.vectorPrebundle.isContMDiff (since := "2025-01-09")]
theorem
Bundle.ContinuousLinearMap.vectorPrebundle.isSmooth
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{n : WithTop ℕ∞}
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[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_8}
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
{HB : Type u_9}
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB 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)]
[ContMDiffVectorBundle n F₁ E₁ IB]
[ContMDiffVectorBundle n F₂ E₂ IB]
:
VectorPrebundle.IsContMDiff IB (vectorPrebundle (RingHom.id 𝕜) F₁ E₁ F₂ E₂) n
Alias of Bundle.ContinuousLinearMap.vectorPrebundle.isContMDiff.
instance
ContMDiffVectorBundle.continuousLinearMap
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{n : WithTop ℕ∞}
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[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_8}
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
{HB : Type u_9}
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB 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)]
[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.clm_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}
{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₁]
{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]
{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) => ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) s m₀)
(hv : ContMDiffWithinAt IM (IB₁.prod (modelWithCornersSelf 𝕜 F₁)) n (fun (m : M) => { proj := b₁ m, snd := v m }) s m₀)
(hb₂ : ContMDiffWithinAt IM IB₂ n b₂ s m₀)
:
ContMDiffWithinAt IM (IB₂.prod (modelWithCornersSelf 𝕜 F₂)) n (fun (m : M) => { proj := b₂ m, snd := (ϕ m) (v m) }) s 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 g m, and the resulting map is C^n.
Note that the smoothness of ϕ can not be 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.clm_bundle_apply
theorem
ContMDiffAt.clm_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}
{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₁]
{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]
{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) => ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀)
(hv : ContMDiffAt IM (IB₁.prod (modelWithCornersSelf 𝕜 F₁)) n (fun (m : M) => { proj := b₁ m, snd := v m }) m₀)
(hb₂ : ContMDiffAt IM IB₂ n b₂ m₀)
:
ContMDiffAt IM (IB₂.prod (modelWithCornersSelf 𝕜 F₂)) n (fun (m : M) => { proj := b₂ m, snd := (ϕ m) (v 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 g m, and the resulting map is C^n.
Note that the smoothness of ϕ can not be 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.clm_bundle_apply
theorem
ContMDiffWithinAt.clm_bundle_apply
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{M : Type u_6}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{E₁ : B → Type u_7}
[(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_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)]
{EB : Type u_10}
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
{HB : Type u_11}
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
{EM : Type u_12}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_13}
[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) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂) (b m) (ϕ m)) s x)
(hv :
ContMDiffWithinAt IM (IB.prod (modelWithCornersSelf 𝕜 F₁)) n (fun (m : M) => Bundle.TotalSpace.mk' F₁ (b m) (v m)) s
x)
:
ContMDiffWithinAt IM (IB.prod (modelWithCornersSelf 𝕜 F₂)) n
(fun (m : M) => Bundle.TotalSpace.mk' F₂ (b m) ((ϕ m) (v m))) s x
Consider a C^n map v : M → E₁ to a vector bundle, over a base map b : M → B, and
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.
We give here a version of this statement within a set at a point.
theorem
ContMDiffAt.clm_bundle_apply
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{M : Type u_6}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{E₁ : B → Type u_7}
[(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_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)]
{EB : Type u_10}
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
{HB : Type u_11}
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
{EM : Type u_12}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_13}
[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) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂) (b m) (ϕ m)) x)
(hv : ContMDiffAt IM (IB.prod (modelWithCornersSelf 𝕜 F₁)) n (fun (m : M) => Bundle.TotalSpace.mk' F₁ (b m) (v m)) x)
:
ContMDiffAt IM (IB.prod (modelWithCornersSelf 𝕜 F₂)) n (fun (m : M) => Bundle.TotalSpace.mk' F₂ (b m) ((ϕ m) (v m))) x
Consider a C^n map v : M → E₁ to a vector bundle, over a base map b : M → B, and
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.
We give here a version of this statement at a point.
theorem
ContMDiffOn.clm_bundle_apply
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{M : Type u_6}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{E₁ : B → Type u_7}
[(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_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)]
{EB : Type u_10}
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
{HB : Type u_11}
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
{EM : Type u_12}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_13}
[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) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂) (b m) (ϕ m)) s)
(hv : ContMDiffOn IM (IB.prod (modelWithCornersSelf 𝕜 F₁)) n (fun (m : M) => Bundle.TotalSpace.mk' F₁ (b m) (v m)) s)
:
ContMDiffOn IM (IB.prod (modelWithCornersSelf 𝕜 F₂)) n (fun (m : M) => Bundle.TotalSpace.mk' F₂ (b m) ((ϕ m) (v m))) s
Consider a C^n map v : M → E₁ to a vector bundle, over a base map b : M → B, and
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.
We give here a version of this statement on a set.
theorem
ContMDiff.clm_bundle_apply
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{M : Type u_6}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{E₁ : B → Type u_7}
[(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_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)]
{EB : Type u_10}
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
{HB : Type u_11}
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
{EM : Type u_12}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_13}
[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) =>
Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂) (b m) (ϕ m))
(hv : ContMDiff IM (IB.prod (modelWithCornersSelf 𝕜 F₁)) n fun (m : M) => Bundle.TotalSpace.mk' F₁ (b m) (v m))
:
ContMDiff IM (IB.prod (modelWithCornersSelf 𝕜 F₂)) n fun (m : M) => Bundle.TotalSpace.mk' F₂ (b m) ((ϕ m) (v m))
Consider a C^n map v : M → E₁ to a vector bundle, over a base map b : M → B, and
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.
theorem
ContMDiffWithinAt.clm_bundle_apply₂
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{F₃ : Type u_5}
{M : Type u_6}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{E₁ : B → Type u_7}
[(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_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_10}
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
{HB : Type u_11}
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
{EM : Type u_12}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_13}
[TopologicalSpace HM]
{IM : ModelWithCorners 𝕜 EM HM}
[TopologicalSpace M]
[ChartedSpace HM M]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
[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) →L[𝕜] E₃ (b x)}
{w : (x : M) → E₂ (b x)}
(hψ :
ContMDiffWithinAt IM (IB.prod (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂ →L[𝕜] F₃))) n
(fun (m : M) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂ →L[𝕜] F₃) (b m) (ψ m)) s x)
(hv :
ContMDiffWithinAt IM (IB.prod (modelWithCornersSelf 𝕜 F₁)) n (fun (m : M) => Bundle.TotalSpace.mk' F₁ (b m) (v m)) s
x)
(hw :
ContMDiffWithinAt IM (IB.prod (modelWithCornersSelf 𝕜 F₂)) n (fun (m : M) => Bundle.TotalSpace.mk' F₂ (b m) (w m)) s
x)
:
ContMDiffWithinAt IM (IB.prod (modelWithCornersSelf 𝕜 F₃)) n
(fun (m : M) => Bundle.TotalSpace.mk' F₃ (b m) (((ψ m) (v m)) (w m))) s x
Consider C^n maps v : M → E₁ and v : M → E₂ to vector bundles, over a base map
b : M → B, and bilinear maps ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m) depending smoothly on m.
One can apply ψ m to v m and w m, and the resulting map is C^n.
We give here a version of this statement within a set at a point.
theorem
ContMDiffAt.clm_bundle_apply₂
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{F₃ : Type u_5}
{M : Type u_6}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{E₁ : B → Type u_7}
[(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_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_10}
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
{HB : Type u_11}
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
{EM : Type u_12}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_13}
[TopologicalSpace HM]
{IM : ModelWithCorners 𝕜 EM HM}
[TopologicalSpace M]
[ChartedSpace HM M]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
[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) →L[𝕜] E₃ (b x)}
{w : (x : M) → E₂ (b x)}
(hψ :
ContMDiffAt IM (IB.prod (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂ →L[𝕜] F₃))) n
(fun (m : M) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂ →L[𝕜] F₃) (b m) (ψ m)) x)
(hv : ContMDiffAt IM (IB.prod (modelWithCornersSelf 𝕜 F₁)) n (fun (m : M) => Bundle.TotalSpace.mk' F₁ (b m) (v m)) x)
(hw : ContMDiffAt IM (IB.prod (modelWithCornersSelf 𝕜 F₂)) n (fun (m : M) => Bundle.TotalSpace.mk' F₂ (b m) (w m)) x)
:
ContMDiffAt IM (IB.prod (modelWithCornersSelf 𝕜 F₃)) n
(fun (m : M) => Bundle.TotalSpace.mk' F₃ (b m) (((ψ m) (v m)) (w m))) x
Consider C^n maps v : M → E₁ and v : M → E₂ to vector bundles, over a base map
b : M → B, and bilinear maps ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m) depending smoothly on m.
One can apply ψ m to v m and w m, and the resulting map is C^n.
We give here a version of this statement at a point.
theorem
ContMDiffOn.clm_bundle_apply₂
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{F₃ : Type u_5}
{M : Type u_6}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{E₁ : B → Type u_7}
[(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_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_10}
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
{HB : Type u_11}
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
{EM : Type u_12}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_13}
[TopologicalSpace HM]
{IM : ModelWithCorners 𝕜 EM HM}
[TopologicalSpace M]
[ChartedSpace HM M]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
[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) →L[𝕜] E₃ (b x)}
{w : (x : M) → E₂ (b x)}
(hψ :
ContMDiffOn IM (IB.prod (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂ →L[𝕜] F₃))) n
(fun (m : M) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂ →L[𝕜] F₃) (b m) (ψ m)) s)
(hv : ContMDiffOn IM (IB.prod (modelWithCornersSelf 𝕜 F₁)) n (fun (m : M) => Bundle.TotalSpace.mk' F₁ (b m) (v m)) s)
(hw : ContMDiffOn IM (IB.prod (modelWithCornersSelf 𝕜 F₂)) n (fun (m : M) => Bundle.TotalSpace.mk' F₂ (b m) (w m)) s)
:
ContMDiffOn IM (IB.prod (modelWithCornersSelf 𝕜 F₃)) n
(fun (m : M) => Bundle.TotalSpace.mk' F₃ (b m) (((ψ m) (v m)) (w m))) s
Consider C^n maps v : M → E₁ and v : M → E₂ to vector bundles, over a base map
b : M → B, and bilinear maps ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m) depending smoothly on m.
One can apply ψ m to v m and w m, and the resulting map is C^n.
We give here a version of this statement on a set.
theorem
ContMDiff.clm_bundle_apply₂
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{F₃ : Type u_5}
{M : Type u_6}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{E₁ : B → Type u_7}
[(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_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_10}
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
{HB : Type u_11}
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
{EM : Type u_12}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_13}
[TopologicalSpace HM]
{IM : ModelWithCorners 𝕜 EM HM}
[TopologicalSpace M]
[ChartedSpace HM M]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
[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) →L[𝕜] E₃ (b x)}
{w : (x : M) → E₂ (b x)}
(hψ :
ContMDiff IM (IB.prod (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂ →L[𝕜] F₃))) n fun (m : M) =>
Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂ →L[𝕜] F₃) (b m) (ψ m))
(hv : ContMDiff IM (IB.prod (modelWithCornersSelf 𝕜 F₁)) n fun (m : M) => Bundle.TotalSpace.mk' F₁ (b m) (v m))
(hw : ContMDiff IM (IB.prod (modelWithCornersSelf 𝕜 F₂)) n fun (m : M) => Bundle.TotalSpace.mk' F₂ (b m) (w m))
:
ContMDiff IM (IB.prod (modelWithCornersSelf 𝕜 F₃)) n fun (m : M) => Bundle.TotalSpace.mk' F₃ (b m) (((ψ m) (v m)) (w m))
Consider C^n maps v : M → E₁ and v : M → E₂ to vector bundles, over a base map
b : M → B, and bilinear maps ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m) depending smoothly on m.
One can apply ψ m to v m and w m, and the resulting map is C^n.