Documentation

Mathlib.Geometry.Manifold.VectorBundle.Hom

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)] [āˆ€ (x : B), TopologicalAddGroup (Eā‚‚ x)] [āˆ€ (x : B), ContinuousSMul š•œ (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ā‚‚] (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)] [āˆ€ (x : B), TopologicalAddGroup (Eā‚‚ x)] [āˆ€ (x : B), ContinuousSMul š•œ (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ā‚‚] (f : M ā†’ Bundle.TotalSpace (Fā‚ ā†’L[š•œ] Fā‚‚) (Bundle.ContinuousLinearMap (RingHom.id š•œ) Eā‚ Eā‚‚)) {xā‚€ : M} {n : ā„•āˆž} :
ContMDiffAt IM (ModelWithCorners.prod IB (modelWithCornersSelf š•œ (Fā‚ ā†’L[š•œ] Fā‚‚))) n f xā‚€ ā†” ContMDiffAt IM IB n (fun x => (f x).proj) xā‚€ āˆ§ ContMDiffAt IM (modelWithCornersSelf š•œ (Fā‚ ā†’L[š•œ] Fā‚‚)) n (fun x => 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)] [āˆ€ (x : B), TopologicalAddGroup (Eā‚‚ x)] [āˆ€ (x : B), ContinuousSMul š•œ (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ā‚‚] (f : M ā†’ Bundle.TotalSpace (Fā‚ ā†’L[š•œ] Fā‚‚) (Bundle.ContinuousLinearMap (RingHom.id š•œ) Eā‚ Eā‚‚)) {xā‚€ : M} :
SmoothAt IM (ModelWithCorners.prod IB (modelWithCornersSelf š•œ (Fā‚ ā†’L[š•œ] Fā‚‚))) f xā‚€ ā†” SmoothAt IM IB (fun x => (f x).proj) xā‚€ āˆ§ SmoothAt IM (modelWithCornersSelf š•œ (Fā‚ ā†’L[š•œ] Fā‚‚)) (fun x => 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)] [āˆ€ (x : B), TopologicalAddGroup (Eā‚‚ x)] [āˆ€ (x : B), ContinuousSMul š•œ (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ā‚‚] [SmoothVectorBundle Fā‚ Eā‚ IB] [SmoothVectorBundle Fā‚‚ Eā‚‚ IB] :
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)] [āˆ€ (x : B), TopologicalAddGroup (Eā‚‚ x)] [āˆ€ (x : B), ContinuousSMul š•œ (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ā‚‚] [SmoothVectorBundle Fā‚ Eā‚ IB] [SmoothVectorBundle Fā‚‚ Eā‚‚ IB] :
SmoothVectorBundle (Fā‚ ā†’L[š•œ] Fā‚‚) (Bundle.ContinuousLinearMap (RingHom.id š•œ) Eā‚ Eā‚‚) IB