mathlib documentation

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 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
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₂)] :
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} [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₂.

Equations
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₂.

Equations
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
@[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
@[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) :