# mathlibdocumentation

topology.vector_bundle.prod

# 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 (λ (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
theorem topological_vector_bundle.prod.inducing_diag {B : Type u_3} (E₁ : B → Type u_6) (E₂ : B → Type u_7)  :
inducing (λ (p : bundle.total_space (λ (x : B), E₁ x × E₂ x)), (p.fst, p.snd.fst, p.fst, p.snd.snd⟩))

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} {F₁ : Type u_6} [ F₁] {E₁ : B → Type u_7} [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), (E₁ x)] {F₂ : Type u_8} [ F₂] {E₂ : B → Type u_9} [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), (E₂ x)] (e₁ : E₁) (e₂ : 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₂.

Equations
theorem topological_vector_bundle.trivialization.prod.continuous_to_fun {R : Type u_1} {B : Type u_3} {F₁ : Type u_6} [ F₁] {E₁ : B → Type u_7} [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), (E₁ x)] {F₂ : Type u_8} [ F₂] {E₂ : B → Type u_9} [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), (E₂ x)] {e₁ : E₁} {e₂ : E₂} :
noncomputable def topological_vector_bundle.trivialization.prod.inv_fun' {R : Type u_1} {B : Type u_3} {F₁ : Type u_6} [ F₁] {E₁ : B → Type u_7} [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), (E₁ x)] {F₂ : Type u_8} [ F₂] {E₂ : B → Type u_9} [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), (E₂ x)] (e₁ : E₁) (e₂ : 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₂.

Equations
theorem topological_vector_bundle.trivialization.prod.left_inv {R : Type u_1} {B : Type u_3} {F₁ : Type u_6} [ F₁] {E₁ : B → Type u_7} [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), (E₁ x)] {F₂ : Type u_8} [ F₂] {E₂ : B → Type u_9} [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), (E₂ x)] {e₁ : E₁} {e₂ : E₂} {x : bundle.total_space (λ (x : B), E₁ x × E₂ x)}  :
theorem topological_vector_bundle.trivialization.prod.right_inv {R : Type u_1} {B : Type u_3} {F₁ : Type u_6} [ F₁] {E₁ : B → Type u_7} [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), (E₁ x)] {F₂ : Type u_8} [ F₂] {E₂ : B → Type u_9} [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), (E₂ x)] {e₁ : E₁} {e₂ : E₂} {x : B × F₁ × F₂}  :
theorem topological_vector_bundle.trivialization.prod.continuous_inv_fun {R : Type u_1} {B : Type u_3} {F₁ : Type u_6} [ F₁] {E₁ : B → Type u_7} [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), (E₁ x)] {F₂ : Type u_8} [ F₂] {E₂ : B → Type u_9} [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), (E₂ x)] {e₁ : E₁} {e₂ : E₂} :
@[nolint]
noncomputable def topological_vector_bundle.trivialization.prod {R : Type u_1} {B : Type u_3} {F₁ : Type u_6} [ F₁] {E₁ : B → Type u_7} [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), (E₁ x)] {F₂ : Type u_8} [ F₂] {E₂ : B → Type u_9} [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), (E₂ x)] (e₁ : E₁) (e₂ : E₂) [Π (x : B), topological_space (E₁ x)] [Π (x : B), topological_space (E₂ x)] [ E₁] [ E₂] :
(λ (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
@[simp]
theorem topological_vector_bundle.trivialization.base_set_prod {R : Type u_1} {B : Type u_3} {F₁ : Type u_6} [ F₁] {E₁ : B → Type u_7} [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), (E₁ x)] {F₂ : Type u_8} [ F₂] {E₂ : B → Type u_9} [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), (E₂ x)] (e₁ : E₁) (e₂ : E₂) [Π (x : B), topological_space (E₁ x)] [Π (x : B), topological_space (E₂ x)] [ E₁] [ E₂] :
theorem topological_vector_bundle.trivialization.prod_apply {R : Type u_1} {B : Type u_3} {F₁ : Type u_6} [ F₁] {E₁ : B → Type u_7} [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), (E₁ x)] {F₂ : Type u_8} [ F₂] {E₂ : B → Type u_9} [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), (E₂ x)] {e₁ : E₁} {e₂ : E₂} [Π (x : B), topological_space (E₁ x)] [Π (x : B), topological_space (E₂ x)] [ E₁] [ 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, hx₁) v₁, hx₂) v₂)
theorem topological_vector_bundle.trivialization.prod_symm_apply {R : Type u_1} {B : Type u_3} {F₁ : Type u_6} [ F₁] {E₁ : B → Type u_7} [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), (E₁ x)] {F₂ : Type u_8} [ F₂] {E₂ : B → Type u_9} [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), (E₂ x)] {e₁ : E₁} {e₂ : E₂} [Π (x : B), topological_space (E₁ x)] [Π (x : B), topological_space (E₂ x)] [ E₁] [ E₂] (x : B) (w₁ : F₁) (w₂ : F₂) :
(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} (F₁ : Type u_6) [ F₁] (E₁ : B → Type u_7) [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), (E₁ x)] (F₂ : Type u_8) [ F₂] (E₂ : B → Type u_9) [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), (E₂ x)] [Π (x : B), topological_space (E₁ x)] [Π (x : B), topological_space (E₂ x)] [ E₁] [ E₂] :
(F₁ × F₂) (λ (x : B), E₁ x × E₂ x)

The product of two vector bundles is a vector bundle.

Equations
@[simp]
theorem topological_vector_bundle.trivialization.continuous_linear_equiv_at_prod {R : Type u_1} {B : Type u_3} {F₁ : Type u_6} [ F₁] {E₁ : B → Type u_7} [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), (E₁ x)] {F₂ : Type u_8} [ F₂] {E₂ : B → Type u_9} [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), (E₂ x)] [Π (x : B), topological_space (E₁ x)] [Π (x : B), topological_space (E₂ x)] [ E₁] [ E₂] {e₁ : E₁} {e₂ : 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 _ = hx₁).prod hx₂)