Direct sum of two vector bundles #
If E₁ : B → Type* and E₂ : B → Type* define two topological vector bundles over R with fiber
models F₁ and F₂, we define the bundle of direct sums E₁ ×ᵇ E₂ := λ x, E₁ x × E₂ x.
We can endow E₁ ×ᵇ E₂ with a topological vector bundle structure:
bundle.prod.topological_vector_bundle.
A similar construction (which is yet to be formalized) can be done for the vector bundle of
continuous linear maps from E₁ x to E₂ x with fiber a type synonym
vector_bundle_continuous_linear_map R F₁ E₁ F₂ E₂ x := (E₁ x →L[R] E₂ x) (and with the
topology inherited from the norm-topology on F₁ →L[R] F₂, without the need to define the strong
topology on continuous linear maps between general topological vector spaces). Likewise for tensor
products of topological vector bundles, exterior algebras, and so on, where the topology can be
defined using a norm on the fiber model if this helps.
Tags #
Vector bundle
@[protected, instance]
def
topological_vector_bundle.prod.topological_space
{B : Type u_3}
(E₁ : B → Type u_6)
(E₂ : B → Type u_7)
[topological_space (bundle.total_space E₁)]
[topological_space (bundle.total_space E₂)] :
topological_space (bundle.total_space (λ (x : B), E₁ x × E₂ x))
Equip the total space of the fibrewise product of two topological vector bundles E₁, E₂ with
the induced topology from the diagonal embedding into total_space E₁ × total_space E₂.
Equations
- topological_vector_bundle.prod.topological_space E₁ E₂ = topological_space.induced (λ (p : bundle.total_space (λ (x : B), E₁ x × E₂ x)), (⟨p.fst, p.snd.fst⟩, ⟨p.fst, p.snd.snd⟩)) prod.topological_space
theorem
topological_vector_bundle.prod.inducing_diag
{B : Type u_3}
(E₁ : B → Type u_6)
(E₂ : B → Type u_7)
[topological_space (bundle.total_space E₁)]
[topological_space (bundle.total_space E₂)] :
The diagonal map from the total space of the fibrewise product of two topological vector bundles
E₁, E₂ into total_space E₁ × total_space E₂ is inducing.
def
topological_vector_bundle.trivialization.prod.to_fun'
{R : Type u_1}
{B : Type u_3}
[nontrivially_normed_field R]
[topological_space B]
{F₁ : Type u_6}
[normed_add_comm_group F₁]
[normed_space R F₁]
{E₁ : B → Type u_7}
[topological_space (bundle.total_space E₁)]
[Π (x : B), add_comm_monoid (E₁ x)]
[Π (x : B), module R (E₁ x)]
{F₂ : Type u_8}
[normed_add_comm_group F₂]
[normed_space R F₂]
{E₂ : B → Type u_9}
[topological_space (bundle.total_space E₂)]
[Π (x : B), add_comm_monoid (E₂ x)]
[Π (x : B), module R (E₂ x)]
(e₁ : topological_vector_bundle.trivialization R F₁ E₁)
(e₂ : topological_vector_bundle.trivialization R F₂ E₂) :
bundle.total_space (λ (x : B), E₁ x × E₂ x) → B × F₁ × F₂
Given trivializations e₁, e₂ for vector bundles E₁, E₂ over a base B, the forward
function for the construction topological_vector_bundle.trivialization.prod, the induced
trivialization for the direct sum of E₁ and E₂.
theorem
topological_vector_bundle.trivialization.prod.continuous_to_fun
{R : Type u_1}
{B : Type u_3}
[nontrivially_normed_field R]
[topological_space B]
{F₁ : Type u_6}
[normed_add_comm_group F₁]
[normed_space R F₁]
{E₁ : B → Type u_7}
[topological_space (bundle.total_space E₁)]
[Π (x : B), add_comm_monoid (E₁ x)]
[Π (x : B), module R (E₁ x)]
{F₂ : Type u_8}
[normed_add_comm_group F₂]
[normed_space R F₂]
{E₂ : B → Type u_9}
[topological_space (bundle.total_space E₂)]
[Π (x : B), add_comm_monoid (E₂ x)]
[Π (x : B), module R (E₂ x)]
{e₁ : topological_vector_bundle.trivialization R F₁ E₁}
{e₂ : topological_vector_bundle.trivialization R F₂ E₂} :
noncomputable
def
topological_vector_bundle.trivialization.prod.inv_fun'
{R : Type u_1}
{B : Type u_3}
[nontrivially_normed_field R]
[topological_space B]
{F₁ : Type u_6}
[normed_add_comm_group F₁]
[normed_space R F₁]
{E₁ : B → Type u_7}
[topological_space (bundle.total_space E₁)]
[Π (x : B), add_comm_monoid (E₁ x)]
[Π (x : B), module R (E₁ x)]
{F₂ : Type u_8}
[normed_add_comm_group F₂]
[normed_space R F₂]
{E₂ : B → Type u_9}
[topological_space (bundle.total_space E₂)]
[Π (x : B), add_comm_monoid (E₂ x)]
[Π (x : B), module R (E₂ x)]
(e₁ : topological_vector_bundle.trivialization R F₁ E₁)
(e₂ : topological_vector_bundle.trivialization R F₂ E₂)
(p : B × F₁ × F₂) :
bundle.total_space (λ (x : B), E₁ x × E₂ x)
Given trivializations e₁, e₂ for vector bundles E₁, E₂ over a base B, the inverse
function for the construction topological_vector_bundle.trivialization.prod, the induced
trivialization for the direct sum of E₁ and E₂.
theorem
topological_vector_bundle.trivialization.prod.left_inv
{R : Type u_1}
{B : Type u_3}
[nontrivially_normed_field R]
[topological_space B]
{F₁ : Type u_6}
[normed_add_comm_group F₁]
[normed_space R F₁]
{E₁ : B → Type u_7}
[topological_space (bundle.total_space E₁)]
[Π (x : B), add_comm_monoid (E₁ x)]
[Π (x : B), module R (E₁ x)]
{F₂ : Type u_8}
[normed_add_comm_group F₂]
[normed_space R F₂]
{E₂ : B → Type u_9}
[topological_space (bundle.total_space E₂)]
[Π (x : B), add_comm_monoid (E₂ x)]
[Π (x : B), module R (E₂ x)]
{e₁ : topological_vector_bundle.trivialization R F₁ E₁}
{e₂ : topological_vector_bundle.trivialization R F₂ E₂}
{x : bundle.total_space (λ (x : B), E₁ x × E₂ x)}
(h : x ∈ bundle.total_space.proj ⁻¹' (e₁.to_fiber_bundle_trivialization.base_set ∩ e₂.to_fiber_bundle_trivialization.base_set)) :
theorem
topological_vector_bundle.trivialization.prod.right_inv
{R : Type u_1}
{B : Type u_3}
[nontrivially_normed_field R]
[topological_space B]
{F₁ : Type u_6}
[normed_add_comm_group F₁]
[normed_space R F₁]
{E₁ : B → Type u_7}
[topological_space (bundle.total_space E₁)]
[Π (x : B), add_comm_monoid (E₁ x)]
[Π (x : B), module R (E₁ x)]
{F₂ : Type u_8}
[normed_add_comm_group F₂]
[normed_space R F₂]
{E₂ : B → Type u_9}
[topological_space (bundle.total_space E₂)]
[Π (x : B), add_comm_monoid (E₂ x)]
[Π (x : B), module R (E₂ x)]
{e₁ : topological_vector_bundle.trivialization R F₁ E₁}
{e₂ : topological_vector_bundle.trivialization R F₂ E₂}
{x : B × F₁ × F₂}
(h : x ∈ (e₁.to_fiber_bundle_trivialization.base_set ∩ e₂.to_fiber_bundle_trivialization.base_set) ×ˢ set.univ) :
theorem
topological_vector_bundle.trivialization.prod.continuous_inv_fun
{R : Type u_1}
{B : Type u_3}
[nontrivially_normed_field R]
[topological_space B]
{F₁ : Type u_6}
[normed_add_comm_group F₁]
[normed_space R F₁]
{E₁ : B → Type u_7}
[topological_space (bundle.total_space E₁)]
[Π (x : B), add_comm_monoid (E₁ x)]
[Π (x : B), module R (E₁ x)]
{F₂ : Type u_8}
[normed_add_comm_group F₂]
[normed_space R F₂]
{E₂ : B → Type u_9}
[topological_space (bundle.total_space E₂)]
[Π (x : B), add_comm_monoid (E₂ x)]
[Π (x : B), module R (E₂ x)]
{e₁ : topological_vector_bundle.trivialization R F₁ E₁}
{e₂ : topological_vector_bundle.trivialization R F₂ E₂} :
@[nolint]
noncomputable
def
topological_vector_bundle.trivialization.prod
{R : Type u_1}
{B : Type u_3}
[nontrivially_normed_field R]
[topological_space B]
{F₁ : Type u_6}
[normed_add_comm_group F₁]
[normed_space R F₁]
{E₁ : B → Type u_7}
[topological_space (bundle.total_space E₁)]
[Π (x : B), add_comm_monoid (E₁ x)]
[Π (x : B), module R (E₁ x)]
{F₂ : Type u_8}
[normed_add_comm_group F₂]
[normed_space R F₂]
{E₂ : B → Type u_9}
[topological_space (bundle.total_space E₂)]
[Π (x : B), add_comm_monoid (E₂ x)]
[Π (x : B), module R (E₂ x)]
(e₁ : topological_vector_bundle.trivialization R F₁ E₁)
(e₂ : topological_vector_bundle.trivialization R F₂ E₂)
[Π (x : B), topological_space (E₁ x)]
[Π (x : B), topological_space (E₂ x)]
[topological_vector_bundle R F₁ E₁]
[topological_vector_bundle R F₂ E₂] :
topological_vector_bundle.trivialization R (F₁ × F₂) (λ (x : B), E₁ x × E₂ x)
Given trivializations e₁, e₂ for vector bundles E₁, E₂ over a base B, the induced
trivialization for the direct sum of E₁ and E₂, whose base set is e₁.base_set ∩ e₂.base_set.
Equations
- e₁.prod e₂ = {to_fiber_bundle_trivialization := {to_local_homeomorph := {to_local_equiv := {to_fun := topological_vector_bundle.trivialization.prod.to_fun' e₁ e₂, inv_fun := topological_vector_bundle.trivialization.prod.inv_fun' e₁ e₂, source := bundle.total_space.proj ⁻¹' (e₁.to_fiber_bundle_trivialization.base_set ∩ e₂.to_fiber_bundle_trivialization.base_set), target := (e₁.to_fiber_bundle_trivialization.base_set ∩ e₂.to_fiber_bundle_trivialization.base_set) ×ˢ set.univ, map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}, open_source := _, open_target := _, continuous_to_fun := _, continuous_inv_fun := _}, base_set := e₁.to_fiber_bundle_trivialization.base_set ∩ e₂.to_fiber_bundle_trivialization.base_set, open_base_set := _, source_eq := _, target_eq := _, proj_to_fun := _}, linear' := _}
@[simp]
theorem
topological_vector_bundle.trivialization.base_set_prod
{R : Type u_1}
{B : Type u_3}
[nontrivially_normed_field R]
[topological_space B]
{F₁ : Type u_6}
[normed_add_comm_group F₁]
[normed_space R F₁]
{E₁ : B → Type u_7}
[topological_space (bundle.total_space E₁)]
[Π (x : B), add_comm_monoid (E₁ x)]
[Π (x : B), module R (E₁ x)]
{F₂ : Type u_8}
[normed_add_comm_group F₂]
[normed_space R F₂]
{E₂ : B → Type u_9}
[topological_space (bundle.total_space E₂)]
[Π (x : B), add_comm_monoid (E₂ x)]
[Π (x : B), module R (E₂ x)]
(e₁ : topological_vector_bundle.trivialization R F₁ E₁)
(e₂ : topological_vector_bundle.trivialization R F₂ E₂)
[Π (x : B), topological_space (E₁ x)]
[Π (x : B), topological_space (E₂ x)]
[topological_vector_bundle R F₁ E₁]
[topological_vector_bundle R F₂ E₂] :
theorem
topological_vector_bundle.trivialization.prod_apply
{R : Type u_1}
{B : Type u_3}
[nontrivially_normed_field R]
[topological_space B]
{F₁ : Type u_6}
[normed_add_comm_group F₁]
[normed_space R F₁]
{E₁ : B → Type u_7}
[topological_space (bundle.total_space E₁)]
[Π (x : B), add_comm_monoid (E₁ x)]
[Π (x : B), module R (E₁ x)]
{F₂ : Type u_8}
[normed_add_comm_group F₂]
[normed_space R F₂]
{E₂ : B → Type u_9}
[topological_space (bundle.total_space E₂)]
[Π (x : B), add_comm_monoid (E₂ x)]
[Π (x : B), module R (E₂ x)]
{e₁ : topological_vector_bundle.trivialization R F₁ E₁}
{e₂ : topological_vector_bundle.trivialization R F₂ E₂}
[Π (x : B), topological_space (E₁ x)]
[Π (x : B), topological_space (E₂ x)]
[topological_vector_bundle R F₁ E₁]
[topological_vector_bundle R F₂ E₂]
{x : B}
(hx₁ : x ∈ e₁.to_fiber_bundle_trivialization.base_set)
(hx₂ : x ∈ e₂.to_fiber_bundle_trivialization.base_set)
(v₁ : E₁ x)
(v₂ : E₂ x) :
⇑(e₁.prod e₂) ⟨x, (v₁, v₂)⟩ = (x, ⇑(e₁.continuous_linear_equiv_at x hx₁) v₁, ⇑(e₂.continuous_linear_equiv_at x hx₂) v₂)
theorem
topological_vector_bundle.trivialization.prod_symm_apply
{R : Type u_1}
{B : Type u_3}
[nontrivially_normed_field R]
[topological_space B]
{F₁ : Type u_6}
[normed_add_comm_group F₁]
[normed_space R F₁]
{E₁ : B → Type u_7}
[topological_space (bundle.total_space E₁)]
[Π (x : B), add_comm_monoid (E₁ x)]
[Π (x : B), module R (E₁ x)]
{F₂ : Type u_8}
[normed_add_comm_group F₂]
[normed_space R F₂]
{E₂ : B → Type u_9}
[topological_space (bundle.total_space E₂)]
[Π (x : B), add_comm_monoid (E₂ x)]
[Π (x : B), module R (E₂ x)]
{e₁ : topological_vector_bundle.trivialization R F₁ E₁}
{e₂ : topological_vector_bundle.trivialization R F₂ E₂}
[Π (x : B), topological_space (E₁ x)]
[Π (x : B), topological_space (E₂ x)]
[topological_vector_bundle R F₁ E₁]
[topological_vector_bundle R F₂ E₂]
(x : B)
(w₁ : F₁)
(w₂ : F₂) :
⇑((e₁.prod e₂).to_fiber_bundle_trivialization.to_local_homeomorph.to_local_equiv.symm) (x, w₁, w₂) = ⟨x, (e₁.symm x w₁, e₂.symm x w₂)⟩
@[protected, instance]
noncomputable
def
bundle.prod.topological_vector_bundle
(R : Type u_1)
{B : Type u_3}
[nontrivially_normed_field R]
[topological_space B]
(F₁ : Type u_6)
[normed_add_comm_group F₁]
[normed_space R F₁]
(E₁ : B → Type u_7)
[topological_space (bundle.total_space E₁)]
[Π (x : B), add_comm_monoid (E₁ x)]
[Π (x : B), module R (E₁ x)]
(F₂ : Type u_8)
[normed_add_comm_group F₂]
[normed_space R F₂]
(E₂ : B → Type u_9)
[topological_space (bundle.total_space E₂)]
[Π (x : B), add_comm_monoid (E₂ x)]
[Π (x : B), module R (E₂ x)]
[Π (x : B), topological_space (E₁ x)]
[Π (x : B), topological_space (E₂ x)]
[topological_vector_bundle R F₁ E₁]
[topological_vector_bundle R F₂ E₂] :
topological_vector_bundle R (F₁ × F₂) (λ (x : B), E₁ x × E₂ x)
The product of two vector bundles is a vector bundle.
Equations
- bundle.prod.topological_vector_bundle R F₁ E₁ F₂ E₂ = {total_space_mk_inducing := _, trivialization_atlas := (λ (p : topological_vector_bundle.trivialization R F₁ E₁ × topological_vector_bundle.trivialization R F₂ E₂), p.fst.prod p.snd) '' topological_vector_bundle.trivialization_atlas R F₁ E₁ ×ˢ topological_vector_bundle.trivialization_atlas R F₂ E₂, trivialization_at := λ (b : B), (topological_vector_bundle.trivialization_at R F₁ E₁ b).prod (topological_vector_bundle.trivialization_at R F₂ E₂ b), mem_base_set_trivialization_at := _, trivialization_mem_atlas := _, continuous_on_coord_change := _}
@[simp]
theorem
topological_vector_bundle.trivialization.continuous_linear_equiv_at_prod
{R : Type u_1}
{B : Type u_3}
[nontrivially_normed_field R]
[topological_space B]
{F₁ : Type u_6}
[normed_add_comm_group F₁]
[normed_space R F₁]
{E₁ : B → Type u_7}
[topological_space (bundle.total_space E₁)]
[Π (x : B), add_comm_monoid (E₁ x)]
[Π (x : B), module R (E₁ x)]
{F₂ : Type u_8}
[normed_add_comm_group F₂]
[normed_space R F₂]
{E₂ : B → Type u_9}
[topological_space (bundle.total_space E₂)]
[Π (x : B), add_comm_monoid (E₂ x)]
[Π (x : B), module R (E₂ x)]
[Π (x : B), topological_space (E₁ x)]
[Π (x : B), topological_space (E₂ x)]
[topological_vector_bundle R F₁ E₁]
[topological_vector_bundle R F₂ E₂]
{e₁ : topological_vector_bundle.trivialization R F₁ E₁}
{e₂ : topological_vector_bundle.trivialization R F₂ E₂}
{x : B}
(hx₁ : x ∈ e₁.to_fiber_bundle_trivialization.base_set)
(hx₂ : x ∈ e₂.to_fiber_bundle_trivialization.base_set) :
(e₁.prod e₂).continuous_linear_equiv_at x _ = (e₁.continuous_linear_equiv_at x hx₁).prod (e₂.continuous_linear_equiv_at x hx₂)