# mathlib3documentation

geometry.manifold.vector_bundle.hom

# 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} [Π (x : B), add_comm_group (E₁ x)] [Π (x : B), (E₁ x)] [ F₁] [topological_space E₁)] [Π (x : B), topological_space (E₁ x)] [Π (x : B), add_comm_group (E₂ x)] [Π (x : B), (E₂ x)] [ F₂] [topological_space E₂)] [Π (x : B), topological_space (E₂ x)] {EB : Type u_12} [ EB] {HB : Type u_13} (IB : HB) [ B] [ E₁] [ F₁ E₁] [ E₂] [ F₂ E₂] {e₁ e₁' : bundle.total_space.proj} {e₂ e₂' : bundle.total_space.proj} [ E₁ IB] [ E₂ IB]  :
((F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂)) e₂') (e₁.base_set e₂.base_set (e₁'.base_set e₂'.base_set))
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} [Π (x : B), add_comm_group (E₁ x)] [Π (x : B), (E₁ x)] [ F₁] [topological_space E₁)] [Π (x : B), topological_space (E₁ x)] [Π (x : B), add_comm_group (E₂ x)] [Π (x : B), (E₂ x)] [ F₂] [topological_space E₂)] [Π (x : B), topological_space (E₂ x)] [ (x : B), topological_add_group (E₂ x)] [ (x : B), (E₂ x)] {HB : Type u_13} [ B] [ E₁] [ F₁ E₁] [ E₂] [ F₂ E₂] (y₀ y : bundle.total_space (F₁ →L[𝕜] F₂) E₂)) :
(charted_space.chart_at (model_prod HB (F₁ →L[𝕜] F₂)) y₀) y = ( y₀.proj) y.proj, 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} [Π (x : B), add_comm_group (E₁ x)] [Π (x : B), (E₁ x)] [ F₁] [topological_space E₁)] [Π (x : B), topological_space (E₁ x)] [Π (x : B), add_comm_group (E₂ x)] [Π (x : B), (E₂ x)] [ F₂] [topological_space E₂)] [Π (x : B), topological_space (E₂ x)] [ (x : B), topological_add_group (E₂ x)] [ (x : B), (E₂ x)] {EB : Type u_12} [ EB] {HB : Type u_13} {IB : HB} [ B] {EM : Type u_14} [ EM] {HM : Type u_15} {IM : HM} [ M] [ E₁] [ F₁ E₁] [ E₂] [ F₂ E₂] (f : M bundle.total_space (F₁ →L[𝕜] F₂) E₂)) {x₀ : M} {n : ℕ∞} :
(IB.prod (F₁ →L[𝕜] F₂))) n f x₀ IB n (λ (x : M), (f x).proj) x₀ (F₁ →L[𝕜] F₂)) n (λ (x : M), 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} [Π (x : B), add_comm_group (E₁ x)] [Π (x : B), (E₁ x)] [ F₁] [topological_space E₁)] [Π (x : B), topological_space (E₁ x)] [Π (x : B), add_comm_group (E₂ x)] [Π (x : B), (E₂ x)] [ F₂] [topological_space E₂)] [Π (x : B), topological_space (E₂ x)] [ (x : B), topological_add_group (E₂ x)] [ (x : B), (E₂ x)] {EB : Type u_12} [ EB] {HB : Type u_13} {IB : HB} [ B] {EM : Type u_14} [ EM] {HM : Type u_15} {IM : HM} [ M] [ E₁] [ F₁ E₁] [ E₂] [ F₂ E₂] (f : M bundle.total_space (F₁ →L[𝕜] F₂) E₂)) {x₀ : M} :
(IB.prod (F₁ →L[𝕜] F₂))) f x₀ IB (λ (x : M), (f x).proj) x₀ (F₁ →L[𝕜] F₂)) (λ (x : M), E₂ (f x₀).proj (f x).proj (f x₀).proj (f x).proj (f x).snd) x₀
@[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} [Π (x : B), add_comm_group (E₁ x)] [Π (x : B), (E₁ x)] [ F₁] [topological_space E₁)] [Π (x : B), topological_space (E₁ x)] [Π (x : B), add_comm_group (E₂ x)] [Π (x : B), (E₂ x)] [ F₂] [topological_space E₂)] [Π (x : B), topological_space (E₂ x)] [ (x : B), topological_add_group (E₂ x)] [ (x : B), (E₂ x)] {EB : Type u_12} [ EB] {HB : Type u_13} {IB : HB} [ B] [ E₁] [ F₁ E₁] [ E₂] [ F₂ E₂] [ E₁ IB] [ E₂ IB] :
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} [Π (x : B), add_comm_group (E₁ x)] [Π (x : B), (E₁ x)] [ F₁] [topological_space E₁)] [Π (x : B), topological_space (E₁ x)] [Π (x : B), add_comm_group (E₂ x)] [Π (x : B), (E₂ x)] [ F₂] [topological_space E₂)] [Π (x : B), topological_space (E₂ x)] [ (x : B), topological_add_group (E₂ x)] [ (x : B), (E₂ x)] {EB : Type u_12} [ EB] {HB : Type u_13} {IB : HB} [ B] [ E₁] [ F₁ E₁] [ E₂] [ F₂ E₂] [ E₁ IB] [ E₂ IB] :
smooth_vector_bundle (F₁ →L[𝕜] F₂) E₂) IB