Smooth vector and fiber bundles

• (topological) fiber bundle

Class(smooth) vector bundle#

When B is a manifold with respect to a model IB and E is a topological vector bundle over B with fibers isomorphic to F, then ContMDiffVectorBundle n F E IB registers that the bundle is C^n, in the sense of having C^n transition functions. This is a mixin, not carrying any new data.

ContMDiffVectorBundle.{u_1, u_2, u_3, u_5, u_6, u_7} (n : WithTop ℕ∞) {𝕜 : Type u_1} {B : Type u_2}
  (F : Type u_3) (E : B → Type u_5) [NontriviallyNormedField 𝕜] {EB : Type u_6}
  [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_7} [TopologicalSpace HB]
  (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B]
  [(x : B) → AddCommMonoid (E x)] [(x : B) → _root_.Module 𝕜 (E x)] [NormedAddCommGroup F]
  [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)]
  [FiberBundle F E] [VectorBundle 𝕜 F E] : Prop

Sources

• Mathlib documentation: ContMDiffVectorBundle
• Source of ContMDiffVectorBundle in Mathlib/Geometry/Manifold/VectorBundle/Basic.lean
• Mathlib overview: Geometry › Smooth vector and fiber bundles

MathlibContMDiffVectorBundle

Uses 7 · Used by 4

Statement usesAssociative algebra over a commutative ring · Completeness · Convex subsets · Infinite sum · Norm of a continuous linear map · Radius of convergence · Topological vector bundle

Used by(smooth) direct sum of vector bundles · (smooth) Hom bundle · (smooth) pullback vector bundle · (smooth) trivial vector bundle

Theorem(smooth) trivial vector bundle#

A trivial vector bundle over a manifold is a C^n vector bundle.

Bundle.Trivial.contMDiffVectorBundle.{u_1, u_2, u_3, u_6, u_7} {n : WithTop ℕ∞} {𝕜 : Type u_1}
  {B : Type u_2} (F : Type u_3) [NontriviallyNormedField 𝕜] {EB : Type u_6} [NormedAddCommGroup EB]
  [NormedSpace 𝕜 EB] {HB : Type u_7} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [TopologicalSpace B] [ChartedSpace HB B] [NormedAddCommGroup F] [NormedSpace 𝕜 F] :
  ContMDiffVectorBundle n F (Bundle.Trivial B F) IB

Sources

• Mathlib documentation: Bundle.Trivial.contMDiffVectorBundle
• Source of Bundle.Trivial.contMDiffVectorBundle in Mathlib/Geometry/Manifold/VectorBundle/Basic.lean
• Mathlib overview: Geometry › Smooth vector and fiber bundles

MathlibBundle.Trivial.contMDiffVectorBundle

Uses 3

Statement uses(smooth) vector bundle

Proof usesHomeomorphisms · Smooth map between manifolds

Theorem(smooth) direct sum of vector bundles#

The direct sum of two C^n vector bundles over the same base is a C^n vector bundle.

Bundle.Prod.contMDiffVectorBundle.{u_1, u_2, u_6, u_7, u_10, u_11, u_12, u_13} {n : WithTop ℕ∞}
  {𝕜 : Type u_1} {B : Type u_2} [NontriviallyNormedField 𝕜] {EB : Type u_6} [NormedAddCommGroup EB]
  [NormedSpace 𝕜 EB] {HB : Type u_7} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [TopologicalSpace B] [ChartedSpace HB B] (F₁ : Type u_10) [NormedAddCommGroup F₁]
  [NormedSpace 𝕜 F₁] (E₁ : B → Type u_11) [TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
  [(x : B) → AddCommMonoid (E₁ x)] [(x : B) → _root_.Module 𝕜 (E₁ x)] (F₂ : Type u_12)
  [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] (E₂ : B → Type u_13)
  [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → AddCommMonoid (E₂ x)]
  [(x : B) → _root_.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₂] [ContMDiffVectorBundle n F₁ E₁ IB] [ContMDiffVectorBundle n F₂ E₂ IB] :
  ContMDiffVectorBundle n (F₁ × F₂) (fun x => E₁ x × E₂ x) IB

Sources

• Mathlib documentation: Bundle.Prod.contMDiffVectorBundle
• Source of Bundle.Prod.contMDiffVectorBundle in Mathlib/Geometry/Manifold/VectorBundle/Basic.lean
• Mathlib overview: Geometry › Smooth vector and fiber bundles

MathlibBundle.Prod.contMDiffVectorBundle

Uses 2

Statement uses(smooth) vector bundle · Product of vector spaces

Theorem(smooth) pullback vector bundle#

For a C^n vector bundle E over a manifold B and a C^n map f : B' → B, the pullback vector bundle f *ᵖ E is a C^n vector bundle.

ContMDiffVectorBundle.pullback.{u_1, u_2, u_3, u_4, u_5, u_6, u_7, u_8, u_9} {𝕜 : Type u_1}
  {B : Type u_2} {B' : Type u_3} (F : Type u_4) (E : B → Type u_5) {n : WithTop ℕ∞}
  [NontriviallyNormedField 𝕜] [(x : B) → AddCommMonoid (E x)] [(x : B) → _root_.Module 𝕜 (E x)]
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)]
  [(x : B) → TopologicalSpace (E x)] {EB : Type u_6} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB]
  {HB : Type u_7} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B]
  [ChartedSpace HB B] {EB' : Type u_8} [NormedAddCommGroup EB'] [NormedSpace 𝕜 EB'] {HB' : Type u_9}
  [TopologicalSpace HB'] (IB' : ModelWithCorners 𝕜 EB' HB') [TopologicalSpace B']
  [ChartedSpace HB' B'] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB]
  (f : ContMDiffMap IB' IB B' B n) : ContMDiffVectorBundle n F (⇑f *ᵖ E) IB'

Sources

• Mathlib documentation: ContMDiffVectorBundle.pullback
• Source of ContMDiffVectorBundle.pullback in Mathlib/Geometry/Manifold/VectorBundle/Pullback.lean
• Mathlib overview: Geometry › Smooth vector and fiber bundles

MathlibContMDiffVectorBundle.pullback

Uses 2

Statement uses(smooth) vector bundle · Smooth map between manifolds

Theorem(smooth) Hom bundle#

Mathlib states this as ContMDiffVectorBundle.continuousLinearMap.

ContMDiffVectorBundle.continuousLinearMap.{u_1, u_2, u_3, u_4, u_6, u_7, u_8, u_9} {𝕜 : Type u_1}
  {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {n : WithTop ℕ∞} {E₁ : B → Type u_6}
  {E₂ : B → Type u_7} [NontriviallyNormedField 𝕜] [(x : B) → AddCommGroup (E₁ x)]
  [(x : B) → _root_.Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁]
  [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B) → TopologicalSpace (E₁ x)]
  [(x : B) → AddCommGroup (E₂ x)] [(x : B) → _root_.Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂]
  [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [(x : B) → TopologicalSpace (E₂ x)] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB]
  {HB : Type u_9} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B]
  [ChartedSpace HB B] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂]
  [VectorBundle 𝕜 F₂ E₂] [∀ (x : B), IsTopologicalAddGroup (E₂ x)]
  [∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] [ContMDiffVectorBundle n F₁ E₁ IB]
  [ContMDiffVectorBundle n F₂ E₂ IB] :
  ContMDiffVectorBundle n (F₁ →L[𝕜] F₂) (fun b => E₁ b →L[𝕜] E₂ b) IB

Sources

• Mathlib documentation: ContMDiffVectorBundle.continuousLinearMap
• Source of ContMDiffVectorBundle.continuousLinearMap in Mathlib/Geometry/Manifold/VectorBundle/Hom.lean
• Mathlib overview: Geometry › Smooth vector and fiber bundles

MathlibContMDiffVectorBundle.continuousLinearMap

Uses 2

Statement uses(smooth) vector bundle · Topological module

StructureCovariant derivatives#

Bundled global covariant derivative on a vector bundle. Caution, the argument order is nonstandard: cov σ x (X x) corresponds to ∇_X σ x on paper.

CovariantDerivative.{u_1, u_2, u_3, u_4, u_5, u_6} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (F : Type u_5)
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] (V : M → Type u_6)
  [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)]
  [(x : M) → _root_.Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)]
  [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul 𝕜 (V x)] [FiberBundle F V] :
  Type (max (max u_2 u_4) u_6)

Sources

• Mathlib documentation: CovariantDerivative
• Source of CovariantDerivative in Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Basic.lean
• Mathlib overview: Geometry › Smooth vector and fiber bundles

MathlibCovariantDerivative

Uses 7

Statement usesAssociative algebra over a commutative ring · Completeness · Continuous linear map · Convex subsets · Normed vector space over a normed field · Topological fiber bundle · Topological module

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.