Theorems · Theorem · algebraic topology

ContinuousAlternatingMap.inCoordinates_eq

∀ {𝕜 : 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₁] [inst_9 : 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₂] [inst_18 : VectorBundle 𝕜 F₂ E₂] {x₀ x : B₁} {y₀ y : B₂} {ϕ : E₁ x [⋀^ι]→L[𝕜] E₂ y}
  (hx : x ∈ (trivializationAt F₁ E₁ x₀).baseSet) (hy : y ∈ (trivializationAt F₂ E₂ y₀).baseSet),
  ContinuousAlternatingMap.inCoordinates F₁ F₂ x₀ x y₀ y ϕ =
    ((↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt F₂ E₂ y₀) y hy)).compContinuousAlternatingMap
          ϕ).compContinuousLinearMap
      ↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt F₁ E₁ x₀) x hx).symm

Rewrite ContinuousAlternatingMap.inCoordinates using continuous linear equivalences.

Defined in

Mathlib.Topology.VectorBundle.ContinuousAlternatingMap

Cited by

0 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceAddCommGroupModuleTopologicalSpaceTopologicalSpaceTopologicalSpaceFiberBundleVectorBundleNormedAddCommGroupNormedSpaceAddCommGroupModuleTopologicalSpaceTopologicalSpaceTopologicalSpaceFiberBundleVectorBundle