mathlib3documentation

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:

• bundle.trivial.vector_bundle 𝕜 B F: the trivial vector bundle with scalar field 𝕜 and model fiber F over the base B

• vector_bundle.prod: for vector bundles E₁ and E₂ with scalar field 𝕜 over a common base, a vector bundle structure on their direct sum E₁ ×ᵇ E₂ (the notation stands for λ x, E₁ x × E₂ x).

• vector_bundle.pullback: for a vector bundle E over B, a vector bundle structure on its pullback f *ᵖ E by a map f : B' → B (the notation is a type synonym for E ∘ f).

Tags #

Vector bundle, direct sum, pullback

The trivial vector bundle #

@[protected, instance]
def bundle.trivial.trivialization.is_linear (𝕜 : Type u_1) (B : Type u_2) (F : Type u_3) [ F]  :
theorem bundle.trivial.trivialization.coord_changeL {𝕜 : Type u_1} (B : Type u_2) (F : Type u_3) [ F] (b : B) :
@[protected, instance]
def bundle.trivial.vector_bundle (𝕜 : Type u_1) (B : Type u_2) (F : Type u_3) [ F]  :
F)

Direct sum of two vector bundles #

@[protected, instance]
def trivialization.prod.is_linear (𝕜 : Type u_1) {B : Type u_2} {F₁ : Type u_3} [ F₁] {E₁ : B Type u_4} [topological_space E₁)] {F₂ : Type u_5} [ F₂] {E₂ : B Type u_6} [topological_space E₂)] [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), (E₁ x)] [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), (E₂ x)] [ e₁] [ e₂] :
(e₁.prod e₂)
@[simp]
theorem trivialization.coord_changeL_prod (𝕜 : Type u_1) {B : Type u_2} {F₁ : Type u_3} [ F₁] {E₁ : B Type u_4} [topological_space E₁)] {F₂ : Type u_5} [ F₂] {E₂ : B Type u_6} [topological_space E₂)] [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), (E₁ x)] [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), (E₂ x)] (e₁ e₁' : bundle.total_space.proj) (e₂ e₂' : bundle.total_space.proj) [ e₁] [ e₁'] [ e₂] [ e₂'] ⦃b : B⦄ (hb : b (e₁.prod e₂).base_set (e₁'.prod e₂').base_set) :
(e₁.prod e₂) (e₁'.prod e₂') b) = e₁' b).prod_map e₂' b)
theorem trivialization.prod_apply (𝕜 : Type u_1) {B : Type u_2} {F₁ : Type u_3} [ F₁] {E₁ : B Type u_4} [topological_space E₁)] {F₂ : Type u_5} [ F₂] {E₂ : B Type u_6} [topological_space E₂)] [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), (E₁ x)] [Π (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₂] {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, hx₁) v₁, hx₂) v₂)
@[protected, instance]
def vector_bundle.prod (𝕜 : Type u_1) {B : Type u_2} (F₁ : Type u_3) [ F₁] (E₁ : B Type u_4) [topological_space E₁)] (F₂ : Type u_5) [ F₂] (E₂ : B Type u_6) [topological_space E₂)] [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), (E₁ x)] [Π (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₁ E₁] [ F₂ E₂] :
(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} {F₁ : Type u_3} [ F₁] {E₁ : B Type u_4} [topological_space E₁)] {F₂ : Type u_5} [ F₂] {E₂ : B Type u_6} [topological_space E₂)] [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), (E₁ x)] [Π (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₂] {x : B} (hx₁ : x e₁.base_set) (hx₂ : x e₂.base_set) :
x _ = hx₁).prod hx₂)

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
• = λ (x : B'), _inst_1 (f x)
@[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), (E x)] (x : B') :
(f *ᵖ E x)
Equations
• = λ (x : B'), _inst_3 (f x)
@[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} [ F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), (E x)] {K : Type u_7} [ B] (f : K) :
(e.pullback f)
@[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} [ F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), (E x)] {K : Type u_7} [ B] [Π (x : B), topological_space (E x)] [ E] [ E] (f : K) :
f *ᵖ E