Alternatization and interior products

For a continuous linear map f : E →L[𝕜] E [⋀^Fin (n + 1)]→L[𝕜] F and a vector y, the two ways of combining the alternatization ContinuousAlternatingMap.alternatizeUncurryFin with the interior product ι_y = ContinuousAlternatingMap.curryLeft · y add up to evaluation at y:

alternatizeUncurryFin (ι_y ∘ f) + ι_y (alternatizeUncurryFin f) = f y.

Applied to the derivative f = Dω(x) of a differential form, this is the pointwise form of Cartan's formula d ι_y + ι_y d = L_y for the constant vector field y. It is the algebraic identity behind the homotopy formula of the Poincaré lemma.

Up to the factor n!, alternatizeUncurryFin f is also the signed sum over all permutations of the uncurried map v ↦ f (v 0) (Fin.tail v). This expresses it as an alternatization and lets it be combined with other permutation sums, such as those defining wedge products.

Main declarations

• ContinuousAlternatingMap.alternatizeUncurryFin_neg, ContinuousAlternatingMap.alternatizeUncurryFin_sub: alternatization commutes with negation and subtraction, complementing Mathlib's alternatizeUncurryFin_add.
• ContinuousAlternatingMap.alternatizeUncurryFin_curryLeft_comp_add_curryLeft: the identity above.
• ContinuousAlternatingMap.alternatizeUncurryFin_compContinuousLinearMap: alternatization commutes with pullback along a continuous linear map.
• ContinuousAlternatingMap.factorial_smul_alternatizeUncurryFin_apply: the permutation-sum formula.
• ContinuousAlternatingMap.alternatizeUncurryFin_apply_eq_inv_factorial_smul_sum: the same formula normalized by n!, in characteristic zero.

@[simp]

theorem ContinuousAlternatingMap.alternatizeUncurryFin_neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) : alternatizeUncurryFin (-f) = -alternatizeUncurryFin f

Alternatization commutes with negation.

@[simp]

theorem ContinuousAlternatingMap.alternatizeUncurryFin_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (f g : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) : alternatizeUncurryFin (f - g) = alternatizeUncurryFin f - alternatizeUncurryFin g

Alternatization commutes with subtraction.

theorem ContinuousAlternatingMap.alternatizeUncurryFin_curryLeft_comp_add_curryLeft {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (f : E →L[𝕜] E [⋀^Fin (n + 1)]→L[𝕜] F) (y : E) : alternatizeUncurryFin (curryLeftLI.toContinuousLinearMap.flip y ∘SL f) + (alternatizeUncurryFin f).curryLeft y = f y

Alternatizing the interior product with y of a family of forms, plus the interior product with y of its alternatization, is evaluation of the family at y. This is the pointwise constant-coefficient case of Cartan's formula d ι_y + ι_y d = L_y.

theorem ContinuousAlternatingMap.alternatizeUncurryFin_compContinuousLinearMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) (L : E' →L[𝕜] E) : (alternatizeUncurryFin f).compContinuousLinearMap L = alternatizeUncurryFin (compContinuousLinearMapCLM L ∘SL f ∘SL L)

Alternatization commutes with pullback along a continuous linear map L: pulling back the alternatization of f is alternatizing f with its argument and its values pulled back. Applied to the derivative of a differential form, this is the pointwise linear case of the naturality of the exterior derivative.

theorem ContinuousAlternatingMap.factorial_smul_alternatizeUncurryFin_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) (v : Fin (n + 1) → E) : n.factorial • (alternatizeUncurryFin f) v = ∑ σ : Equiv.Perm (Fin (n + 1)), Equiv.Perm.sign σ • (f (v (σ 0))) fun (i : Fin n) => v (σ i.succ)

Up to the factor n!, the alternatization of a linear family of n-forms is the signed sum over all permutations of the uncurried map: the entry moved to the first slot is fed to f, and the remaining entries to the resulting form.

theorem ContinuousAlternatingMap.alternatizeUncurryFin_apply_eq_inv_factorial_smul_sum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} [CharZero 𝕜] (f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) (v : Fin (n + 1) → E) : (alternatizeUncurryFin f) v = (↑n.factorial)⁻¹ • ∑ σ : Equiv.Perm (Fin (n + 1)), Equiv.Perm.sign σ • (f (v (σ 0))) fun (i : Fin n) => v (σ i.succ)

In characteristic zero, the alternatization of a linear family of n-forms is the signed sum over all permutations of the uncurried map, normalized by n!.

theorem ContinuousAlternatingMap.alternatizeUncurryFin_fderivCompContinuousLinearMap_comp_eq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {J : E →L[𝕜] E} (ω : E [⋀^Fin n]→L[𝕜] F) {A N : E →L[𝕜] E →L[𝕜] E} (hN : ∀ (v w : E), (N v) w = (A (J v)) w + (A v) (J w) - (A (J w)) v - (A w) (J v)) : alternatizeUncurryFin (ω.fderivCompContinuousLinearMap (ContinuousLinearMap.id 𝕜 E) ∘SL N) = alternatizeUncurryFin ((ω.fderivCompContinuousLinearMap (ContinuousLinearMap.id 𝕜 E) ∘SL A) ∘SL J) + alternatizeUncurryFin (ω.fderivCompContinuousLinearMap (ContinuousLinearMap.id 𝕜 E) ∘SL (ContinuousLinearMap.compL 𝕜 E E E).flip J ∘SL A) + (alternatizeUncurryFin ((ω.fderivCompContinuousLinearMap (ContinuousLinearMap.id 𝕜 E) ∘SL A) ∘SL J) + alternatizeUncurryFin (ω.fderivCompContinuousLinearMap (ContinuousLinearMap.id 𝕜 E) ∘SL (ContinuousLinearMap.compL 𝕜 E E E).flip J ∘SL A))

The alternation of D ∘ N, for D the derivative of L ↦ ω.compContinuousLinearMap L at the identity and N the Nijenhuis-type tensor N v w = A (J v) w + A v (J w) - A (J w) v - A w (J v), is twice the alternation of D ∘ S for S v = A (J v) + A v ∘ J; this involves only the families v ↦ D (A (J v)) and v ↦ D (A v ∘L J).