Alternatization of wedges with a linear family of forms

For a continuous linear family f of k-forms, a fixed l-form ψ and a fixed continuous bilinear pairing μ, alternatizing the family v ↦ f v ∧ ψ gives alternatizeUncurryFin f ∧ ψ, and alternatizing v ↦ φ ∧ g v for a fixed k-form φ gives (-1) ^ k • φ ∧ alternatizeUncurryFin g. Applied to the derivatives of two families of forms, these are the two terms of the Leibniz rule d (φ ∧ ψ) = dφ ∧ ψ + (-1) ^ k • φ ∧ dψ for the exterior derivative. The degrees k + 1 + l and k + (l + 1) are identified with k + l + 1 by Fin.cast.

Both sides are expanded as signed sums over permutations. The alternatization of f is itself such a sum (ContinuousAlternatingMap.factorial_smul_alternatizeUncurryFin_apply), and the nested alternatization is absorbed into the outer one (TauCeti.sum_sign_smul_sum_sign_smul_eq_card_nsmul). The wedge normalization follows John M. Lee, Introduction to Smooth Manifolds, second edition, Chapter 14.

Main declarations

• ContinuousAlternatingMap.alternatizeUncurryFin_pairedWedgeCLM_flip_comp_apply: the identity for v ↦ f v ∧ ψ.
• ContinuousAlternatingMap.alternatizeUncurryFin_pairedWedgeCLM_comp_apply: the identity for v ↦ φ ∧ g v.
• ContinuousAlternatingMap.alternatizeUncurryFin_smulRight_apply: alternatizing v ↦ a v • ψ for a covector a gives the wedge a ∧ ψ.

theorem ContinuousAlternatingMap.alternatizeUncurryFin_pairedWedgeCLM_flip_comp_apply {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (f : E →L[ℝ] E [⋀^Fin k]→L[ℝ] F₁) (ψ : E [⋀^Fin l]→L[ℝ] F₂) (v : Fin (k + l + 1) → E) : (alternatizeUncurryFin ((pairedWedgeCLM μ).flip ψ ∘SL f)) v = (pairedWedge μ ⋯ (alternatizeUncurryFin f) ψ) (v ∘ Fin.cast ⋯)

Alternatizing the linear family v ↦ f v ∧ ψ gives the wedge of the alternatization of f with ψ. This is the algebraic identity behind the first term of the Leibniz rule d (φ ∧ ψ) = dφ ∧ ψ + (-1) ^ k • φ ∧ dψ.

theorem ContinuousAlternatingMap.alternatizeUncurryFin_pairedWedgeCLM_comp_apply {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (φ : E [⋀^Fin k]→L[ℝ] F₁) (g : E →L[ℝ] E [⋀^Fin l]→L[ℝ] F₂) (v : Fin (k + l + 1) → E) : (alternatizeUncurryFin ((pairedWedgeCLM μ) φ ∘SL g)) v = (-1) ^ k • (pairedWedge μ ⋯ φ (alternatizeUncurryFin g)) (v ∘ Fin.cast ⋯)

Alternatizing the linear family v ↦ φ ∧ g v gives (-1) ^ k times the wedge of φ with the alternatization of g, for a k-form φ. This is the algebraic identity behind the second term of the Leibniz rule d (φ ∧ ψ) = dφ ∧ ψ + (-1) ^ k • φ ∧ dψ.

theorem ContinuousAlternatingMap.alternatizeUncurryFin_smulRight_apply {E : Type u_1} {F₂ : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] {l : ℕ} (a : E →L[ℝ] ℝ) (ψ : E [⋀^Fin l]→L[ℝ] F₂) (v : Fin (l + 1) → E) : (alternatizeUncurryFin (a.smulRight ψ)) v = (pairedWedge (ContinuousLinearMap.lsmul ℝ ℝ) ⋯ ((ofSubsingleton ℝ E ℝ 0) a) ψ) (v ∘ Fin.cast ⋯)

Alternatizing the linear family v ↦ a v • ψ for a covector a gives the wedge a ∧ ψ of a, regarded as a one-form, with ψ. This identifies the term dc ∧ ω in the Leibniz rule TauCeti.extDerivWithin_function_smul with the paired wedge. The degree 1 + l is identified with l + 1 by Fin.cast.