Smoothness and differentiation of paired wedges #
Families of alternating maps can be wedged without loss of regularity. The pairing itself may vary: differentiating the paired wedge gives three terms, one for each input. For a fixed pairing the first term vanishes. The relative statements apply to arbitrary sets, including chart ranges of manifolds with boundary or corners.
For a fixed pairing, alternatizing this derivative gives the Leibniz rule for the exterior
derivative, d (φ ∧ ψ) = dφ ∧ ψ + (-1) ^ k • φ ∧ dψ for a k-form φ
(TauCeti.extDerivWithin_pairedWedge).
The construction uses ContinuousAlternatingMap.pairedWedgeCLM and Mathlib's calculus of
application of continuous linear maps; ContDiff.wedge specializes the regularity statement to
the real wedge of real-valued forms. A paired wedge with a compactly supported second factor is
compactly supported (HasCompactSupport.pairedWedge_left, HasCompactSupport.wedge_left).
These results provide the coefficient calculus for wedge products of smooth bundle-valued forms.
The wedge normalization follows John M. Lee, Introduction to Smooth Manifolds, second edition,
Chapter 14.
theorem
ContDiffWithinAt.pairedWedge
{X : Type u_1}
{E : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{F₃ : Type u_5}
[NormedAddCommGroup X]
[NormedSpace ℝ X]
[SeminormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[NormedAddCommGroup F₃]
[NormedSpace ℝ F₃]
{k l : ℕ}
{n : WithTop ℕ∞}
{s : Set X}
{x : X}
{μ : X → F₁ →L[ℝ] F₂ →L[ℝ] F₃}
{φ : X → E [⋀^Fin k]→L[ℝ] F₁}
{ψ : X → E [⋀^Fin l]→L[ℝ] F₂}
(hμ : ContDiffWithinAt ℝ n μ s x)
(hφ : ContDiffWithinAt ℝ n φ s x)
(hψ : ContDiffWithinAt ℝ n ψ s x)
:
ContDiffWithinAt ℝ n (fun (y : X) => ContinuousAlternatingMap.pairedWedge (μ y) ⋯ (φ y) (ψ y)) s x
The paired wedge of C^n families and a C^n pairing is C^n within a set at a point.
theorem
ContDiffOn.pairedWedge
{X : Type u_1}
{E : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{F₃ : Type u_5}
[NormedAddCommGroup X]
[NormedSpace ℝ X]
[SeminormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[NormedAddCommGroup F₃]
[NormedSpace ℝ F₃]
{k l : ℕ}
{n : WithTop ℕ∞}
{s : Set X}
{μ : X → F₁ →L[ℝ] F₂ →L[ℝ] F₃}
{φ : X → E [⋀^Fin k]→L[ℝ] F₁}
{ψ : X → E [⋀^Fin l]→L[ℝ] F₂}
(hμ : ContDiffOn ℝ n μ s)
(hφ : ContDiffOn ℝ n φ s)
(hψ : ContDiffOn ℝ n ψ s)
:
ContDiffOn ℝ n (fun (y : X) => ContinuousAlternatingMap.pairedWedge (μ y) ⋯ (φ y) (ψ y)) s
The paired wedge preserves C^n regularity on an arbitrary set.
theorem
ContDiffAt.pairedWedge
{X : Type u_1}
{E : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{F₃ : Type u_5}
[NormedAddCommGroup X]
[NormedSpace ℝ X]
[SeminormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[NormedAddCommGroup F₃]
[NormedSpace ℝ F₃]
{k l : ℕ}
{n : WithTop ℕ∞}
{x : X}
{μ : X → F₁ →L[ℝ] F₂ →L[ℝ] F₃}
{φ : X → E [⋀^Fin k]→L[ℝ] F₁}
{ψ : X → E [⋀^Fin l]→L[ℝ] F₂}
(hμ : ContDiffAt ℝ n μ x)
(hφ : ContDiffAt ℝ n φ x)
(hψ : ContDiffAt ℝ n ψ x)
:
ContDiffAt ℝ n (fun (y : X) => ContinuousAlternatingMap.pairedWedge (μ y) ⋯ (φ y) (ψ y)) x
The paired wedge preserves C^n regularity at a point.
theorem
ContDiff.pairedWedge
{X : Type u_1}
{E : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{F₃ : Type u_5}
[NormedAddCommGroup X]
[NormedSpace ℝ X]
[SeminormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[NormedAddCommGroup F₃]
[NormedSpace ℝ F₃]
{k l : ℕ}
{n : WithTop ℕ∞}
{μ : X → F₁ →L[ℝ] F₂ →L[ℝ] F₃}
{φ : X → E [⋀^Fin k]→L[ℝ] F₁}
{ψ : X → E [⋀^Fin l]→L[ℝ] F₂}
(hμ : ContDiff ℝ n μ)
(hφ : ContDiff ℝ n φ)
(hψ : ContDiff ℝ n ψ)
:
ContDiff ℝ n fun (y : X) => ContinuousAlternatingMap.pairedWedge (μ y) ⋯ (φ y) (ψ y)
The paired wedge of C^n families and a C^n pairing is C^n.
theorem
ContDiff.wedge
{X : Type u_1}
{E : Type u_2}
[NormedAddCommGroup X]
[NormedSpace ℝ X]
[SeminormedAddCommGroup E]
[NormedSpace ℝ E]
{k l : ℕ}
{n : WithTop ℕ∞}
{φ : X → E [⋀^Fin k]→L[ℝ] ℝ}
{ψ : X → E [⋀^Fin l]→L[ℝ] ℝ}
(hφ : ContDiff ℝ n φ)
(hψ : ContDiff ℝ n ψ)
:
The real wedge of C^n families of real-valued forms is C^n.
theorem
HasCompactSupport.pairedWedge_left
{X : Type u_1}
{E : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{F₃ : Type u_5}
[NormedAddCommGroup X]
[SeminormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[NormedAddCommGroup F₃]
[NormedSpace ℝ F₃]
{k l : ℕ}
{μ : X → F₁ →L[ℝ] F₂ →L[ℝ] F₃}
{φ : X → E [⋀^Fin k]→L[ℝ] F₁}
{ψ : X → E [⋀^Fin l]→L[ℝ] F₂}
(hψ : HasCompactSupport ψ)
:
HasCompactSupport fun (y : X) => ContinuousAlternatingMap.pairedWedge (μ y) ⋯ (φ y) (ψ y)
The paired wedge of a family of forms with a compactly supported family is compactly
supported, as for HasCompactSupport.mul_left.
theorem
HasCompactSupport.wedge_left
{X : Type u_1}
{E : Type u_2}
[NormedAddCommGroup X]
[SeminormedAddCommGroup E]
[NormedSpace ℝ E]
{k l : ℕ}
{φ : X → E [⋀^Fin k]→L[ℝ] ℝ}
{ψ : X → E [⋀^Fin l]→L[ℝ] ℝ}
(hψ : HasCompactSupport ψ)
:
HasCompactSupport fun (y : X) => (φ y).wedge (ψ y)
The real wedge of a family of real-valued forms with a compactly supported family is compactly supported.
theorem
DifferentiableWithinAt.pairedWedge
{X : Type u_1}
{E : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{F₃ : Type u_5}
[NormedAddCommGroup X]
[NormedSpace ℝ X]
[SeminormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[NormedAddCommGroup F₃]
[NormedSpace ℝ F₃]
{k l : ℕ}
{s : Set X}
{x : X}
{μ : X → F₁ →L[ℝ] F₂ →L[ℝ] F₃}
{φ : X → E [⋀^Fin k]→L[ℝ] F₁}
{ψ : X → E [⋀^Fin l]→L[ℝ] F₂}
(hμ : DifferentiableWithinAt ℝ μ s x)
(hφ : DifferentiableWithinAt ℝ φ s x)
(hψ : DifferentiableWithinAt ℝ ψ s x)
:
DifferentiableWithinAt ℝ (fun (y : X) => ContinuousAlternatingMap.pairedWedge (μ y) ⋯ (φ y) (ψ y)) s x
The paired wedge of differentiable families is differentiable within a set at a point.
theorem
DifferentiableOn.pairedWedge
{X : Type u_1}
{E : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{F₃ : Type u_5}
[NormedAddCommGroup X]
[NormedSpace ℝ X]
[SeminormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[NormedAddCommGroup F₃]
[NormedSpace ℝ F₃]
{k l : ℕ}
{s : Set X}
{μ : X → F₁ →L[ℝ] F₂ →L[ℝ] F₃}
{φ : X → E [⋀^Fin k]→L[ℝ] F₁}
{ψ : X → E [⋀^Fin l]→L[ℝ] F₂}
(hμ : DifferentiableOn ℝ μ s)
(hφ : DifferentiableOn ℝ φ s)
(hψ : DifferentiableOn ℝ ψ s)
:
DifferentiableOn ℝ (fun (y : X) => ContinuousAlternatingMap.pairedWedge (μ y) ⋯ (φ y) (ψ y)) s
The paired wedge of differentiable families is differentiable on a set.
theorem
DifferentiableAt.pairedWedge
{X : Type u_1}
{E : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{F₃ : Type u_5}
[NormedAddCommGroup X]
[NormedSpace ℝ X]
[SeminormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[NormedAddCommGroup F₃]
[NormedSpace ℝ F₃]
{k l : ℕ}
{x : X}
{μ : X → F₁ →L[ℝ] F₂ →L[ℝ] F₃}
{φ : X → E [⋀^Fin k]→L[ℝ] F₁}
{ψ : X → E [⋀^Fin l]→L[ℝ] F₂}
(hμ : DifferentiableAt ℝ μ x)
(hφ : DifferentiableAt ℝ φ x)
(hψ : DifferentiableAt ℝ ψ x)
:
DifferentiableAt ℝ (fun (y : X) => ContinuousAlternatingMap.pairedWedge (μ y) ⋯ (φ y) (ψ y)) x
The paired wedge of differentiable families is differentiable at a point.
theorem
Differentiable.pairedWedge
{X : Type u_1}
{E : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{F₃ : Type u_5}
[NormedAddCommGroup X]
[NormedSpace ℝ X]
[SeminormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[NormedAddCommGroup F₃]
[NormedSpace ℝ F₃]
{k l : ℕ}
{μ : X → F₁ →L[ℝ] F₂ →L[ℝ] F₃}
{φ : X → E [⋀^Fin k]→L[ℝ] F₁}
{ψ : X → E [⋀^Fin l]→L[ℝ] F₂}
(hμ : Differentiable ℝ μ)
(hφ : Differentiable ℝ φ)
(hψ : Differentiable ℝ ψ)
:
Differentiable ℝ fun (y : X) => ContinuousAlternatingMap.pairedWedge (μ y) ⋯ (φ y) (ψ y)
The paired wedge of differentiable families is differentiable.
theorem
HasFDerivWithinAt.pairedWedge
{X : Type u_1}
{E : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{F₃ : Type u_5}
[NormedAddCommGroup X]
[NormedSpace ℝ X]
[SeminormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[NormedAddCommGroup F₃]
[NormedSpace ℝ F₃]
{k l : ℕ}
{s : Set X}
{x : X}
{μ : X → F₁ →L[ℝ] F₂ →L[ℝ] F₃}
{φ : X → E [⋀^Fin k]→L[ℝ] F₁}
{ψ : X → E [⋀^Fin l]→L[ℝ] F₂}
{μ' : X →L[ℝ] F₁ →L[ℝ] F₂ →L[ℝ] F₃}
{φ' : X →L[ℝ] E [⋀^Fin k]→L[ℝ] F₁}
{ψ' : X →L[ℝ] E [⋀^Fin l]→L[ℝ] F₂}
(hμ : HasFDerivWithinAt μ μ' s x)
(hφ : HasFDerivWithinAt φ φ' s x)
(hψ : HasFDerivWithinAt ψ ψ' s x)
:
HasFDerivWithinAt (fun (y : X) => ContinuousAlternatingMap.pairedWedge (μ y) ⋯ (φ y) (ψ y))
((ContinuousAlternatingMap.pairedWedgeCLM (μ x)) (φ x) ∘SL ψ' + (ContinuousAlternatingMap.pairedWedgeCLM (μ x) ∘SL φ' + (ContinuousAlternatingMap.pairedWedgeCLM ∘SL μ').flip (φ x)).flip
(ψ x))
s x
Derivative witnesses for a pairing and two forms give the three-term derivative of their paired wedge within an arbitrary set.
theorem
HasFDerivAt.pairedWedge
{X : Type u_1}
{E : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{F₃ : Type u_5}
[NormedAddCommGroup X]
[NormedSpace ℝ X]
[SeminormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[NormedAddCommGroup F₃]
[NormedSpace ℝ F₃]
{k l : ℕ}
{x : X}
{μ : X → F₁ →L[ℝ] F₂ →L[ℝ] F₃}
{φ : X → E [⋀^Fin k]→L[ℝ] F₁}
{ψ : X → E [⋀^Fin l]→L[ℝ] F₂}
{μ' : X →L[ℝ] F₁ →L[ℝ] F₂ →L[ℝ] F₃}
{φ' : X →L[ℝ] E [⋀^Fin k]→L[ℝ] F₁}
{ψ' : X →L[ℝ] E [⋀^Fin l]→L[ℝ] F₂}
(hμ : HasFDerivAt μ μ' x)
(hφ : HasFDerivAt φ φ' x)
(hψ : HasFDerivAt ψ ψ' x)
:
HasFDerivAt (fun (y : X) => ContinuousAlternatingMap.pairedWedge (μ y) ⋯ (φ y) (ψ y))
((ContinuousAlternatingMap.pairedWedgeCLM (μ x)) (φ x) ∘SL ψ' + (ContinuousAlternatingMap.pairedWedgeCLM (μ x) ∘SL φ' + (ContinuousAlternatingMap.pairedWedgeCLM ∘SL μ').flip (φ x)).flip
(ψ x))
x
Derivative witnesses for a pairing and two forms give the three-term derivative of their paired wedge at a point.
theorem
TauCeti.fderivWithin_pairedWedge_apply
{X : Type u_1}
{E : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{F₃ : Type u_5}
[NormedAddCommGroup X]
[NormedSpace ℝ X]
[SeminormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[NormedAddCommGroup F₃]
[NormedSpace ℝ F₃]
{k l : ℕ}
{s : Set X}
{x : X}
{μ : X → F₁ →L[ℝ] F₂ →L[ℝ] F₃}
{φ : X → E [⋀^Fin k]→L[ℝ] F₁}
{ψ : X → E [⋀^Fin l]→L[ℝ] F₂}
(hs : UniqueDiffWithinAt ℝ s x)
(hμ : DifferentiableWithinAt ℝ μ s x)
(hφ : DifferentiableWithinAt ℝ φ s x)
(hψ : DifferentiableWithinAt ℝ ψ s x)
(v : X)
:
(fderivWithin ℝ (fun (y : X) => ContinuousAlternatingMap.pairedWedge (μ y) ⋯ (φ y) (ψ y)) s x) v = ContinuousAlternatingMap.pairedWedge ((fderivWithin ℝ μ s x) v) ⋯ (φ x) (ψ x) + ContinuousAlternatingMap.pairedWedge (μ x) ⋯ ((fderivWithin ℝ φ s x) v) (ψ x) + ContinuousAlternatingMap.pairedWedge (μ x) ⋯ (φ x) ((fderivWithin ℝ ψ s x) v)
Differentiating a paired wedge within a unique-differentiability set gives one term for each of the pairing and the two forms.
theorem
TauCeti.fderiv_pairedWedge_apply
{X : Type u_1}
{E : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{F₃ : Type u_5}
[NormedAddCommGroup X]
[NormedSpace ℝ X]
[SeminormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[NormedAddCommGroup F₃]
[NormedSpace ℝ F₃]
{k l : ℕ}
{x : X}
{μ : X → F₁ →L[ℝ] F₂ →L[ℝ] F₃}
{φ : X → E [⋀^Fin k]→L[ℝ] F₁}
{ψ : X → E [⋀^Fin l]→L[ℝ] F₂}
(hμ : DifferentiableAt ℝ μ x)
(hφ : DifferentiableAt ℝ φ x)
(hψ : DifferentiableAt ℝ ψ x)
(v : X)
:
(fderiv ℝ (fun (y : X) => ContinuousAlternatingMap.pairedWedge (μ y) ⋯ (φ y) (ψ y)) x) v = ContinuousAlternatingMap.pairedWedge ((fderiv ℝ μ x) v) ⋯ (φ x) (ψ x) + ContinuousAlternatingMap.pairedWedge (μ x) ⋯ ((fderiv ℝ φ x) v) (ψ x) + ContinuousAlternatingMap.pairedWedge (μ x) ⋯ (φ x) ((fderiv ℝ ψ x) v)
Differentiating a paired wedge gives one term for each of its three inputs.
theorem
TauCeti.extDerivWithin_pairedWedge
{E : Type u_6}
{F₁ : Type u_7}
{F₂ : Type u_8}
{F₃ : Type u_9}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[NormedAddCommGroup F₃]
[NormedSpace ℝ F₃]
{k l : ℕ}
{s : Set E}
{x : E}
{φ : E → E [⋀^Fin k]→L[ℝ] F₁}
{ψ : E → E [⋀^Fin l]→L[ℝ] F₂}
(μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃)
(hs : UniqueDiffWithinAt ℝ s x)
(hφ : DifferentiableWithinAt ℝ φ s x)
(hψ : DifferentiableWithinAt ℝ ψ s x)
(v : Fin (k + l + 1) → E)
:
(extDerivWithin (fun (y : E) => ContinuousAlternatingMap.pairedWedge μ ⋯ (φ y) (ψ y)) s x) v = (ContinuousAlternatingMap.pairedWedge μ ⋯ (extDerivWithin φ s x) (ψ x)) (v ∘ Fin.cast ⋯) + (-1) ^ k • (ContinuousAlternatingMap.pairedWedge μ ⋯ (φ x) (extDerivWithin ψ s x)) (v ∘ Fin.cast ⋯)
The Leibniz rule for the exterior derivative of a paired wedge within a set:
d (φ ∧ ψ) = dφ ∧ ψ + (-1) ^ k • φ ∧ dψ for a k-form φ and a fixed continuous bilinear
pairing. The degrees k + 1 + l and k + (l + 1) are identified with k + l + 1 by Fin.cast.
theorem
TauCeti.extDeriv_pairedWedge
{E : Type u_6}
{F₁ : Type u_7}
{F₂ : Type u_8}
{F₃ : Type u_9}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[NormedAddCommGroup F₃]
[NormedSpace ℝ F₃]
{k l : ℕ}
{x : E}
{φ : E → E [⋀^Fin k]→L[ℝ] F₁}
{ψ : E → E [⋀^Fin l]→L[ℝ] F₂}
(μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃)
(hφ : DifferentiableAt ℝ φ x)
(hψ : DifferentiableAt ℝ ψ x)
(v : Fin (k + l + 1) → E)
:
(extDeriv (fun (y : E) => ContinuousAlternatingMap.pairedWedge μ ⋯ (φ y) (ψ y)) x) v = (ContinuousAlternatingMap.pairedWedge μ ⋯ (extDeriv φ x) (ψ x)) (v ∘ Fin.cast ⋯) + (-1) ^ k • (ContinuousAlternatingMap.pairedWedge μ ⋯ (φ x) (extDeriv ψ x)) (v ∘ Fin.cast ⋯)
The Leibniz rule for the exterior derivative of a paired wedge:
d (φ ∧ ψ) = dφ ∧ ψ + (-1) ^ k • φ ∧ dψ for a k-form φ and a fixed continuous bilinear
pairing.