Smooth paired wedges with bundle coefficients

A smooth fibrewise bilinear pairing sends two smooth bundle-valued differential forms to a smooth form in its target bundle. The pairing may vary with the base point, and none of the value bundles needs a global trivialization or a norm on its individual fibres.

ContMDiffWithinAt.bundleWedgeWith_form gives the relative regularity statement, including boundary and corner points. SmoothBundleForm.wedgeWith packages the smooth product as a bilinear map. In bundle coordinates the product is the continuous trilinear paired wedge on the model fibres, applied to the coordinates of the pairing and of the two forms.

The wedge normalization and bundle-valued construction follow John M. Lee, Introduction to Smooth Manifolds, second edition, Chapter 14, and the paired-wedge design of Yury Kudryashov's DeRhamCohomology.

theorem TauCeti.inCoordinates_bundleWedgeWith {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} {F₃ : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] {V₁ : M → Type u_7} {V₂ : M → Type u_8} {V₃ : M → Type u_9} [(x : M) → AddCommGroup (V₁ x)] [(x : M) → Module ℝ (V₁ x)] [(x : M) → TopologicalSpace (V₁ x)] [(x : M) → AddCommGroup (V₂ x)] [(x : M) → Module ℝ (V₂ x)] [(x : M) → TopologicalSpace (V₂ x)] [(x : M) → AddCommGroup (V₃ x)] [(x : M) → Module ℝ (V₃ x)] [(x : M) → 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 : M), IsTopologicalAddGroup (V₃ x)] [∀ (x : M), ContinuousSMul ℝ (V₃ x)] [IsManifold I 1 M] {k l : ℕ} (μ : (y : M) → V₁ y →L[ℝ] V₂ y →L[ℝ] V₃ y) (hμ : ∀ (y : M), Continuous (Function.uncurry fun (a : V₁ y) (b : V₂ y) => ((μ y) a) b)) (φ : RoughBundleForm I M V₁ k) (ψ : RoughBundleForm I M V₂ l) (x₀ y : M) (h₁ : y ∈ (trivializationAt F₁ V₁ x₀).baseSet) (h₂ : y ∈ (trivializationAt F₂ V₂ x₀).baseSet) (h₃ : y ∈ (trivializationAt F₃ V₃ x₀).baseSet) : ContinuousAlternatingMap.inCoordinates E F₃ x₀ y x₀ y (bundleWedgeWith μ hμ φ ψ y) = ((ContinuousAlternatingMap.pairedWedgeCLM (ContinuousLinearMap.inCoordinates F₁ V₁ (F₂ →L[ℝ] F₃) (fun (z : M) => V₂ z →L[ℝ] V₃ z) x₀ y x₀ y (μ y))) (ContinuousAlternatingMap.inCoordinates E F₁ x₀ y x₀ y (φ y))) (ContinuousAlternatingMap.inCoordinates E F₂ x₀ y x₀ y (ψ y))

In valid coefficient trivializations, coordinates of a bundle wedge are the paired wedge of the coordinates, with the pairing itself also expressed in coordinates.

theorem ContMDiffWithinAt.bundleWedgeWith_form {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} {F₃ : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] {V₁ : M → Type u_7} {V₂ : M → Type u_8} {V₃ : M → Type u_9} [(x : M) → AddCommGroup (V₁ x)] [(x : M) → Module ℝ (V₁ x)] [(x : M) → TopologicalSpace (V₁ x)] [(x : M) → AddCommGroup (V₂ x)] [(x : M) → Module ℝ (V₂ x)] [(x : M) → TopologicalSpace (V₂ x)] [(x : M) → AddCommGroup (V₃ x)] [(x : M) → Module ℝ (V₃ x)] [(x : M) → 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 : M), IsTopologicalAddGroup (V₃ x)] [∀ (x : M), ContinuousSMul ℝ (V₃ x)] [IsManifold I 1 M] {k l : ℕ} {n : WithTop ℕ∞} {s : Set M} {x : M} [∀ (x : M), IsTopologicalAddGroup (V₁ x)] [∀ (x : M), ContinuousSMul ℝ (V₁ x)] [∀ (x : M), IsTopologicalAddGroup (V₂ x)] [∀ (x : M), ContinuousSMul ℝ (V₂ x)] {μ : (y : M) → V₁ y →L[ℝ] V₂ y →L[ℝ] V₃ y} (hμ : ∀ (y : M), Continuous (Function.uncurry fun (a : V₁ y) (b : V₂ y) => ((μ y) a) b)) (hpair : ContMDiffWithinAt I (I.prod (modelWithCornersSelf ℝ (F₁ →L[ℝ] F₂ →L[ℝ] F₃))) n (fun (y : M) => ⟨y, μ y⟩) s x) {φ : TauCeti.RoughBundleForm I M V₁ k} {ψ : TauCeti.RoughBundleForm I M V₂ l} (hφ : ContMDiffWithinAt I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin k]→L[ℝ] F₁))) n (fun (y : M) => ⟨y, φ y⟩) s x) (hψ : ContMDiffWithinAt I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin l]→L[ℝ] F₂))) n (fun (y : M) => ⟨y, ψ y⟩) s x) : ContMDiffWithinAt I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin (k + l)]→L[ℝ] F₃))) n (fun (y : M) => ⟨y, TauCeti.bundleWedgeWith μ hμ φ ψ y⟩) s x

A smooth bundle pairing takes two C^n bundle-valued forms to a C^n form within an arbitrary set.

theorem ContMDiffOn.bundleWedgeWith_form {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} {F₃ : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] {V₁ : M → Type u_7} {V₂ : M → Type u_8} {V₃ : M → Type u_9} [(x : M) → AddCommGroup (V₁ x)] [(x : M) → Module ℝ (V₁ x)] [(x : M) → TopologicalSpace (V₁ x)] [(x : M) → AddCommGroup (V₂ x)] [(x : M) → Module ℝ (V₂ x)] [(x : M) → TopologicalSpace (V₂ x)] [(x : M) → AddCommGroup (V₃ x)] [(x : M) → Module ℝ (V₃ x)] [(x : M) → 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 : M), IsTopologicalAddGroup (V₃ x)] [∀ (x : M), ContinuousSMul ℝ (V₃ x)] [IsManifold I 1 M] {k l : ℕ} {n : WithTop ℕ∞} {s : Set M} [∀ (x : M), IsTopologicalAddGroup (V₁ x)] [∀ (x : M), ContinuousSMul ℝ (V₁ x)] [∀ (x : M), IsTopologicalAddGroup (V₂ x)] [∀ (x : M), ContinuousSMul ℝ (V₂ x)] {μ : (y : M) → V₁ y →L[ℝ] V₂ y →L[ℝ] V₃ y} (hμ : ∀ (y : M), Continuous (Function.uncurry fun (a : V₁ y) (b : V₂ y) => ((μ y) a) b)) (hpair : ContMDiffOn I (I.prod (modelWithCornersSelf ℝ (F₁ →L[ℝ] F₂ →L[ℝ] F₃))) n (fun (y : M) => ⟨y, μ y⟩) s) {φ : TauCeti.RoughBundleForm I M V₁ k} {ψ : TauCeti.RoughBundleForm I M V₂ l} (hφ : ContMDiffOn I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin k]→L[ℝ] F₁))) n (fun (y : M) => ⟨y, φ y⟩) s) (hψ : ContMDiffOn I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin l]→L[ℝ] F₂))) n (fun (y : M) => ⟨y, ψ y⟩) s) : ContMDiffOn I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin (k + l)]→L[ℝ] F₃))) n (fun (y : M) => ⟨y, TauCeti.bundleWedgeWith μ hμ φ ψ y⟩) s

A C^n bundle pairing takes C^n bundle-valued forms to a C^n form on a set.

theorem ContMDiffAt.bundleWedgeWith_form {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} {F₃ : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] {V₁ : M → Type u_7} {V₂ : M → Type u_8} {V₃ : M → Type u_9} [(x : M) → AddCommGroup (V₁ x)] [(x : M) → Module ℝ (V₁ x)] [(x : M) → TopologicalSpace (V₁ x)] [(x : M) → AddCommGroup (V₂ x)] [(x : M) → Module ℝ (V₂ x)] [(x : M) → TopologicalSpace (V₂ x)] [(x : M) → AddCommGroup (V₃ x)] [(x : M) → Module ℝ (V₃ x)] [(x : M) → 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 : M), IsTopologicalAddGroup (V₃ x)] [∀ (x : M), ContinuousSMul ℝ (V₃ x)] [IsManifold I 1 M] {k l : ℕ} {n : WithTop ℕ∞} {x : M} [∀ (x : M), IsTopologicalAddGroup (V₁ x)] [∀ (x : M), ContinuousSMul ℝ (V₁ x)] [∀ (x : M), IsTopologicalAddGroup (V₂ x)] [∀ (x : M), ContinuousSMul ℝ (V₂ x)] {μ : (y : M) → V₁ y →L[ℝ] V₂ y →L[ℝ] V₃ y} (hμ : ∀ (y : M), Continuous (Function.uncurry fun (a : V₁ y) (b : V₂ y) => ((μ y) a) b)) (hpair : ContMDiffAt I (I.prod (modelWithCornersSelf ℝ (F₁ →L[ℝ] F₂ →L[ℝ] F₃))) n (fun (y : M) => ⟨y, μ y⟩) x) {φ : TauCeti.RoughBundleForm I M V₁ k} {ψ : TauCeti.RoughBundleForm I M V₂ l} (hφ : ContMDiffAt I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin k]→L[ℝ] F₁))) n (fun (y : M) => ⟨y, φ y⟩) x) (hψ : ContMDiffAt I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin l]→L[ℝ] F₂))) n (fun (y : M) => ⟨y, ψ y⟩) x) : ContMDiffAt I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin (k + l)]→L[ℝ] F₃))) n (fun (y : M) => ⟨y, TauCeti.bundleWedgeWith μ hμ φ ψ y⟩) x

Pointwise regularity of a bundle wedge follows from regularity of both forms and pairing.

theorem TauCeti.IsSmoothBundleForm.bundleWedgeWith {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} {F₃ : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] {V₁ : M → Type u_7} {V₂ : M → Type u_8} {V₃ : M → Type u_9} [(x : M) → AddCommGroup (V₁ x)] [(x : M) → Module ℝ (V₁ x)] [(x : M) → TopologicalSpace (V₁ x)] [(x : M) → AddCommGroup (V₂ x)] [(x : M) → Module ℝ (V₂ x)] [(x : M) → TopologicalSpace (V₂ x)] [(x : M) → AddCommGroup (V₃ x)] [(x : M) → Module ℝ (V₃ x)] [(x : M) → 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 : M), IsTopologicalAddGroup (V₃ x)] [∀ (x : M), ContinuousSMul ℝ (V₃ x)] [IsManifold I 1 M] {k l : ℕ} {n : WithTop ℕ∞} [∀ (x : M), IsTopologicalAddGroup (V₁ x)] [∀ (x : M), ContinuousSMul ℝ (V₁ x)] [∀ (x : M), IsTopologicalAddGroup (V₂ x)] [∀ (x : M), ContinuousSMul ℝ (V₂ x)] {μ : (y : M) → V₁ y →L[ℝ] V₂ y →L[ℝ] V₃ y} (hμ : ∀ (y : M), Continuous (Function.uncurry fun (a : V₁ y) (b : V₂ y) => ((μ y) a) b)) (hpair : ContMDiff I (I.prod (modelWithCornersSelf ℝ (F₁ →L[ℝ] F₂ →L[ℝ] F₃))) n fun (y : M) => ⟨y, μ y⟩) {φ : RoughBundleForm I M V₁ k} {ψ : RoughBundleForm I M V₂ l} (hφ : IsSmoothBundleForm I F₁ V₁ n φ) (hψ : IsSmoothBundleForm I F₂ V₂ n ψ) : IsSmoothBundleForm I F₃ V₃ n (TauCeti.bundleWedgeWith μ hμ φ ψ)

A C^n pairing preserves C^n bundle-valued forms.

noncomputable def TauCeti.SmoothBundleForm.wedgeWith {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} {F₃ : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] {V₁ : M → Type u_7} {V₂ : M → Type u_8} {V₃ : M → Type u_9} [(x : M) → AddCommGroup (V₁ x)] [(x : M) → Module ℝ (V₁ x)] [(x : M) → TopologicalSpace (V₁ x)] [(x : M) → AddCommGroup (V₂ x)] [(x : M) → Module ℝ (V₂ x)] [(x : M) → TopologicalSpace (V₂ x)] [(x : M) → AddCommGroup (V₃ x)] [(x : M) → Module ℝ (V₃ x)] [(x : M) → 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 : M), IsTopologicalAddGroup (V₃ x)] [∀ (x : M), ContinuousSMul ℝ (V₃ x)] [IsManifold I 1 M] {k l : ℕ} [∀ (x : M), IsTopologicalAddGroup (V₁ x)] [∀ (x : M), ContinuousSMul ℝ (V₁ x)] [∀ (x : M), IsTopologicalAddGroup (V₂ x)] [∀ (x : M), ContinuousSMul ℝ (V₂ x)] (μ : (y : M) → V₁ y →L[ℝ] V₂ y →L[ℝ] V₃ y) (hμ : ∀ (y : M), Continuous (Function.uncurry fun (a : V₁ y) (b : V₂ y) => ((μ y) a) b)) (hpair : ContMDiff I (I.prod (modelWithCornersSelf ℝ (F₁ →L[ℝ] F₂ →L[ℝ] F₃))) ↑⊤ fun (y : M) => ⟨y, μ y⟩) : SmoothBundleForm I F₁ V₁ k →ₗ[ℝ] SmoothBundleForm I F₂ V₂ l →ₗ[ℝ] SmoothBundleForm I F₃ V₃ (k + l)

The wedge induced by a smooth bundle pairing, as a bilinear map on smooth forms.

@[simp]

theorem TauCeti.SmoothBundleForm.coe_wedgeWith {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} {F₃ : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] {V₁ : M → Type u_7} {V₂ : M → Type u_8} {V₃ : M → Type u_9} [(x : M) → AddCommGroup (V₁ x)] [(x : M) → Module ℝ (V₁ x)] [(x : M) → TopologicalSpace (V₁ x)] [(x : M) → AddCommGroup (V₂ x)] [(x : M) → Module ℝ (V₂ x)] [(x : M) → TopologicalSpace (V₂ x)] [(x : M) → AddCommGroup (V₃ x)] [(x : M) → Module ℝ (V₃ x)] [(x : M) → 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 : M), IsTopologicalAddGroup (V₃ x)] [∀ (x : M), ContinuousSMul ℝ (V₃ x)] [IsManifold I 1 M] {k l : ℕ} [∀ (x : M), IsTopologicalAddGroup (V₁ x)] [∀ (x : M), ContinuousSMul ℝ (V₁ x)] [∀ (x : M), IsTopologicalAddGroup (V₂ x)] [∀ (x : M), ContinuousSMul ℝ (V₂ x)] (μ : (y : M) → V₁ y →L[ℝ] V₂ y →L[ℝ] V₃ y) (hμ : ∀ (y : M), Continuous (Function.uncurry fun (a : V₁ y) (b : V₂ y) => ((μ y) a) b)) (hpair : ContMDiff I (I.prod (modelWithCornersSelf ℝ (F₁ →L[ℝ] F₂ →L[ℝ] F₃))) ↑⊤ fun (y : M) => ⟨y, μ y⟩) (φ : SmoothBundleForm I F₁ V₁ k) (ψ : SmoothBundleForm I F₂ V₂ l) : ↑(((wedgeWith μ hμ hpair) φ) ψ) = bundleWedgeWith μ hμ ↑φ ↑ψ

The smooth bundle wedge has the existing rough bundle wedge as its underlying form.

theorem TauCeti.SmoothBundleForm.wedgeWith_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} {F₃ : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] {V₁ : M → Type u_7} {V₂ : M → Type u_8} {V₃ : M → Type u_9} [(x : M) → AddCommGroup (V₁ x)] [(x : M) → Module ℝ (V₁ x)] [(x : M) → TopologicalSpace (V₁ x)] [(x : M) → AddCommGroup (V₂ x)] [(x : M) → Module ℝ (V₂ x)] [(x : M) → TopologicalSpace (V₂ x)] [(x : M) → AddCommGroup (V₃ x)] [(x : M) → Module ℝ (V₃ x)] [(x : M) → 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 : M), IsTopologicalAddGroup (V₃ x)] [∀ (x : M), ContinuousSMul ℝ (V₃ x)] [IsManifold I 1 M] {k l : ℕ} [∀ (x : M), IsTopologicalAddGroup (V₁ x)] [∀ (x : M), ContinuousSMul ℝ (V₁ x)] [∀ (x : M), IsTopologicalAddGroup (V₂ x)] [∀ (x : M), ContinuousSMul ℝ (V₂ x)] (μ : (y : M) → V₁ y →L[ℝ] V₂ y →L[ℝ] V₃ y) (hμ : ∀ (y : M), Continuous (Function.uncurry fun (a : V₁ y) (b : V₂ y) => ((μ y) a) b)) (hpair : ContMDiff I (I.prod (modelWithCornersSelf ℝ (F₁ →L[ℝ] F₂ →L[ℝ] F₃))) ↑⊤ fun (y : M) => ⟨y, μ y⟩) (φ : SmoothBundleForm I F₁ V₁ k) (ψ : SmoothBundleForm I F₂ V₂ l) (y : M) (v : Fin (k + l) → TangentSpace I y) : (↑(((wedgeWith μ hμ hpair) φ) ψ) y) v = (↑k.factorial * ↑l.factorial)⁻¹ • ∑ σ : Equiv.Perm (Fin (k + l)), Equiv.Perm.sign σ • ((μ y) ((↑φ y) fun (i : Fin k) => v (σ (Fin.castAdd l i)))) ((↑ψ y) fun (j : Fin l) => v (σ (Fin.natAdd k j)))

Evaluation of the smooth bundle wedge on a tangent tuple.

theorem TauCeti.SmoothBundleForm.wedgeWith_apply_one_one {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} {F₃ : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] {V₁ : M → Type u_7} {V₂ : M → Type u_8} {V₃ : M → Type u_9} [(x : M) → AddCommGroup (V₁ x)] [(x : M) → Module ℝ (V₁ x)] [(x : M) → TopologicalSpace (V₁ x)] [(x : M) → AddCommGroup (V₂ x)] [(x : M) → Module ℝ (V₂ x)] [(x : M) → TopologicalSpace (V₂ x)] [(x : M) → AddCommGroup (V₃ x)] [(x : M) → Module ℝ (V₃ x)] [(x : M) → 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 : M), IsTopologicalAddGroup (V₃ x)] [∀ (x : M), ContinuousSMul ℝ (V₃ x)] [IsManifold I 1 M] [∀ (x : M), IsTopologicalAddGroup (V₁ x)] [∀ (x : M), ContinuousSMul ℝ (V₁ x)] [∀ (x : M), IsTopologicalAddGroup (V₂ x)] [∀ (x : M), ContinuousSMul ℝ (V₂ x)] (μ : (y : M) → V₁ y →L[ℝ] V₂ y →L[ℝ] V₃ y) (hμ : ∀ (y : M), Continuous (Function.uncurry fun (a : V₁ y) (b : V₂ y) => ((μ y) a) b)) (hpair : ContMDiff I (I.prod (modelWithCornersSelf ℝ (F₁ →L[ℝ] F₂ →L[ℝ] F₃))) ↑⊤ fun (y : M) => ⟨y, μ y⟩) (φ : SmoothBundleForm I F₁ V₁ 1) (ψ : SmoothBundleForm I F₂ V₂ 1) (y : M) (v w : TangentSpace I y) : (↑(((wedgeWith μ hμ hpair) φ) ψ) y) ![v, w] = ((μ y) ((↑φ y) ![v])) ((↑ψ y) ![w]) - ((μ y) ((↑φ y) ![w])) ((↑ψ y) ![v])

The smooth bundle wedge of two one-forms is the alternating two-term pairing.