mathlib3 documentation

topology.vector_bundle.constructions

Standard constructions on vector bundles #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains several standard constructions on vector bundles:

Tags #

Vector bundle, direct sum, pullback

The trivial vector bundle #

@[protected, instance]

Direct sum of two vector bundles #

@[protected, instance]
def trivialization.prod.is_linear (𝕜 : Type u_1) {B : Type u_2} [nontrivially_normed_field 𝕜] [topological_space B] {F₁ : Type u_3} [normed_add_comm_group F₁] [normed_space 𝕜 F₁] {E₁ : B Type u_4} [topological_space (bundle.total_space F₁ E₁)] {F₂ : Type u_5} [normed_add_comm_group F₂] [normed_space 𝕜 F₂] {E₂ : B Type u_6} [topological_space (bundle.total_space F₂ E₂)] [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), module 𝕜 (E₁ x)] [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), module 𝕜 (E₂ x)] (e₁ : trivialization F₁ bundle.total_space.proj) (e₂ : trivialization F₂ bundle.total_space.proj) [trivialization.is_linear 𝕜 e₁] [trivialization.is_linear 𝕜 e₂] :
@[simp]
theorem trivialization.coord_changeL_prod (𝕜 : Type u_1) {B : Type u_2} [nontrivially_normed_field 𝕜] [topological_space B] {F₁ : Type u_3} [normed_add_comm_group F₁] [normed_space 𝕜 F₁] {E₁ : B Type u_4} [topological_space (bundle.total_space F₁ E₁)] {F₂ : Type u_5} [normed_add_comm_group F₂] [normed_space 𝕜 F₂] {E₂ : B Type u_6} [topological_space (bundle.total_space F₂ E₂)] [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), module 𝕜 (E₁ x)] [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), module 𝕜 (E₂ x)] (e₁ e₁' : trivialization F₁ bundle.total_space.proj) (e₂ e₂' : trivialization F₂ bundle.total_space.proj) [trivialization.is_linear 𝕜 e₁] [trivialization.is_linear 𝕜 e₁'] [trivialization.is_linear 𝕜 e₂] [trivialization.is_linear 𝕜 e₂'] ⦃b : B⦄ (hb : b (e₁.prod e₂).base_set (e₁'.prod e₂').base_set) :
(trivialization.coord_changeL 𝕜 (e₁.prod e₂) (e₁'.prod e₂') b) = (trivialization.coord_changeL 𝕜 e₁ e₁' b).prod_map (trivialization.coord_changeL 𝕜 e₂ e₂' b)
theorem trivialization.prod_apply (𝕜 : Type u_1) {B : Type u_2} [nontrivially_normed_field 𝕜] [topological_space B] {F₁ : Type u_3} [normed_add_comm_group F₁] [normed_space 𝕜 F₁] {E₁ : B Type u_4} [topological_space (bundle.total_space F₁ E₁)] {F₂ : Type u_5} [normed_add_comm_group F₂] [normed_space 𝕜 F₂] {E₂ : B Type u_6} [topological_space (bundle.total_space F₂ E₂)] [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), module 𝕜 (E₁ x)] [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), module 𝕜 (E₂ x)] {e₁ : trivialization F₁ bundle.total_space.proj} {e₂ : trivialization F₂ bundle.total_space.proj} [Π (x : B), topological_space (E₁ x)] [Π (x : B), topological_space (E₂ x)] [fiber_bundle F₁ E₁] [fiber_bundle F₂ E₂] [trivialization.is_linear 𝕜 e₁] [trivialization.is_linear 𝕜 e₂] {x : B} (hx₁ : x e₁.base_set) (hx₂ : x e₂.base_set) (v₁ : E₁ x) (v₂ : E₂ x) :
(e₁.prod e₂) {proj := x, snd := (v₁, v₂)} = (x, (trivialization.continuous_linear_equiv_at 𝕜 e₁ x hx₁) v₁, (trivialization.continuous_linear_equiv_at 𝕜 e₂ x hx₂) v₂)
@[protected, instance]
def vector_bundle.prod (𝕜 : Type u_1) {B : Type u_2} [nontrivially_normed_field 𝕜] [topological_space B] (F₁ : Type u_3) [normed_add_comm_group F₁] [normed_space 𝕜 F₁] (E₁ : B Type u_4) [topological_space (bundle.total_space F₁ E₁)] (F₂ : Type u_5) [normed_add_comm_group F₂] [normed_space 𝕜 F₂] (E₂ : B Type u_6) [topological_space (bundle.total_space F₂ E₂)] [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), module 𝕜 (E₁ x)] [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), module 𝕜 (E₂ x)] [Π (x : B), topological_space (E₁ x)] [Π (x : B), topological_space (E₂ x)] [fiber_bundle F₁ E₁] [fiber_bundle F₂ E₂] [vector_bundle 𝕜 F₁ E₁] [vector_bundle 𝕜 F₂ E₂] :
vector_bundle 𝕜 (F₁ × F₂) (λ (x : B), E₁ x × E₂ x)

The product of two vector bundles is a vector bundle.

@[simp]
theorem trivialization.continuous_linear_equiv_at_prod {𝕜 : Type u_1} {B : Type u_2} [nontrivially_normed_field 𝕜] [topological_space B] {F₁ : Type u_3} [normed_add_comm_group F₁] [normed_space 𝕜 F₁] {E₁ : B Type u_4} [topological_space (bundle.total_space F₁ E₁)] {F₂ : Type u_5} [normed_add_comm_group F₂] [normed_space 𝕜 F₂] {E₂ : B Type u_6} [topological_space (bundle.total_space F₂ E₂)] [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), module 𝕜 (E₁ x)] [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), module 𝕜 (E₂ x)] [Π (x : B), topological_space (E₁ x)] [Π (x : B), topological_space (E₂ x)] [fiber_bundle F₁ E₁] [fiber_bundle F₂ E₂] {e₁ : trivialization F₁ bundle.total_space.proj} {e₂ : trivialization F₂ bundle.total_space.proj} [trivialization.is_linear 𝕜 e₁] [trivialization.is_linear 𝕜 e₂] {x : B} (hx₁ : x e₁.base_set) (hx₂ : x e₂.base_set) :

Pullbacks of vector bundles #

@[protected, instance]
def bundle.pullback.add_comm_monoid {B : Type u_3} (E : B Type u_5) {B' : Type u_6} (f : B' B) [Π (x : B), add_comm_monoid (E x)] (x : B') :
Equations
@[protected, instance]
def bundle.pullback.module (R : Type u_1) {B : Type u_3} (E : B Type u_5) {B' : Type u_6} (f : B' B) [semiring R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (x : B') :
module R (f *ᵖ E x)
Equations
@[protected, instance]
def trivialization.pullback_linear (𝕜 : Type u_2) {B : Type u_3} {F : Type u_4} {E : B Type u_5} {B' : Type u_6} [topological_space B'] [topological_space (bundle.total_space F E)] [nontrivially_normed_field 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] [topological_space B] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module 𝕜 (E x)] {K : Type u_7} [continuous_map_class K B' B] (e : trivialization F bundle.total_space.proj) [trivialization.is_linear 𝕜 e] (f : K) :
@[protected, instance]
def vector_bundle.pullback (𝕜 : Type u_2) {B : Type u_3} {F : Type u_4} {E : B Type u_5} {B' : Type u_6} [topological_space B'] [topological_space (bundle.total_space F E)] [nontrivially_normed_field 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] [topological_space B] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module 𝕜 (E x)] {K : Type u_7} [continuous_map_class K B' B] [Π (x : B), topological_space (E x)] [fiber_bundle F E] [vector_bundle 𝕜 F E] (f : K) :