Homs of smooth vector bundles over the same base space

Here we show that Bundle.ContinuousLinearMap is a smooth vector bundle.

Note that we only do this for bundles of linear maps, not for bundles of arbitrary semilinear maps. To do it for semilinear maps, we would need to generalize ContinuousLinearMap.contMDiff (and ContinuousLinearMap.contDiff) to semilinear maps.

theorem smoothOn_continuousLinearMapCoordChange {𝕜 : 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)] {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₁ : Trivialization F₁ Bundle.TotalSpace.proj} {e₁' : Trivialization F₁ Bundle.TotalSpace.proj} {e₂ : Trivialization F₂ Bundle.TotalSpace.proj} {e₂' : Trivialization F₂ Bundle.TotalSpace.proj} [SmoothVectorBundle F₁ E₁ IB] [SmoothVectorBundle F₂ E₂ IB] [MemTrivializationAtlas e₁] [MemTrivializationAtlas e₁'] [MemTrivializationAtlas e₂] [MemTrivializationAtlas e₂'] : SmoothOn IB (modelWithCornersSelf 𝕜 ((F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂)) (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), TopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] (y₀ : Bundle.TotalSpace (F₁ →L[𝕜] F₂) (Bundle.ContinuousLinearMap (RingHom.id 𝕜) E₁ E₂)) (y : Bundle.TotalSpace (F₁ →L[𝕜] F₂) (Bundle.ContinuousLinearMap (RingHom.id 𝕜) E₁ E₂)) : ↑(chartAt (ModelProd HB (F₁ →L[𝕜] F₂)) y₀) y = (↑(chartAt HB y₀.proj) y.proj, ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ y₀.proj y.proj y₀.proj y.proj y.snd)

theorem contMDiffAt_hom_bundle {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {M : Type u_5} {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), TopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] (f : M → Bundle.TotalSpace (F₁ →L[𝕜] F₂) (Bundle.ContinuousLinearMap (RingHom.id 𝕜) E₁ E₂)) {x₀ : M} {n : ℕ∞} : 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₀

theorem smoothAt_hom_bundle {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {M : Type u_5} {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), TopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] (f : M → Bundle.TotalSpace (F₁ →L[𝕜] F₂) (Bundle.ContinuousLinearMap (RingHom.id 𝕜) E₁ E₂)) {x₀ : M} : SmoothAt IM (IB.prod (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂))) f x₀ ↔ SmoothAt IM IB (fun (x : M) => (f x).proj) x₀ ∧ SmoothAt IM (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) (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₀

instance Bundle.ContinuousLinearMap.vectorPrebundle.isSmooth {𝕜 : 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)] {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), TopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] [SmoothVectorBundle F₁ E₁ IB] [SmoothVectorBundle F₂ E₂ IB] : VectorPrebundle.IsSmooth IB (Bundle.ContinuousLinearMap.vectorPrebundle (RingHom.id 𝕜) F₁ E₁ F₂ E₂)

Equations

• ⋯ = ⋯

instance SmoothVectorBundle.continuousLinearMap {𝕜 : 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)] {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), TopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] [SmoothVectorBundle F₁ E₁ IB] [SmoothVectorBundle F₂ E₂ IB] : SmoothVectorBundle (F₁ →L[𝕜] F₂) (Bundle.ContinuousLinearMap (RingHom.id 𝕜) E₁ E₂) IB

Equations

• ⋯ = ⋯