Composition in alternating-bundle coordinates

Precomposing a fibrewise alternating map with a fibrewise linear map commutes with passing into bundle coordinates wherever the intermediate trivialization is valid. This identity allows regularity of pullbacks to be checked on fixed model fibres, without choosing norms on the original fibres.

In degree one, the identification ContinuousAlternatingMap.ofSubsingleton of linear maps with alternating maps of one variable also commutes with passing into coordinates, with no base-set hypothesis. This compares regularity of degree-one forms with regularity of sections of the bundle of fibrewise linear maps.

When the codomain is a fixed space, a fibre alternating map read in the trivialization at x₀ is precomposed with the inverse, at its base point, of the trivialization of the domain bundle at x₀ (FiberBundle.trivializationAt_continuousAlternatingMap_apply_snd). This holds everywhere, with no base-set hypothesis.

The coordinate maps are Mathlib's ContinuousAlternatingMap.inCoordinates and ContinuousLinearMap.inCoordinates.

theorem ContinuousAlternatingMap.inCoordinates_compContinuousLinearMap {𝕜 : Type u_1} {ι : Type u_2} {B₁ : Type u_3} {B₂ : Type u_4} {B₃ : Type u_5} {F₁ : Type u_6} {F₂ : Type u_7} {F₃ : Type u_8} [NontriviallyNormedField 𝕜] [TopologicalSpace B₁] [TopologicalSpace B₂] [TopologicalSpace B₃] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {V₁ : B₁ → Type u_9} {V₂ : B₂ → Type u_10} {V₃ : B₃ → Type u_11} [(x : B₁) → AddCommGroup (V₁ x)] [(x : B₁) → Module 𝕜 (V₁ x)] [(x : B₁) → TopologicalSpace (V₁ x)] [(x : B₂) → AddCommGroup (V₂ x)] [(x : B₂) → Module 𝕜 (V₂ x)] [(x : B₂) → TopologicalSpace (V₂ x)] [(x : B₃) → AddCommGroup (V₃ x)] [(x : B₃) → Module 𝕜 (V₃ x)] [(x : B₃) → TopologicalSpace (V₃ x)] [TopologicalSpace (Bundle.TotalSpace F₁ V₁)] [FiberBundle F₁ V₁] [VectorBundle 𝕜 F₁ V₁] [TopologicalSpace (Bundle.TotalSpace F₂ V₂)] [FiberBundle F₂ V₂] [VectorBundle 𝕜 F₂ V₂] [TopologicalSpace (Bundle.TotalSpace F₃ V₃)] [FiberBundle F₃ V₃] [VectorBundle 𝕜 F₃ V₃] {x₀ x : B₁} {y₀ y : B₂} {z₀ z : B₃} (φ : V₂ y [⋀^ι]→L[𝕜] V₃ z) (A : V₁ x →L[𝕜] V₂ y) (hy : y ∈ (trivializationAt F₂ V₂ y₀).baseSet) : inCoordinates F₁ F₃ x₀ x z₀ z (φ.compContinuousLinearMap A) = (inCoordinates F₂ F₃ y₀ y z₀ z φ).compContinuousLinearMap (ContinuousLinearMap.inCoordinates F₁ V₁ F₂ V₂ x₀ x y₀ y A)

Coordinates of precomposition are precomposition of coordinates. Only the intermediate fibre must belong to its chosen trivialization's base set.

@[simp]

theorem ContinuousAlternatingMap.inCoordinates_ofSubsingleton {𝕜 : Type u_1} {ι : Type u_2} {B₁ : Type u_3} {B₂ : Type u_4} {F₁ : Type u_6} {F₂ : Type u_7} [NontriviallyNormedField 𝕜] [TopologicalSpace B₁] [TopologicalSpace B₂] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {V₁ : B₁ → Type u_9} {V₂ : B₂ → Type u_10} [(x : B₁) → AddCommGroup (V₁ x)] [(x : B₁) → Module 𝕜 (V₁ x)] [(x : B₁) → TopologicalSpace (V₁ x)] [(x : B₂) → AddCommGroup (V₂ x)] [(x : B₂) → Module 𝕜 (V₂ x)] [(x : B₂) → TopologicalSpace (V₂ x)] [TopologicalSpace (Bundle.TotalSpace F₁ V₁)] [FiberBundle F₁ V₁] [VectorBundle 𝕜 F₁ V₁] [TopologicalSpace (Bundle.TotalSpace F₂ V₂)] [FiberBundle F₂ V₂] [VectorBundle 𝕜 F₂ V₂] [Subsingleton ι] (i : ι) {x₀ x : B₁} {y₀ y : B₂} (φ : V₁ x →L[𝕜] V₂ y) : inCoordinates F₁ F₂ x₀ x y₀ y ((ofSubsingleton 𝕜 (V₁ x) (V₂ y) i) φ) = (ofSubsingleton 𝕜 F₁ F₂ i) (ContinuousLinearMap.inCoordinates F₁ V₁ F₂ V₂ x₀ x y₀ y φ)

Coordinates of a fibrewise linear map, viewed as an alternating map of one variable, are the coordinates of the linear map, viewed in the same way.

@[simp]

theorem FiberBundle.trivializationAt_continuousAlternatingMap_apply_snd {𝕜 : Type u_1} {ι : Type u_2} {B : Type u_3} {F₁ : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [Fintype ι] [TopologicalSpace B] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [(x : B) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F₁ V)] [FiberBundle F₁ V] [VectorBundle 𝕜 F₁ V] (x₀ : B) {x : B} (ω : V x [⋀^ι]→L[𝕜] F) : (↑(trivializationAt (F₁ [⋀^ι]→L[𝕜] F) (fun (x : B) => V x [⋀^ι]→L[𝕜] F) x₀) { proj := x, snd := ω }).2 = ω.compContinuousLinearMap (Bundle.Trivialization.symmL 𝕜 (trivializationAt F₁ V x₀) x)

In the trivialization at x₀ of the bundle of alternating maps from V to a fixed space F, a fibre map ω at x is precomposed with the inverse, at x, of the trivialization of V at x₀.