# 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} [] [(x : B) ā AddCommGroup (Eā x)] [(x : B) ā Module š (Eā x)] [] [NormedSpace š Fā] [TopologicalSpace (Bundle.TotalSpace Fā Eā)] [(x : B) ā TopologicalSpace (Eā x)] [(x : B) ā AddCommGroup (Eā x)] [(x : B) ā Module š (Eā x)] [] [NormedSpace š Fā] [TopologicalSpace (Bundle.TotalSpace Fā Eā)] [(x : B) ā TopologicalSpace (Eā x)] {EB : Type u_8} [] [NormedSpace š EB] {HB : Type u_9} [] (IB : ModelWithCorners š EB HB) [] [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] [] [] [] [] :
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} [] [(x : B) ā AddCommGroup (Eā x)] [(x : B) ā Module š (Eā x)] [] [NormedSpace š Fā] [TopologicalSpace (Bundle.TotalSpace Fā Eā)] [(x : B) ā TopologicalSpace (Eā x)] [(x : B) ā AddCommGroup (Eā x)] [(x : B) ā Module š (Eā x)] [] [NormedSpace š Fā] [TopologicalSpace (Bundle.TotalSpace Fā Eā)] [(x : B) ā TopologicalSpace (Eā x)] {HB : Type u_9} [] [] [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} [] [(x : B) ā AddCommGroup (Eā x)] [(x : B) ā Module š (Eā x)] [] [NormedSpace š Fā] [TopologicalSpace (Bundle.TotalSpace Fā Eā)] [(x : B) ā TopologicalSpace (Eā x)] [(x : B) ā AddCommGroup (Eā x)] [(x : B) ā Module š (Eā x)] [] [NormedSpace š Fā] [TopologicalSpace (Bundle.TotalSpace Fā Eā)] [(x : B) ā TopologicalSpace (Eā x)] {EB : Type u_8} [] [NormedSpace š EB] {HB : Type u_9} [] {IB : ModelWithCorners š EB HB} [] [ChartedSpace HB B] {EM : Type u_10} [] [NormedSpace š EM] {HM : Type u_11} [] {IM : ModelWithCorners š EM HM} [] [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} [] [(x : B) ā AddCommGroup (Eā x)] [(x : B) ā Module š (Eā x)] [] [NormedSpace š Fā] [TopologicalSpace (Bundle.TotalSpace Fā Eā)] [(x : B) ā TopologicalSpace (Eā x)] [(x : B) ā AddCommGroup (Eā x)] [(x : B) ā Module š (Eā x)] [] [NormedSpace š Fā] [TopologicalSpace (Bundle.TotalSpace Fā Eā)] [(x : B) ā TopologicalSpace (Eā x)] {EB : Type u_8} [] [NormedSpace š EB] {HB : Type u_9} [] {IB : ModelWithCorners š EB HB} [] [ChartedSpace HB B] {EM : Type u_10} [] [NormedSpace š EM] {HM : Type u_11} [] {IM : ModelWithCorners š EM HM} [] [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} [] [(x : B) ā AddCommGroup (Eā x)] [(x : B) ā Module š (Eā x)] [] [NormedSpace š Fā] [TopologicalSpace (Bundle.TotalSpace Fā Eā)] [(x : B) ā TopologicalSpace (Eā x)] [(x : B) ā AddCommGroup (Eā x)] [(x : B) ā Module š (Eā x)] [] [NormedSpace š Fā] [TopologicalSpace (Bundle.TotalSpace Fā Eā)] [(x : B) ā TopologicalSpace (Eā x)] {EB : Type u_8} [] [NormedSpace š EB] {HB : Type u_9} [] {IB : ModelWithCorners š EB HB} [] [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] :
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} [] [(x : B) ā AddCommGroup (Eā x)] [(x : B) ā Module š (Eā x)] [] [NormedSpace š Fā] [TopologicalSpace (Bundle.TotalSpace Fā Eā)] [(x : B) ā TopologicalSpace (Eā x)] [(x : B) ā AddCommGroup (Eā x)] [(x : B) ā Module š (Eā x)] [] [NormedSpace š Fā] [TopologicalSpace (Bundle.TotalSpace Fā Eā)] [(x : B) ā TopologicalSpace (Eā x)] {EB : Type u_8} [] [NormedSpace š EB] {HB : Type u_9} [] {IB : ModelWithCorners š EB HB} [] [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
• āÆ = āÆ