Paired wedges of continuous alternating maps

This file constructs the paired wedge of continuous alternating maps on real modules with a topology. Its determinant normalization is the signed-permutation sum divided by the two input factorials. It provides bilinearity and pullback compatibility for general topological coefficient spaces, including the flip law, and transports a degree equality in the first factor through the wedge (ContinuousAlternatingMap.pairedWedge_apply_of_left_eq_smul_cast). A pairing that turns multiplication by one scalar into multiplication by another, such as a complex-bilinear pairing, makes the paired wedge semilinear in the same way, and the paired wedge is natural for coefficient maps intertwining two pairings. The paired wedge of two alternatizations is the alternatization of the paired product of the underlying multilinear maps. Joint continuity of each pairing is supplied explicitly; no norm is required on the domain or coefficients. The output coefficients require only continuity of multiplication by each fixed scalar. The flip law assumes this property for the second input coefficient space as well.

It also proves the norm-free interior-product antiderivation law ι_v (φ ∧ ψ) = ι_v φ ∧ ψ + (-1) ^ (deg φ) • φ ∧ ι_v ψ, using ContinuousAlternatingMap.curryLeftTopological from the accompanying Curry module. The normed counterpart is ContinuousAlternatingMap.curryLeft_pairedWedge. Consequently a wedge α ∧ ψ with a one-form α, evaluated on (u, w) where α kills every vector of w, is the pairing of α u with ψ w (ContinuousAlternatingMap.pairedWedge_apply_vecCons_of_forall).

The alternating-map API follows Mathlib's AlternatingMap.curryLeft and map_insertNth, and the paired-wedge design follows Yury Kudryashov's DeRhamCohomology project.

References

• John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Graduate Texts in Mathematics 218, Springer, 2013, Lemma 14.13.
• Yury Kudryashov's DeRhamCohomology project.

noncomputable def ContinuousAlternatingMap.pairingLinear {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) : TensorProduct ℝ F₁ F₂ →ₗ[ℝ] F₃

The linear map induced by a continuous bilinear pairing on the tensor product.

@[simp]

theorem ContinuousAlternatingMap.pairingLinear_tmul {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (x : F₁) (y : F₂) : (pairingLinear μ) (x ⊗ₜ[ℝ] y) = (μ x) y

The pairing-induced linear map evaluates pure tensors by the original pairing.

noncomputable def ContinuousAlternatingMap.wedgeWithUnalternated {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (φ : E [⋀^Fin k]→L[ℝ] F₁) (ψ : E [⋀^Fin l]→L[ℝ] F₂) : (Fin (k + l) → E) →ₘₗ[ℝ] F₃

The unalternated multilinear pairing underlying the paired wedge.

theorem ContinuousAlternatingMap.wedgeWithUnalternated_def {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (φ : E [⋀^Fin k]→L[ℝ] F₁) (ψ : E [⋀^Fin l]→L[ℝ] F₂) : wedgeWithUnalternated μ φ ψ = (pairingLinear μ).compMultilinearMap (MultilinearMap.domDomCongr finSumFinEquiv ((↑φ.toAlternatingMap).domCoprod ↑ψ.toAlternatingMap))

The tensor-product construction of the unalternated paired wedge.

@[simp]

theorem ContinuousAlternatingMap.wedgeWithUnalternated_apply {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (φ : E [⋀^Fin k]→L[ℝ] F₁) (ψ : E [⋀^Fin l]→L[ℝ] F₂) (v : Fin (k + l) → E) : (wedgeWithUnalternated μ φ ψ) v = (μ (φ fun (i : Fin k) => v (Fin.castAdd l i))) (ψ fun (j : Fin l) => v (Fin.natAdd k j))

Evaluation of the unalternated pairing on concatenated vectors.

noncomputable def ContinuousAlternatingMap.wedgeWithUnalternatedContinuous {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hμ : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (μ x) y)) (φ : E [⋀^Fin k]→L[ℝ] F₁) (ψ : E [⋀^Fin l]→L[ℝ] F₂) : E [×k + l]→L[ℝ] F₃

The continuous multilinear map associated to the unalternated paired product.

@[simp]

theorem ContinuousAlternatingMap.wedgeWithUnalternatedContinuous_apply {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hμ : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (μ x) y)) (φ : E [⋀^Fin k]→L[ℝ] F₁) (ψ : E [⋀^Fin l]→L[ℝ] F₂) (v : Fin (k + l) → E) : (wedgeWithUnalternatedContinuous μ hμ φ ψ) v = (μ (φ fun (i : Fin k) => v (Fin.castAdd l i))) (ψ fun (j : Fin l) => v (Fin.natAdd k j))

Evaluation of the continuous unalternated pairing on concatenated vectors.

noncomputable def ContinuousAlternatingMap.pairedWedge {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hμ : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (μ x) y)) (φ : E [⋀^Fin k]→L[ℝ] F₁) (ψ : E [⋀^Fin l]→L[ℝ] F₂) : E [⋀^Fin (k + l)]→L[ℝ] F₃

The paired wedge of continuous alternating maps, normalized by the two input factorials.

theorem ContinuousAlternatingMap.pairedWedge_apply {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hμ : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (μ x) y)) (φ : E [⋀^Fin k]→L[ℝ] F₁) (ψ : E [⋀^Fin l]→L[ℝ] F₂) (v : Fin (k + l) → E) : (pairedWedge μ hμ φ ψ) v = (↑k.factorial * ↑l.factorial)⁻¹ • ∑ σ : Equiv.Perm (Fin (k + l)), Equiv.Perm.sign σ • (μ (φ fun (i : Fin k) => v (σ (Fin.castAdd l i)))) (ψ fun (j : Fin l) => v (σ (Fin.natAdd k j)))

The pointwise formula for the paired wedge in all degrees.

@[simp]

theorem ContinuousAlternatingMap.pairedWedge_apply_zero_right {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] {k : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hμ : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (μ x) y)) (φ : E [⋀^Fin k]→L[ℝ] F₁) (ψ : E [⋀^Fin 0]→L[ℝ] F₂) (v : Fin k → E) : (pairedWedge μ hμ φ ψ) v = (μ (φ v)) (ψ 0)

Wedge with a degree-zero form is the coefficient pairing with its value on the empty tuple.

@[simp]

theorem ContinuousAlternatingMap.pairedWedge_apply_one_one {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] {μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃} (hμ : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (μ x) y)) (φ : E [⋀^Fin 1]→L[ℝ] F₁) (ψ : E [⋀^Fin 1]→L[ℝ] F₂) (v w : E) : (pairedWedge μ hμ φ ψ) ![v, w] = (μ (φ ![v])) (ψ ![w]) - (μ (φ ![w])) (ψ ![v])

On one-forms, the paired wedge is the usual two-term alternating product.

@[simp]

theorem ContinuousAlternatingMap.pairedWedge_toAlternatingMap {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] {k l : ℕ} (mu : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hmu : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (mu x) y)) (phi : E [⋀^Fin k]→L[ℝ] F₁) (psi : E [⋀^Fin l]→L[ℝ] F₂) : (pairedWedge mu hmu phi psi).toAlternatingMap = (↑k.factorial * ↑l.factorial)⁻¹ • MultilinearMap.alternatization (wedgeWithUnalternated mu phi psi)

The underlying alternating map of the paired wedge is the alternatization of its unalternated multilinear pairing, divided by k! l!.

theorem ContinuousAlternatingMap.pairedWedge_toAlternatingMap_of_eq_alternatization {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hμ : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (μ x) y)) {φ : E [⋀^Fin k]→L[ℝ] F₁} {ψ : E [⋀^Fin l]→L[ℝ] F₂} {f : (Fin k → E) →ₘₗ[ℝ] F₁} {g : (Fin l → E) →ₘₗ[ℝ] F₂} (hf : φ.toAlternatingMap = MultilinearMap.alternatization f) (hg : ψ.toAlternatingMap = MultilinearMap.alternatization g) : (pairedWedge μ hμ φ ψ).toAlternatingMap = MultilinearMap.alternatization ((pairingLinear μ).compMultilinearMap (MultilinearMap.domDomCongr finSumFinEquiv (f.domCoprod g)))

The paired wedge of alternatizations is the alternatization of the paired product: if φ and ψ are the alternatizations of f and g, then their paired wedge is the alternatization of v ↦ μ (f (v ∘ Fin.castAdd l)) (g (v ∘ Fin.natAdd k)). The factorials produced by alternatizing twice cancel the determinant normalization.

@[simp]

theorem ContinuousAlternatingMap.pairedWedge_compContinuousLinearMap {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] {E' : Type u_5} [AddCommGroup E'] [Module ℝ E'] [TopologicalSpace E'] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hμ : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (μ x) y)) (φ : E [⋀^Fin k]→L[ℝ] F₁) (ψ : E [⋀^Fin l]→L[ℝ] F₂) (f : E' →L[ℝ] E) : (pairedWedge μ hμ φ ψ).compContinuousLinearMap f = pairedWedge μ hμ (φ.compContinuousLinearMap f) (ψ.compContinuousLinearMap f)

Precomposing both inputs of a paired wedge by a continuous linear map is the same as precomposing the resulting wedge.

@[simp]

theorem ContinuousAlternatingMap.pairedWedge_add_left {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] [ContinuousAdd F₁] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hμ : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (μ x) y)) (φ φ' : E [⋀^Fin k]→L[ℝ] F₁) (ψ : E [⋀^Fin l]→L[ℝ] F₂) : pairedWedge μ hμ (φ + φ') ψ = pairedWedge μ hμ φ ψ + pairedWedge μ hμ φ' ψ

The paired wedge is additive in its first alternating map.

@[simp]

theorem ContinuousAlternatingMap.pairedWedge_add_right {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] [ContinuousAdd F₂] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hμ : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (μ x) y)) (φ : E [⋀^Fin k]→L[ℝ] F₁) (ψ ψ' : E [⋀^Fin l]→L[ℝ] F₂) : pairedWedge μ hμ φ (ψ + ψ') = pairedWedge μ hμ φ ψ + pairedWedge μ hμ φ ψ'

The paired wedge is additive in its second alternating map.

theorem ContinuousAlternatingMap.pairedWedge_sum_left {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] [ContinuousAdd F₁] {k l : ℕ} {ι : Type u_5} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hμ : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (μ x) y)) (s : Finset ι) (φ : ι → E [⋀^Fin k]→L[ℝ] F₁) (ψ : E [⋀^Fin l]→L[ℝ] F₂) : pairedWedge μ hμ (∑ i ∈ s, φ i) ψ = ∑ i ∈ s, pairedWedge μ hμ (φ i) ψ

The paired wedge distributes over finite sums in its first alternating map.

theorem ContinuousAlternatingMap.pairedWedge_sum_right {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] [ContinuousAdd F₂] {k l : ℕ} {ι : Type u_5} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hμ : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (μ x) y)) (s : Finset ι) (φ : E [⋀^Fin k]→L[ℝ] F₁) (ψ : ι → E [⋀^Fin l]→L[ℝ] F₂) : pairedWedge μ hμ φ (∑ i ∈ s, ψ i) = ∑ i ∈ s, pairedWedge μ hμ φ (ψ i)

The paired wedge distributes over finite sums in its second alternating map.

theorem ContinuousAlternatingMap.pairedWedge_smul_left_of_map_smul {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] {S : Type u_5} {S' : Type u_6} [Monoid S] [DistribMulAction S F₁] [ContinuousConstSMul S F₁] [SMulCommClass ℝ S F₁] [Monoid S'] [DistribMulAction S' F₃] [ContinuousConstSMul S' F₃] [SMulCommClass ℝ S' F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hμ : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (μ x) y)) {c : S} {d : S'} (hcd : ∀ (a : F₁) (b : F₂), (μ (c • a)) b = d • (μ a) b) (φ : E [⋀^Fin k]→L[ℝ] F₁) (ψ : E [⋀^Fin l]→L[ℝ] F₂) : pairedWedge μ hμ (c • φ) ψ = d • pairedWedge μ hμ φ ψ

If the pairing turns multiplication by c in its first argument into multiplication by d, then so does the paired wedge in its first alternating map. For a complex-bilinear pairing this is complex-linearity in the first factor; it also covers pairings that are conjugate-linear in the first argument.

theorem ContinuousAlternatingMap.pairedWedge_smul_right_of_map_smul {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] {S : Type u_5} {S' : Type u_6} [Monoid S] [DistribMulAction S F₂] [ContinuousConstSMul S F₂] [SMulCommClass ℝ S F₂] [Monoid S'] [DistribMulAction S' F₃] [ContinuousConstSMul S' F₃] [SMulCommClass ℝ S' F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hμ : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (μ x) y)) {c : S} {d : S'} (hcd : ∀ (a : F₁) (b : F₂), (μ a) (c • b) = d • (μ a) b) (φ : E [⋀^Fin k]→L[ℝ] F₁) (ψ : E [⋀^Fin l]→L[ℝ] F₂) : pairedWedge μ hμ φ (c • ψ) = d • pairedWedge μ hμ φ ψ

If the pairing turns multiplication by c in its second argument into multiplication by d, then so does the paired wedge in its second alternating map. For a complex-bilinear pairing this is complex-linearity in the second factor.

@[simp]

theorem ContinuousAlternatingMap.pairedWedge_smul_left {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] [ContinuousConstSMul ℝ F₁] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hμ : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (μ x) y)) (c : ℝ) (φ : E [⋀^Fin k]→L[ℝ] F₁) (ψ : E [⋀^Fin l]→L[ℝ] F₂) : pairedWedge μ hμ (c • φ) ψ = c • pairedWedge μ hμ φ ψ

The paired wedge respects scalar multiplication in its first alternating map.

@[simp]

theorem ContinuousAlternatingMap.pairedWedge_smul_right {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] [ContinuousConstSMul ℝ F₂] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hμ : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (μ x) y)) (c : ℝ) (φ : E [⋀^Fin k]→L[ℝ] F₁) (ψ : E [⋀^Fin l]→L[ℝ] F₂) : pairedWedge μ hμ φ (c • ψ) = c • pairedWedge μ hμ φ ψ

The paired wedge respects scalar multiplication in its second alternating map.

theorem ContinuousAlternatingMap.pairedWedge_apply_of_left_eq_smul_cast {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] [ContinuousConstSMul ℝ F₁] {a b l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hμ : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (μ x) y)) (h : a = b) {A : E [⋀^Fin b]→L[ℝ] F₁} {B : E [⋀^Fin a]→L[ℝ] F₁} (c : ℝ) (hAB : ∀ (w : Fin b → E), A w = c • B (w ∘ Fin.cast h)) (ψ : E [⋀^Fin l]→L[ℝ] F₂) (x : Fin (b + l) → E) : (pairedWedge μ hμ A ψ) x = c • (pairedWedge μ hμ B ψ) (x ∘ Fin.cast ⋯)

Degree transport in the first factor of a paired wedge: if A, of degree b, agrees with c • B after reindexing its arguments along Fin.cast h : Fin a → Fin b, then the wedge of A and ψ is c • the wedge of B and ψ, evaluated on the correspondingly transported tuple.

theorem ContinuousAlternatingMap.compContinuousAlternatingMap_pairedWedge {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddCommGroup G₁] [Module ℝ G₁] [TopologicalSpace G₁] [AddCommGroup G₂] [Module ℝ G₂] [TopologicalSpace G₂] [AddCommGroup G₃] [Module ℝ G₃] [TopologicalSpace G₃] [IsTopologicalAddGroup G₃] [ContinuousConstSMul ℝ G₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hμ : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (μ x) y)) (μ' : G₁ →L[ℝ] G₂ →L[ℝ] G₃) (hμ' : Continuous (Function.uncurry fun (x : G₁) (y : G₂) => (μ' x) y)) (L₁ : F₁ →L[ℝ] G₁) (L₂ : F₂ →L[ℝ] G₂) (L : F₃ →L[ℝ] G₃) (hL : ∀ (a : F₁) (b : F₂), L ((μ a) b) = (μ' (L₁ a)) (L₂ b)) (φ : E [⋀^Fin k]→L[ℝ] F₁) (ψ : E [⋀^Fin l]→L[ℝ] F₂) : L.compContinuousAlternatingMap (pairedWedge μ hμ φ ψ) = pairedWedge μ' hμ' (L₁.compContinuousAlternatingMap φ) (L₂.compContinuousAlternatingMap ψ)

The paired wedge is natural in the coefficients: if continuous linear maps L₁, L₂, L of the coefficient spaces intertwine the pairings μ and μ', then applying L to the paired wedge of φ and ψ gives the paired wedge of L₁ ∘ φ and L₂ ∘ ψ.

@[simp]

theorem ContinuousAlternatingMap.pairedWedge_postcomp {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] {F₄ : Type u_5} [AddCommGroup F₄] [Module ℝ F₄] [TopologicalSpace F₄] [IsTopologicalAddGroup F₄] [ContinuousConstSMul ℝ F₄] {k l : ℕ} (nu : F₃ →L[ℝ] F₄) (mu : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hmu : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (mu x) y)) (phi : E [⋀^Fin k]→L[ℝ] F₁) (psi : E [⋀^Fin l]→L[ℝ] F₂) : pairedWedge (ContinuousLinearMap.postcomp F₂ nu ∘SL mu) ⋯ phi psi = nu.compContinuousAlternatingMap (pairedWedge mu hmu phi psi)

Postcomposing the pairing postcomposes the paired wedge.

@[simp]

theorem ContinuousAlternatingMap.pairedWedge_add_pairing {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] {k l : ℕ} (mu nu : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hmu : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (mu x) y)) (hnu : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (nu x) y)) (phi : E [⋀^Fin k]→L[ℝ] F₁) (psi : E [⋀^Fin l]→L[ℝ] F₂) : pairedWedge (mu + nu) ⋯ phi psi = pairedWedge mu hmu phi psi + pairedWedge nu hnu phi psi

The paired wedge is additive in the pairing.

@[simp]

theorem ContinuousAlternatingMap.pairedWedge_smul_pairing {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] {k l : ℕ} (c : ℝ) (mu : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hmu : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (mu x) y)) (phi : E [⋀^Fin k]→L[ℝ] F₁) (psi : E [⋀^Fin l]→L[ℝ] F₂) : pairedWedge (c • mu) ⋯ phi psi = c • pairedWedge mu hmu phi psi

The paired wedge respects scalar multiplication of the pairing.

@[simp]

theorem ContinuousAlternatingMap.pairedWedge_neg_pairing {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] {k l : ℕ} (mu : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hmu : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (mu x) y)) (phi : E [⋀^Fin k]→L[ℝ] F₁) (psi : E [⋀^Fin l]→L[ℝ] F₂) : pairedWedge (-mu) ⋯ phi psi = -pairedWedge mu hmu phi psi

Negating the pairing negates the paired wedge.

@[simp]

theorem ContinuousAlternatingMap.pairedWedge_zero_pairing {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] {k l : ℕ} (phi : E [⋀^Fin k]→L[ℝ] F₁) (psi : E [⋀^Fin l]→L[ℝ] F₂) : pairedWedge 0 ⋯ phi psi = 0

The paired wedge for the zero pairing is zero.

@[simp]

theorem ContinuousAlternatingMap.pairedWedge_zero_left {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] {k l : ℕ} (mu : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hmu : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (mu x) y)) (psi : E [⋀^Fin l]→L[ℝ] F₂) : pairedWedge mu hmu 0 psi = 0

Wedge with the zero form on the left is zero.

@[simp]

theorem ContinuousAlternatingMap.pairedWedge_zero_right {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] {k l : ℕ} (mu : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hmu : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (mu x) y)) (phi : E [⋀^Fin k]→L[ℝ] F₁) : pairedWedge mu hmu phi 0 = 0

Wedge with the zero form on the right is zero.

theorem ContinuousAlternatingMap.pairedWedge_flip_of_forall_apply_eq {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] {k l : ℕ} (mu : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hmu : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (mu x) y)) (nu : F₂ →L[ℝ] F₁ →L[ℝ] F₃) (hnu : Continuous (Function.uncurry fun (x : F₂) (y : F₁) => (nu x) y)) (hmunu : ∀ (a : F₁) (b : F₂), (nu b) a = (mu a) b) (phi : E [⋀^Fin k]→L[ℝ] F₁) (psi : E [⋀^Fin l]→L[ℝ] F₂) (v : Fin (k + l) → E) : (pairedWedge mu hmu phi psi) v = (-1) ^ (k * l) • (pairedWedge nu hnu psi phi) (v ∘ Fin.cast ⋯)

The flip identity for two pairings that are each other's transpose: swapping the two forms of a paired wedge swaps the pairing and costs the graded sign (-1) ^ (k * l).

theorem ContinuousAlternatingMap.pairedWedge_flip {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] [IsTopologicalAddGroup F₂] [ContinuousConstSMul ℝ F₂] {k l : ℕ} (mu : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hmu : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (mu x) y)) (phi : E [⋀^Fin k]→L[ℝ] F₁) (psi : E [⋀^Fin l]→L[ℝ] F₂) (v : Fin (k + l) → E) : (pairedWedge mu hmu phi psi) v = (-1) ^ (k * l) • (pairedWedge (mu.pairingFlip hmu) ⋯ psi phi) (v ∘ Fin.cast ⋯)

The flip identity: swapping the two forms of a paired wedge flips the pairing and costs the graded sign (-1) ^ (k * l). This holds for every pairing.

theorem ContinuousAlternatingMap.pairedWedge_anticomm {E : Type u_1} {F₁ : Type u_2} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] [IsTopologicalAddGroup F₁] [ContinuousConstSMul ℝ F₁] {k l : ℕ} {mu : F₁ →L[ℝ] F₁ →L[ℝ] F₃} (hmu : Continuous (Function.uncurry fun (x y : F₁) => (mu x) y)) (hskew : ∀ (a b : F₁), (mu a) b = -(mu b) a) (phi : E [⋀^Fin k]→L[ℝ] F₁) (psi : E [⋀^Fin l]→L[ℝ] F₁) (v : Fin (k + l) → E) : (pairedWedge mu hmu phi psi) v = -((-1) ^ (k * l) • (pairedWedge mu hmu psi phi) (v ∘ Fin.cast ⋯))

Anticommutation of a paired wedge along a skew-symmetric pairing.

theorem ContinuousAlternatingMap.pairedWedge_comm {E : Type u_1} {F₁ : Type u_2} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] {k l : ℕ} {mu : F₁ →L[ℝ] F₁ →L[ℝ] F₃} (hmu : Continuous (Function.uncurry fun (x y : F₁) => (mu x) y)) (hsymm : ∀ (a b : F₁), (mu a) b = (mu b) a) (phi : E [⋀^Fin k]→L[ℝ] F₁) (psi : E [⋀^Fin l]→L[ℝ] F₁) (v : Fin (k + l) → E) : (pairedWedge mu hmu phi psi) v = (-1) ^ (k * l) • (pairedWedge mu hmu psi phi) (v ∘ Fin.cast ⋯)

Graded commutativity of the paired wedge along a symmetric pairing.

@[simp]

theorem ContinuousAlternatingMap.pairedWedge_apply_zero_left {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] [IsTopologicalAddGroup F₂] [ContinuousConstSMul ℝ F₂] {l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hμ : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (μ x) y)) (φ : E [⋀^Fin 0]→L[ℝ] F₁) (ψ : E [⋀^Fin l]→L[ℝ] F₂) (v : Fin (0 + l) → E) : (pairedWedge μ hμ φ ψ) v = (μ (φ 0)) (ψ (v ∘ Fin.cast ⋯))

Wedge with a degree-zero form on the left pairs its value on the empty tuple with the other form.

theorem ContinuousAlternatingMap.pairedWedge_apply_eq_zero_of_forall {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] {l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hμ : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (μ x) y)) (α : E [⋀^Fin 1]→L[ℝ] F₁) (ψ : E [⋀^Fin l]→L[ℝ] F₂) (w : Fin (1 + l) → E) (hw : ∀ (i : Fin (1 + l)), α ![w i] = 0) : (pairedWedge μ hμ α ψ) w = 0

A wedge α ∧ ψ with a one-form α vanishes on every tuple of vectors that α kills.

theorem ContinuousAlternatingMap.curryLeftTopological_pairedWedge {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] {k l : ℕ} [ContinuousAdd F₁] [ContinuousConstSMul ℝ F₁] [ContinuousAdd F₂] [ContinuousConstSMul ℝ F₂] (mu : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hmu : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (mu x) y)) (phi : E [⋀^Fin (k + 1)]→L[ℝ] F₁) (psi : E [⋀^Fin (l + 1)]→L[ℝ] F₂) (v : E) (w : Fin (k + 1 + l) → E) : ((pairedWedge mu hmu phi psi).curryLeftTopological v) w = (pairedWedge mu hmu (phi.curryLeftTopological v) psi) (w ∘ Fin.cast ⋯) + (-1) ^ (k + 1) • (pairedWedge mu hmu phi (psi.curryLeftTopological v)) w

The interior product is an antiderivation of degree -1 for the paired wedge: ι_v (φ ∧ ψ) = ι_v φ ∧ ψ + (-1) ^ (k + 1) • φ ∧ ι_v ψ for a (k + 1)-form φ. This is the topological counterpart of ContinuousAlternatingMap.curryLeft_pairedWedge and the formula of Lee, Introduction to Smooth Manifolds, 2nd ed., Lemma 14.13.

theorem ContinuousAlternatingMap.pairedWedge_apply_vecCons_of_forall {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [AddCommGroup F₂] [Module ℝ F₂] [TopologicalSpace F₂] [AddCommGroup F₃] [Module ℝ F₃] [TopologicalSpace F₃] [IsTopologicalAddGroup F₃] [ContinuousConstSMul ℝ F₃] {l : ℕ} [ContinuousAdd F₁] [ContinuousConstSMul ℝ F₁] [IsTopologicalAddGroup F₂] [ContinuousConstSMul ℝ F₂] (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hμ : Continuous (Function.uncurry fun (x : F₁) (y : F₂) => (μ x) y)) (α : E [⋀^Fin 1]→L[ℝ] F₁) (ψ : E [⋀^Fin l]→L[ℝ] F₂) (u : E) (w : Fin l → E) (hw : ∀ (i : Fin l), α ![w i] = 0) : (pairedWedge μ hμ α ψ) (Matrix.vecCons u w ∘ Fin.cast ⋯) = (μ (α ![u])) (ψ w)

Expanding a wedge α ∧ ψ with a one-form α along its first argument u: when α kills the remaining arguments w, the wedge is μ (α u) (ψ w).