Standard constructions on vector bundles

This file contains several standard constructions on vector bundles:

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

• VectorBundle.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 fun x ↦ E₁ x × E₂ x).

• VectorBundle.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

instance Bundle.Trivial.trivialization.isLinear (𝕜 : Type u_1) (B : Type u_2) (F : Type u_3) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] : Trivialization.IsLinear 𝕜 (Bundle.Trivial.trivialization B F)

Equations

• (_ : Trivialization.IsLinear 𝕜 (Bundle.Trivial.trivialization B F)) = (_ : Trivialization.IsLinear 𝕜 (Bundle.Trivial.trivialization B F))

theorem Bundle.Trivial.trivialization.coordChangeL {𝕜 : Type u_1} (B : Type u_2) (F : Type u_3) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] (b : B) : Trivialization.coordChangeL 𝕜 (Bundle.Trivial.trivialization B F) (Bundle.Trivial.trivialization B F) b = ContinuousLinearEquiv.refl 𝕜 F

instance Bundle.Trivial.vectorBundle (𝕜 : Type u_1) (B : Type u_2) (F : Type u_3) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] : VectorBundle 𝕜 F (Bundle.Trivial B F)

Equations

• (_ : VectorBundle 𝕜 F (Bundle.Trivial B F)) = (_ : VectorBundle 𝕜 F (Bundle.Trivial B F))

Direct sum of two vector bundles

instance Trivialization.prod.isLinear (𝕜 : Type u_1) {B : Type u_2} [NontriviallyNormedField 𝕜] [TopologicalSpace B] {F₁ : Type u_3} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {E₁ : B → Type u_4} [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_5} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {E₂ : B → Type u_6} [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → AddCommMonoid (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [(x : B) → AddCommMonoid (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] (e₁ : Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Trivialization F₂ Bundle.TotalSpace.proj) [Trivialization.IsLinear 𝕜 e₁] [Trivialization.IsLinear 𝕜 e₂] : Trivialization.IsLinear 𝕜 (Trivialization.prod e₁ e₂)

Equations

• (_ : Trivialization.IsLinear 𝕜 (Trivialization.prod e₁ e₂)) = (_ : Trivialization.IsLinear 𝕜 (Trivialization.prod e₁ e₂))

@[simp]

theorem Trivialization.coordChangeL_prod (𝕜 : Type u_1) {B : Type u_2} [NontriviallyNormedField 𝕜] [TopologicalSpace B] {F₁ : Type u_3} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {E₁ : B → Type u_4} [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_5} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {E₂ : B → Type u_6} [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → AddCommMonoid (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [(x : B) → AddCommMonoid (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] (e₁ : Trivialization F₁ Bundle.TotalSpace.proj) (e₁' : Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Trivialization F₂ Bundle.TotalSpace.proj) (e₂' : Trivialization F₂ Bundle.TotalSpace.proj) [Trivialization.IsLinear 𝕜 e₁] [Trivialization.IsLinear 𝕜 e₁'] [Trivialization.IsLinear 𝕜 e₂] [Trivialization.IsLinear 𝕜 e₂'] ⦃b : B⦄ (hb : b ∈ (Trivialization.prod e₁ e₂).baseSet ∩ (Trivialization.prod e₁' e₂').baseSet) : ↑(Trivialization.coordChangeL 𝕜 (Trivialization.prod e₁ e₂) (Trivialization.prod e₁' e₂') b) = ContinuousLinearMap.prodMap ↑(Trivialization.coordChangeL 𝕜 e₁ e₁' b) ↑(Trivialization.coordChangeL 𝕜 e₂ e₂' b)

theorem Trivialization.prod_apply (𝕜 : Type u_1) {B : Type u_2} [NontriviallyNormedField 𝕜] [TopologicalSpace B] {F₁ : Type u_3} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {E₁ : B → Type u_4} [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_5} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {E₂ : B → Type u_6} [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → AddCommMonoid (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [(x : B) → AddCommMonoid (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] {e₁ : Trivialization F₁ Bundle.TotalSpace.proj} {e₂ : Trivialization F₂ Bundle.TotalSpace.proj} [(x : B) → TopologicalSpace (E₁ x)] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₁ E₁] [FiberBundle F₂ E₂] [Trivialization.IsLinear 𝕜 e₁] [Trivialization.IsLinear 𝕜 e₂] {x : B} (hx₁ : x ∈ e₁.baseSet) (hx₂ : x ∈ e₂.baseSet) (v₁ : E₁ x) (v₂ : E₂ x) : ↑(Trivialization.prod e₁ e₂) { proj := x, snd := (v₁, v₂) } = (x, (Trivialization.continuousLinearEquivAt 𝕜 e₁ x hx₁) v₁, (Trivialization.continuousLinearEquivAt 𝕜 e₂ x hx₂) v₂)

instance VectorBundle.prod (𝕜 : Type u_1) {B : Type u_2} [NontriviallyNormedField 𝕜] [TopologicalSpace B] (F₁ : Type u_3) [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] (E₁ : B → Type u_4) [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] (F₂ : Type u_5) [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] (E₂ : B → Type u_6) [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → AddCommMonoid (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [(x : B) → AddCommMonoid (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [(x : B) → TopologicalSpace (E₁ x)] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₁ E₁] [VectorBundle 𝕜 F₂ E₂] : VectorBundle 𝕜 (F₁ × F₂) fun (x : B) => E₁ x × E₂ x

The product of two vector bundles is a vector bundle.

Equations

• (_ : VectorBundle 𝕜 (F₁ × F₂) fun (x : B) => E₁ x × E₂ x) = (_ : VectorBundle 𝕜 (F₁ × F₂) fun (x : B) => E₁ x × E₂ x)

@[simp]

theorem Trivialization.continuousLinearEquivAt_prod {𝕜 : Type u_1} {B : Type u_2} [NontriviallyNormedField 𝕜] [TopologicalSpace B] {F₁ : Type u_3} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {E₁ : B → Type u_4} [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_5} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {E₂ : B → Type u_6} [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → AddCommMonoid (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [(x : B) → AddCommMonoid (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [(x : B) → TopologicalSpace (E₁ x)] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₁ E₁] [FiberBundle F₂ E₂] {e₁ : Trivialization F₁ Bundle.TotalSpace.proj} {e₂ : Trivialization F₂ Bundle.TotalSpace.proj} [Trivialization.IsLinear 𝕜 e₁] [Trivialization.IsLinear 𝕜 e₂] {x : B} (hx : x ∈ (Trivialization.prod e₁ e₂).baseSet) : Trivialization.continuousLinearEquivAt 𝕜 (Trivialization.prod e₁ e₂) x hx = ContinuousLinearEquiv.prod (Trivialization.continuousLinearEquivAt 𝕜 e₁ x (_ : x ∈ e₁.baseSet)) (Trivialization.continuousLinearEquivAt 𝕜 e₂ x (_ : x ∈ e₂.baseSet))

Pullbacks of vector bundles

instance instAddCommMonoidPullback {B : Type u_3} (E : B → Type u_5) {B' : Type u_6} (f : B' → B) [i : (x : B) → AddCommMonoid (E x)] (x : B') : AddCommMonoid ((f *ᵖ E) x)

Equations

• instAddCommMonoidPullback E f x = i (f x)

instance instModulePullbackInstAddCommMonoidPullback (R : Type u_1) {B : Type u_3} (E : B → Type u_5) {B' : Type u_6} (f : B' → B) [Semiring R] [(x : B) → AddCommMonoid (E x)] [i : (x : B) → Module R (E x)] (x : B') : Module R ((f *ᵖ E) x)

Equations

• instModulePullbackInstAddCommMonoidPullback R E f x = i (f x)

instance Trivialization.pullback_linear (𝕜 : Type u_2) {B : Type u_3} {F : Type u_4} {E : B → Type u_5} {B' : Type u_6} [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {K : Type u_7} [FunLike K B' B] [ContinuousMapClass K B' B] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear 𝕜 e] (f : K) : Trivialization.IsLinear 𝕜 (Trivialization.pullback e f)

Equations

• (_ : Trivialization.IsLinear 𝕜 (Trivialization.pullback e f)) = (_ : Trivialization.IsLinear 𝕜 (Trivialization.pullback e f))

instance VectorBundle.pullback (𝕜 : Type u_2) {B : Type u_3} {F : Type u_4} {E : B → Type u_5} {B' : Type u_6} [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {K : Type u_7} [FunLike K B' B] [ContinuousMapClass K B' B] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] (f : K) : VectorBundle 𝕜 F (⇑f *ᵖ E)

Equations

• (_ : VectorBundle 𝕜 F (⇑f *ᵖ E)) = (_ : VectorBundle 𝕜 F (⇑f *ᵖ E))