Theorems · Definition · algebraic topology

ContinuousAlternatingMap.inCoordinates

{𝕜 : Type u_1} →
  {ι : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      {B₁ : Type u_3} →
        (F₁ : Type u_4) →
          [inst_1 : NormedAddCommGroup F₁] →
            [inst_2 : NormedSpace 𝕜 F₁] →
              {E₁ : B₁ → Type u_5} →
                [inst_3 : (x : B₁) → AddCommGroup (E₁ x)] →
                  [inst_4 : (x : B₁) → Module 𝕜 (E₁ x)] →
                    [inst_5 : TopologicalSpace B₁] →
                      [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] →
                        [inst_7 : (x : B₁) → TopologicalSpace (E₁ x)] →
                          [inst_8 : FiberBundle F₁ E₁] →
                            [VectorBundle 𝕜 F₁ E₁] →
                              {B₂ : Type u_6} →
                                (F₂ : Type u_7) →
                                  [inst_10 : NormedAddCommGroup F₂] →
                                    [inst_11 : NormedSpace 𝕜 F₂] →
                                      {E₂ : B₂ → Type u_8} →
                                        [inst_12 : (x : B₂) → AddCommGroup (E₂ x)] →
                                          [inst_13 : (x : B₂) → Module 𝕜 (E₂ x)] →
                                            [inst_14 : TopologicalSpace B₂] →
                                              [inst_15 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] →
                                                [inst_16 : (x : B₂) → TopologicalSpace (E₂ x)] →
                                                  [inst_17 : FiberBundle F₂ E₂] →
                                                    [VectorBundle 𝕜 F₂ E₂] →
                                                      B₁ →
                                                        (x : B₁) →
                                                          B₂ → (y : B₂) → E₁ x [⋀^ι]→L[𝕜] E₂ y → F₁ [⋀^ι]→L[𝕜] F₂

When ϕ is a continuous alternating map between the fibers E₁ x and E₂ y of two vector bundles E and E', ContinuousAlternatingMap.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 ContinuousAlternatingMap.inCoordinates is defined everywhere. See also ContinuousAlternatingMap.inCoordinates_eq. This is the (second component of the) underlying function of a trivialization of the bundle of continuous alternating maps, see FiberBundle.trivializationAt_continuousAlternatingMap_apply. However, note that ContinuousAlternatingMap.inCoordinates is defined even when x and y live in different base sets. Therefore, it is also convenient when working with the bundle of continuous alternating maps between pulled back bundles.

Defined in

Mathlib.Topology.VectorBundle.ContinuousAlternatingMap

Cited by

4 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceAddCommGroupModuleTopologicalSpaceTopologicalSpaceTopologicalSpaceFiberBundleVectorBundleNormedAddCommGroupNormedSpaceAddCommGroupModuleTopologicalSpaceTopologicalSpaceTopologicalSpaceFiberBundleVectorBundle