Documentation

Mathlib.Topology.VectorBundle.Constructions

Standard constructions on vector bundles #

This file contains several standard constructions on vector bundles:

Tags #

Vector bundle, direct sum, pullback

The trivial vector bundle #

Equations
  • โ‹ฏ = โ‹ฏ
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
  • โ‹ฏ = โ‹ฏ

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 ๐•œ (eโ‚.prod eโ‚‚)
Equations
  • โ‹ฏ = โ‹ฏ
@[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 โˆˆ (eโ‚.prod eโ‚‚).baseSet โˆฉ (eโ‚'.prod eโ‚‚').baseSet) :
โ†‘(Trivialization.coordChangeL ๐•œ (eโ‚.prod eโ‚‚) (eโ‚'.prod eโ‚‚') b) = (โ†‘(Trivialization.coordChangeL ๐•œ eโ‚ eโ‚' b)).prodMap โ†‘(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) :
โ†‘(eโ‚.prod 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
  • โ‹ฏ = โ‹ฏ
@[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 โˆˆ (eโ‚.prod eโ‚‚).baseSet) :
Trivialization.continuousLinearEquivAt ๐•œ (eโ‚.prod eโ‚‚) x hx = (Trivialization.continuousLinearEquivAt ๐•œ eโ‚ x โ‹ฏ).prod (Trivialization.continuousLinearEquivAt ๐•œ eโ‚‚ x โ‹ฏ)

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') :
Equations
instance instModulePullback (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
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 ๐•œ (e.pullback f)
Equations
  • โ‹ฏ = โ‹ฏ
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
  • โ‹ฏ = โ‹ฏ