Various operations on and properties of smooth vector bundles

theorem FiberBundle.chartedSpace_chartAt_fst' {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {HB : Type u_7} [TopologicalSpace HB] [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] (x y : Bundle.TotalSpace F E) : (↑(chartAt (ModelProd HB F) x) y).1 = ↑(chartAt HB x.proj) (↑(trivializationAt F E x.proj) y).1

theorem FiberBundle.chartedSpace_chartAt_fst {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {HB : Type u_7} [TopologicalSpace HB] [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] {x y : Bundle.TotalSpace F E} (hy : y.proj ∈ (trivializationAt F E x.proj).baseSet) : (↑(chartAt (ModelProd HB F) x) y).1 = ↑(chartAt HB x.proj) y.proj

theorem FiberBundle.chartedSpace_chartAt_snd {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {HB : Type u_7} [TopologicalSpace HB] [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] (x y : Bundle.TotalSpace F E) : (↑(chartAt (ModelProd HB F) x) y).2 = (↑(trivializationAt F E x.proj) y).2

theorem VectorBundleCore.coordChange_comp_eq_self {R : Type u_1} {B : Type u_3} {F : Type u_4} {ι : Type u_5} [NontriviallyNormedField R] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] (Z : VectorBundleCore R B F ι) {i j : ι} {x : B} (hx : x ∈ Z.baseSet i ∩ Z.baseSet j) (v : F) : (Z.coordChange j i x) ((Z.coordChange i j x) v) = v

Z.coord_change j i is a partial inverse of Z.coord_change i j.

@[simp]

theorem Bundle.Trivial.trivializationAt {B : Type u_2} {F : Type u_3} [NormedAddCommGroup F] [TopologicalSpace B] (x : B) : trivializationAt F (Trivial B F) x = trivialization B F

@[simp]

theorem Bundle.Trivial.trivialization_continuousLinearMapAt {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] (x : B) : Trivialization.continuousLinearMapAt 𝕜 (trivialization B F) x = ContinuousLinearMap.id 𝕜 F

@[simp]

theorem continuousLinearMap_trivializationAt {𝕜₁ : Type u_1} [NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [NontriviallyNormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} [TopologicalSpace B] (F₁ : Type u_4) [NormedAddCommGroup F₁] [NormedSpace 𝕜₁ F₁] (E₁ : B → Type u_5) [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] (F₂ : Type u_6) [NormedAddCommGroup F₂] [NormedSpace 𝕜₂ F₂] (E₂ : B → Type u_7) [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [RingHomIsometric σ] [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [VectorBundle 𝕜₁ F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [VectorBundle 𝕜₂ F₂ E₂] [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] (x : B) : trivializationAt (F₁ →SL[σ] F₂) (Bundle.ContinuousLinearMap σ E₁ E₂) x = Trivialization.continuousLinearMap σ (trivializationAt F₁ E₁ x) (trivializationAt F₂ E₂ x)

instance instAddCommGroupPullback_sphereEversion {B : Type u_2} {B' : Type u_3} {E : B → Type u_1} {f : B' → B} {x : B'} [(x' : B) → AddCommGroup (E x')] : AddCommGroup ((f *ᵖ E) x)

We need some instances like this to work with negation on pullbacks

Equations

• instAddCommGroupPullback_sphereEversion = id inferInstance

instance instZeroPullback_sphereEversion {B : Type u_2} {B' : Type u_3} {E : B → Type u_1} {f : B' → B} {x : B'} [(x' : B) → Zero (E x')] : Zero ((f *ᵖ E) x)

Equations

• instZeroPullback_sphereEversion = id inferInstance

theorem Trivialization.pullback_symm {B : Type u_1} {F : Type u_2} {B' : Type u_3} {K : Type u_4} {E : B → Type u_5} {f : K} [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] [TopologicalSpace F] [TopologicalSpace B] [(b : B) → Zero (E b)] [FunLike K B' B] [ContinuousMapClass K B' B] (e : Trivialization F Bundle.TotalSpace.proj) (x : B') : (e.pullback f).symm x = e.symm (f x)

theorem pullback_trivializationAt {B : Type u_1} {F : Type u_2} {B' : Type u_3} {K : Type u_4} {E : B → Type u_5} {f : K} [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] [TopologicalSpace F] [TopologicalSpace B] [(b : B) → Zero (E b)] [FunLike K B' B] [ContinuousMapClass K B' B] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] {x : B'} : trivializationAt F (⇑f *ᵖ E) x = (trivializationAt F E (f x)).pullback f

theorem Trivialization.pullback_symmL {𝕜 : Type u_2} {B : Type u_3} {F : Type u_4} {B' : Type u_5} {E : 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)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] {K : Type u_7} [FunLike K B' B] [ContinuousMapClass K B' B] (f : K) (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear 𝕜 e] (x : B') : symmL 𝕜 (e.pullback f) x = symmL 𝕜 e (f x)