Theorems · Theorem · algebraic topology

ContinuousLinearMap.inCoordinates_eq

∀ {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : (x : B) → AddCommMonoid (E x)]
  [inst_1 : NormedAddCommGroup F] [inst_2 : TopologicalSpace B] [inst_3 : (x : B) → TopologicalSpace (E x)]
  {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} [inst_4 : NontriviallyNormedField 𝕜₁] [inst_5 : NontriviallyNormedField 𝕜₂]
  {σ : 𝕜₁ →+* 𝕜₂} {B' : Type u_7} [inst_6 : TopologicalSpace B'] [inst_7 : NormedSpace 𝕜₁ F]
  [inst_8 : (x : B) → Module 𝕜₁ (E x)] [inst_9 : TopologicalSpace (Bundle.TotalSpace F E)] {F' : Type u_8}
  [inst_10 : NormedAddCommGroup F'] [inst_11 : NormedSpace 𝕜₂ F'] {E' : B' → Type u_9}
  [inst_12 : (x : B') → AddCommMonoid (E' x)] [inst_13 : (x : B') → Module 𝕜₂ (E' x)]
  [inst_14 : TopologicalSpace (Bundle.TotalSpace F' E')] [inst_15 : FiberBundle F E] [inst_16 : VectorBundle 𝕜₁ F E]
  [inst_17 : (x : B') → TopologicalSpace (E' x)] [inst_18 : FiberBundle F' E'] [inst_19 : VectorBundle 𝕜₂ F' E']
  {x₀ x : B} {y₀ y : B'} {ϕ : E x →SL[σ] E' y} (hx : x ∈ (trivializationAt F E x₀).baseSet)
  (hy : y ∈ (trivializationAt F' E' y₀).baseSet),
  ContinuousLinearMap.inCoordinates F E F' E' x₀ x y₀ y ϕ =
    ↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜₂ (trivializationAt F' E' y₀) y hy) ∘SL
      ϕ ∘SL ↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜₁ (trivializationAt F E x₀) x hx).symm

Rewrite ContinuousLinearMap.inCoordinates using continuous linear equivalences.

Defined in

Mathlib.Topology.VectorBundle.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

AddCommMonoidNormedAddCommGroupTopologicalSpaceTopologicalSpaceNontriviallyNormedFieldNontriviallyNormedFieldTopologicalSpaceNormedSpaceModuleTopologicalSpaceNormedAddCommGroupNormedSpaceAddCommMonoidModuleTopologicalSpaceFiberBundleVectorBundleTopologicalSpaceFiberBundleVectorBundle