Associativity of topological paired wedges

Paired wedges are associative whenever the two composites of their coefficient pairings agree. The domain and coefficient spaces need no norms. This permits iterated wedges on tangent fibres and on general topological vector bundles. Joint continuity of each pairing is stated explicitly; separate continuity alone does not suffice. On the intermediate and final coefficient spaces, scalar multiplication need only be continuous for each fixed scalar.

The iterated evaluation formulas flatten the nested alternatizations into a single signed permutation sum with coefficient 1 / (k! l! m!). They use signed-sum reindexing for the nested alternatizations. The normalization follows John M. Lee, Introduction to Smooth Manifolds, second edition, Chapter 14.

theorem ContinuousAlternatingMap.pairedWedge_pairedWedge_left_apply {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} {F₁₂ : Type u_5} {G : Type u_7} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [AddCommGroup F₁₂] [Module ℝ F₁₂] [TopologicalSpace F₁₂] [IsTopologicalAddGroup F₁₂] [ContinuousConstSMul ℝ F₁₂] [AddCommGroup G] [Module ℝ G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul ℝ G] {k l m : ℕ} (mu₁₂ : F₁ →L[ℝ] F₂ →L[ℝ] F₁₂) (mu₁₂₃ : F₁₂ →L[ℝ] F₃ →L[ℝ] G) (h₁₂ : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (mu₁₂ x) y)) (h₁₂₃ : Continuous (Function.uncurry fun (x : F₁₂) (y : F₃) => (mu₁₂₃ x) y)) (phi : E [⋀^Fin k]→L[ℝ] F₁) (psi : E [⋀^Fin l]→L[ℝ] F₂) (chi : E [⋀^Fin m]→L[ℝ] F₃) (v : Fin (k + l + m) → E) : (pairedWedge mu₁₂₃ h₁₂₃ (pairedWedge mu₁₂ h₁₂ phi psi) chi) v = (↑k.factorial * ↑l.factorial * ↑m.factorial)⁻¹ • ∑ sigma : Equiv.Perm (Fin (k + l + m)), Equiv.Perm.sign sigma • (mu₁₂₃ ((mu₁₂ (phi fun (i : Fin k) => v (sigma (Fin.castAdd m (Fin.castAdd l i))))) (psi fun (j : Fin l) => v (sigma (Fin.castAdd m (Fin.natAdd k j)))))) (chi fun (r : Fin m) => v (sigma (Fin.natAdd (k + l) r)))

A paired wedge whose left factor is itself a paired wedge is the signed sum over all permutations of k + l + m slots, divided by k! l! m!.

theorem ContinuousAlternatingMap.pairedWedge_pairedWedge_right_apply {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} {F₂₃ : Type u_6} {G : Type u_7} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [AddCommGroup F₂₃] [Module ℝ F₂₃] [TopologicalSpace F₂₃] [IsTopologicalAddGroup F₂₃] [ContinuousConstSMul ℝ F₂₃] [AddCommGroup G] [Module ℝ G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul ℝ G] {k l m : ℕ} (mu₂₃ : F₂ →L[ℝ] F₃ →L[ℝ] F₂₃) (mu₁₂₃' : F₁ →L[ℝ] F₂₃ →L[ℝ] G) (h₂₃ : Continuous (Function.uncurry fun (x : F₂) (y : F₃) => (mu₂₃ x) y)) (h₁₂₃' : Continuous (Function.uncurry fun (x : F₁) (y : F₂₃) => (mu₁₂₃' x) y)) (phi : E [⋀^Fin k]→L[ℝ] F₁) (psi : E [⋀^Fin l]→L[ℝ] F₂) (chi : E [⋀^Fin m]→L[ℝ] F₃) (v : Fin (k + (l + m)) → E) : (pairedWedge mu₁₂₃' h₁₂₃' phi (pairedWedge mu₂₃ h₂₃ psi chi)) v = (↑k.factorial * ↑l.factorial * ↑m.factorial)⁻¹ • ∑ sigma : Equiv.Perm (Fin (k + (l + m))), Equiv.Perm.sign sigma • (mu₁₂₃' (phi fun (i : Fin k) => v (sigma (Fin.castAdd (l + m) i)))) ((mu₂₃ (psi fun (j : Fin l) => v (sigma (Fin.natAdd k (Fin.castAdd m j))))) (chi fun (r : Fin m) => v (sigma (Fin.natAdd k (Fin.natAdd l r)))))

A paired wedge whose right factor is itself a paired wedge is the signed sum over all permutations of k + (l + m) slots, divided by k! l! m!.

theorem ContinuousAlternatingMap.pairedWedge_assoc {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} {F₁₂ : Type u_5} {F₂₃ : Type u_6} {G : Type u_7} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [AddCommGroup F₁₂] [Module ℝ F₁₂] [TopologicalSpace F₁₂] [IsTopologicalAddGroup F₁₂] [ContinuousConstSMul ℝ F₁₂] [AddCommGroup F₂₃] [Module ℝ F₂₃] [TopologicalSpace F₂₃] [IsTopologicalAddGroup F₂₃] [ContinuousConstSMul ℝ F₂₃] [AddCommGroup G] [Module ℝ G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul ℝ G] {k l m : ℕ} (mu₁₂ : F₁ →L[ℝ] F₂ →L[ℝ] F₁₂) (mu₁₂₃ : F₁₂ →L[ℝ] F₃ →L[ℝ] G) (mu₂₃ : F₂ →L[ℝ] F₃ →L[ℝ] F₂₃) (mu₁₂₃' : F₁ →L[ℝ] F₂₃ →L[ℝ] G) (h₁₂ : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (mu₁₂ x) y)) (h₁₂₃ : Continuous (Function.uncurry fun (x : F₁₂) (y : F₃) => (mu₁₂₃ x) y)) (h₂₃ : Continuous (Function.uncurry fun (x : F₂) (y : F₃) => (mu₂₃ x) y)) (h₁₂₃' : Continuous (Function.uncurry fun (x : F₁) (y : F₂₃) => (mu₁₂₃' x) y)) (h : ∀ (a : F₁) (b : F₂) (c : F₃), (mu₁₂₃ ((mu₁₂ a) b)) c = (mu₁₂₃' a) ((mu₂₃ b) c)) (phi : E [⋀^Fin k]→L[ℝ] F₁) (psi : E [⋀^Fin l]→L[ℝ] F₂) (chi : E [⋀^Fin m]→L[ℝ] F₃) (v : Fin (k + l + m) → E) : (pairedWedge mu₁₂₃ h₁₂₃ (pairedWedge mu₁₂ h₁₂ phi psi) chi) v = (pairedWedge mu₁₂₃' h₁₂₃' phi (pairedWedge mu₂₃ h₂₃ psi chi)) (v ∘ Fin.cast ⋯)

Associativity of the paired wedge, for pairings whose two composites agree: mu₁₂₃ (mu₁₂ a b) c = mu₁₂₃' a (mu₂₃ b c). For the multiplication of a normed algebra this hypothesis is mul_assoc; for a Lie bracket it does not hold in general.