Homs of smooth vector bundles over the same base space #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Here we show that bundle.continuous_linear_map 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 continuous_linear_map.cont_mdiff
(and continuous_linear_map.cont_diff) to semilinear maps.
theorem
smooth_on_continuous_linear_map_coord_change
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_4}
{F₂ : Type u_5}
{E₁ : B → Type u_10}
{E₂ : B → Type u_11}
[nontrivially_normed_field 𝕜]
[Π (x : B), add_comm_group (E₁ x)]
[Π (x : B), module 𝕜 (E₁ x)]
[normed_add_comm_group F₁]
[normed_space 𝕜 F₁]
[topological_space (bundle.total_space F₁ E₁)]
[Π (x : B), topological_space (E₁ x)]
[Π (x : B), add_comm_group (E₂ x)]
[Π (x : B), module 𝕜 (E₂ x)]
[normed_add_comm_group F₂]
[normed_space 𝕜 F₂]
[topological_space (bundle.total_space F₂ E₂)]
[Π (x : B), topological_space (E₂ x)]
{EB : Type u_12}
[normed_add_comm_group EB]
[normed_space 𝕜 EB]
{HB : Type u_13}
[topological_space HB]
(IB : model_with_corners 𝕜 EB HB)
[topological_space B]
[charted_space HB B]
[fiber_bundle F₁ E₁]
[vector_bundle 𝕜 F₁ E₁]
[fiber_bundle F₂ E₂]
[vector_bundle 𝕜 F₂ E₂]
{e₁ e₁' : trivialization F₁ bundle.total_space.proj}
{e₂ e₂' : trivialization F₂ bundle.total_space.proj}
[smooth_manifold_with_corners IB B]
[smooth_vector_bundle F₁ E₁ IB]
[smooth_vector_bundle F₂ E₂ IB]
[mem_trivialization_atlas e₁]
[mem_trivialization_atlas e₁']
[mem_trivialization_atlas e₂]
[mem_trivialization_atlas e₂'] :
theorem
hom_chart
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_4}
{F₂ : Type u_5}
{E₁ : B → Type u_10}
{E₂ : B → Type u_11}
[nontrivially_normed_field 𝕜]
[Π (x : B), add_comm_group (E₁ x)]
[Π (x : B), module 𝕜 (E₁ x)]
[normed_add_comm_group F₁]
[normed_space 𝕜 F₁]
[topological_space (bundle.total_space F₁ E₁)]
[Π (x : B), topological_space (E₁ x)]
[Π (x : B), add_comm_group (E₂ x)]
[Π (x : B), module 𝕜 (E₂ x)]
[normed_add_comm_group F₂]
[normed_space 𝕜 F₂]
[topological_space (bundle.total_space F₂ E₂)]
[Π (x : B), topological_space (E₂ x)]
[∀ (x : B), topological_add_group (E₂ x)]
[∀ (x : B), has_continuous_smul 𝕜 (E₂ x)]
{HB : Type u_13}
[topological_space HB]
[topological_space B]
[charted_space HB B]
[fiber_bundle F₁ E₁]
[vector_bundle 𝕜 F₁ E₁]
[fiber_bundle F₂ E₂]
[vector_bundle 𝕜 F₂ E₂]
(y₀ y : bundle.total_space (F₁ →L[𝕜] F₂) (bundle.continuous_linear_map (ring_hom.id 𝕜) E₁ E₂)) :
⇑(charted_space.chart_at (model_prod HB (F₁ →L[𝕜] F₂)) y₀) y = (⇑(charted_space.chart_at HB y₀.proj) y.proj, continuous_linear_map.in_coordinates F₁ E₁ F₂ E₂ y₀.proj y.proj y₀.proj y.proj y.snd)
theorem
cont_mdiff_at_hom_bundle
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_4}
{F₂ : Type u_5}
{M : Type u_6}
{E₁ : B → Type u_10}
{E₂ : B → Type u_11}
[nontrivially_normed_field 𝕜]
[Π (x : B), add_comm_group (E₁ x)]
[Π (x : B), module 𝕜 (E₁ x)]
[normed_add_comm_group F₁]
[normed_space 𝕜 F₁]
[topological_space (bundle.total_space F₁ E₁)]
[Π (x : B), topological_space (E₁ x)]
[Π (x : B), add_comm_group (E₂ x)]
[Π (x : B), module 𝕜 (E₂ x)]
[normed_add_comm_group F₂]
[normed_space 𝕜 F₂]
[topological_space (bundle.total_space F₂ E₂)]
[Π (x : B), topological_space (E₂ x)]
[∀ (x : B), topological_add_group (E₂ x)]
[∀ (x : B), has_continuous_smul 𝕜 (E₂ x)]
{EB : Type u_12}
[normed_add_comm_group EB]
[normed_space 𝕜 EB]
{HB : Type u_13}
[topological_space HB]
{IB : model_with_corners 𝕜 EB HB}
[topological_space B]
[charted_space HB B]
{EM : Type u_14}
[normed_add_comm_group EM]
[normed_space 𝕜 EM]
{HM : Type u_15}
[topological_space HM]
{IM : model_with_corners 𝕜 EM HM}
[topological_space M]
[charted_space HM M]
[fiber_bundle F₁ E₁]
[vector_bundle 𝕜 F₁ E₁]
[fiber_bundle F₂ E₂]
[vector_bundle 𝕜 F₂ E₂]
(f : M → bundle.total_space (F₁ →L[𝕜] F₂) (bundle.continuous_linear_map (ring_hom.id 𝕜) E₁ E₂))
{x₀ : M}
{n : ℕ∞} :
cont_mdiff_at IM (IB.prod (model_with_corners_self 𝕜 (F₁ →L[𝕜] F₂))) n f x₀ ↔ cont_mdiff_at IM IB n (λ (x : M), (f x).proj) x₀ ∧ cont_mdiff_at IM (model_with_corners_self 𝕜 (F₁ →L[𝕜] F₂)) n (λ (x : M), continuous_linear_map.in_coordinates F₁ E₁ F₂ E₂ (f x₀).proj (f x).proj (f x₀).proj (f x).proj (f x).snd) x₀
theorem
smooth_at_hom_bundle
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_4}
{F₂ : Type u_5}
{M : Type u_6}
{E₁ : B → Type u_10}
{E₂ : B → Type u_11}
[nontrivially_normed_field 𝕜]
[Π (x : B), add_comm_group (E₁ x)]
[Π (x : B), module 𝕜 (E₁ x)]
[normed_add_comm_group F₁]
[normed_space 𝕜 F₁]
[topological_space (bundle.total_space F₁ E₁)]
[Π (x : B), topological_space (E₁ x)]
[Π (x : B), add_comm_group (E₂ x)]
[Π (x : B), module 𝕜 (E₂ x)]
[normed_add_comm_group F₂]
[normed_space 𝕜 F₂]
[topological_space (bundle.total_space F₂ E₂)]
[Π (x : B), topological_space (E₂ x)]
[∀ (x : B), topological_add_group (E₂ x)]
[∀ (x : B), has_continuous_smul 𝕜 (E₂ x)]
{EB : Type u_12}
[normed_add_comm_group EB]
[normed_space 𝕜 EB]
{HB : Type u_13}
[topological_space HB]
{IB : model_with_corners 𝕜 EB HB}
[topological_space B]
[charted_space HB B]
{EM : Type u_14}
[normed_add_comm_group EM]
[normed_space 𝕜 EM]
{HM : Type u_15}
[topological_space HM]
{IM : model_with_corners 𝕜 EM HM}
[topological_space M]
[charted_space HM M]
[fiber_bundle F₁ E₁]
[vector_bundle 𝕜 F₁ E₁]
[fiber_bundle F₂ E₂]
[vector_bundle 𝕜 F₂ E₂]
(f : M → bundle.total_space (F₁ →L[𝕜] F₂) (bundle.continuous_linear_map (ring_hom.id 𝕜) E₁ E₂))
{x₀ : M} :
@[protected, instance]
def
bundle.continuous_linear_map.vector_prebundle.is_smooth
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_4}
{F₂ : Type u_5}
{E₁ : B → Type u_10}
{E₂ : B → Type u_11}
[nontrivially_normed_field 𝕜]
[Π (x : B), add_comm_group (E₁ x)]
[Π (x : B), module 𝕜 (E₁ x)]
[normed_add_comm_group F₁]
[normed_space 𝕜 F₁]
[topological_space (bundle.total_space F₁ E₁)]
[Π (x : B), topological_space (E₁ x)]
[Π (x : B), add_comm_group (E₂ x)]
[Π (x : B), module 𝕜 (E₂ x)]
[normed_add_comm_group F₂]
[normed_space 𝕜 F₂]
[topological_space (bundle.total_space F₂ E₂)]
[Π (x : B), topological_space (E₂ x)]
[∀ (x : B), topological_add_group (E₂ x)]
[∀ (x : B), has_continuous_smul 𝕜 (E₂ x)]
{EB : Type u_12}
[normed_add_comm_group EB]
[normed_space 𝕜 EB]
{HB : Type u_13}
[topological_space HB]
{IB : model_with_corners 𝕜 EB HB}
[topological_space B]
[charted_space HB B]
[fiber_bundle F₁ E₁]
[vector_bundle 𝕜 F₁ E₁]
[fiber_bundle F₂ E₂]
[vector_bundle 𝕜 F₂ E₂]
[smooth_manifold_with_corners IB B]
[smooth_vector_bundle F₁ E₁ IB]
[smooth_vector_bundle F₂ E₂ IB] :
vector_prebundle.is_smooth IB (bundle.continuous_linear_map.vector_prebundle (ring_hom.id 𝕜) F₁ E₁ F₂ E₂)
@[protected, instance]
def
smooth_vector_bundle.continuous_linear_map
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_4}
{F₂ : Type u_5}
{E₁ : B → Type u_10}
{E₂ : B → Type u_11}
[nontrivially_normed_field 𝕜]
[Π (x : B), add_comm_group (E₁ x)]
[Π (x : B), module 𝕜 (E₁ x)]
[normed_add_comm_group F₁]
[normed_space 𝕜 F₁]
[topological_space (bundle.total_space F₁ E₁)]
[Π (x : B), topological_space (E₁ x)]
[Π (x : B), add_comm_group (E₂ x)]
[Π (x : B), module 𝕜 (E₂ x)]
[normed_add_comm_group F₂]
[normed_space 𝕜 F₂]
[topological_space (bundle.total_space F₂ E₂)]
[Π (x : B), topological_space (E₂ x)]
[∀ (x : B), topological_add_group (E₂ x)]
[∀ (x : B), has_continuous_smul 𝕜 (E₂ x)]
{EB : Type u_12}
[normed_add_comm_group EB]
[normed_space 𝕜 EB]
{HB : Type u_13}
[topological_space HB]
{IB : model_with_corners 𝕜 EB HB}
[topological_space B]
[charted_space HB B]
[fiber_bundle F₁ E₁]
[vector_bundle 𝕜 F₁ E₁]
[fiber_bundle F₂ E₂]
[vector_bundle 𝕜 F₂ E₂]
[smooth_manifold_with_corners IB B]
[smooth_vector_bundle F₁ E₁ IB]
[smooth_vector_bundle F₂ E₂ IB] :
smooth_vector_bundle (F₁ →L[𝕜] F₂) (bundle.continuous_linear_map (ring_hom.id 𝕜) E₁ E₂) IB