Theorems · Theorem · algebraic topology

Bundle.Trivialization.contMDiffAt_symmL

∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {EB : Type u_4}
  [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_5} [inst_3 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B] [inst_5 : ChartedSpace HB B] {E₁ : B → Type u_6}
  [inst_6 : (x : B) → AddCommGroup (E₁ x)] [inst_7 : (x : B) → Module 𝕜 (E₁ x)] [inst_8 : NormedAddCommGroup F₁]
  [inst_9 : NormedSpace 𝕜 F₁] [inst_10 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
  [inst_11 : (x : B) → TopologicalSpace (E₁ x)] [inst_12 : ∀ (x : B), IsTopologicalAddGroup (E₁ x)]
  [inst_13 : ∀ (x : B), ContinuousSMul 𝕜 (E₁ x)] [inst_14 : FiberBundle F₁ E₁] [inst_15 : VectorBundle 𝕜 F₁ E₁]
  [ContMDiffVectorBundle n F₁ E₁ IB] (e : Bundle.Trivialization F₁ Bundle.TotalSpace.proj)
  [inst_17 : MemTrivializationAtlas e] {x : B},
  x ∈ e.baseSet →
    ContMDiffAt IB (IB.prod (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₁))) n (fun m => ⟨m, Bundle.Trivialization.symmL 𝕜 e m⟩)
      x

Let e be a trivialization of a C^n vector bundle E₁ over B. Then m ↦ e.symmL 𝕜 m defines a section of the bundle of continuous linear maps F₁ →L[𝕜] E₁ over B, and this section is C^n at any point in e.baseSet.

Defined in

Mathlib.Geometry.Manifold.VectorBundle.Hom

Cited by

1 results in Mathlib

Foundations

Depth 208 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceAddCommGroupModuleNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceIsTopologicalAddGroupContinuousSMulFiberBundleVectorBundleContMDiffVectorBundleMemTrivializationAtlas