Theorems · Definition · algebraic topology

ContinuousLinearMap.inCoordinates

{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] →
                                                  [VectorBundle 𝕜₁ F E] →
                                                    [inst_17 : (x : B') → TopologicalSpace (E' x)] →
                                                      [inst_18 : FiberBundle F' E'] →
                                                        [VectorBundle 𝕜₂ F' E'] →
                                                          B → (x : B) → B' → (y : B') → (E x →SL[σ] E' y) → F →SL[σ] F'

When ϕ is a continuous (semi)linear map between the fibers E x and E' y of two vector bundles E and E', ContinuousLinearMap.inCoordinates F E F' E' x₀ x y₀ y ϕ is a coordinate change of this continuous linear map w.r.t. the chart around x₀ and the chart around y₀. It is defined by composing ϕ with appropriate coordinate changes given by the vector bundles E and E'. We use the operations Bundle.Trivialization.continuousLinearMapAt and Bundle.Trivialization.symmL in the definition, instead of Bundle.Trivialization.continuousLinearEquivAt, so that ContinuousLinearMap.inCoordinates is defined everywhere (but see ContinuousLinearMap.inCoordinates_eq). This is the (second component of the) underlying function of a trivialization of the hom-bundle (see hom_trivializationAt_apply). However, note that ContinuousLinearMap.inCoordinates is defined even when x and y live in different base sets. Therefore, it is also convenient when working with the hom-bundle between pulled back bundles.

Defined in

Mathlib.Topology.VectorBundle.Basic

Cited by

24 results in Mathlib

Foundations

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

Assumes

AddCommMonoidNormedAddCommGroupTopologicalSpaceTopologicalSpaceNontriviallyNormedFieldNontriviallyNormedFieldTopologicalSpaceNormedSpaceModuleTopologicalSpaceNormedAddCommGroupNormedSpaceAddCommMonoidModuleTopologicalSpaceFiberBundleVectorBundleTopologicalSpaceFiberBundleVectorBundle