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 (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)] [āˆ€ (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 (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)] [āˆ€ (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] :
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)] [āˆ€ (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
Equations
  • ⋯ = ⋯