Regularity of wedge products of differential forms

The paired wedge of two fixed-coefficient forms of class C^n is again of class C^n, for every continuous bilinear pairing of the coefficient spaces. These results specialize the bundle-valued smooth wedge to trivial coefficient bundles and a constant pairing. The constant pairing defines a smooth section of the bundle of bilinear maps.

The relative statements use no derivative, so they hold within arbitrary subsets and at boundary and corner points. In particular smooth forms are closed under the paired wedge, and TauCeti.SmoothForm.wedgeWith and TauCeti.SmoothForm.wedge bundle the product as a bilinear map on smooth forms; these supply the product on de Rham cohomology.

References

• John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Chapter 14.

theorem ContMDiffWithinAt.wedgeWith_form {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} {F₃ : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] [IsManifold I 1 M] {k l : ℕ} {n : WithTop ℕ∞} {s : Set M} {x : M} {φ : TauCeti.RoughForm I M F₁ k} {ψ : TauCeti.RoughForm I M F₂ l} (hφ : ContMDiffWithinAt I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin k]→L[ℝ] F₁))) n (fun (y : M) => ⟨y, φ y⟩) s x) (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hψ : ContMDiffWithinAt I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin l]→L[ℝ] F₂))) n (fun (y : M) => ⟨y, ψ y⟩) s x) : ContMDiffWithinAt I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin (k + l)]→L[ℝ] F₃))) n (fun (y : M) => ⟨y, TauCeti.RoughForm.wedgeWith μ φ ψ y⟩) s x

The paired wedge of two C^n sections of the alternating bundle is a C^n section, within an arbitrary subset.

theorem ContMDiffOn.wedgeWith_form {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} {F₃ : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] [IsManifold I 1 M] {k l : ℕ} {n : WithTop ℕ∞} {s : Set M} {φ : TauCeti.RoughForm I M F₁ k} {ψ : TauCeti.RoughForm I M F₂ l} (hφ : ContMDiffOn I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin k]→L[ℝ] F₁))) n (fun (y : M) => ⟨y, φ y⟩) s) (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hψ : ContMDiffOn I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin l]→L[ℝ] F₂))) n (fun (y : M) => ⟨y, ψ y⟩) s) : ContMDiffOn I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin (k + l)]→L[ℝ] F₃))) n (fun (y : M) => ⟨y, TauCeti.RoughForm.wedgeWith μ φ ψ y⟩) s

The paired wedge of two C^n sections of the alternating bundle is a C^n section on an arbitrary subset.

theorem ContMDiffAt.wedgeWith_form {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} {F₃ : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] [IsManifold I 1 M] {k l : ℕ} {n : WithTop ℕ∞} {x : M} {φ : TauCeti.RoughForm I M F₁ k} {ψ : TauCeti.RoughForm I M F₂ l} (hφ : ContMDiffAt I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin k]→L[ℝ] F₁))) n (fun (y : M) => ⟨y, φ y⟩) x) (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (hψ : ContMDiffAt I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin l]→L[ℝ] F₂))) n (fun (y : M) => ⟨y, ψ y⟩) x) : ContMDiffAt I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin (k + l)]→L[ℝ] F₃))) n (fun (y : M) => ⟨y, TauCeti.RoughForm.wedgeWith μ φ ψ y⟩) x

The paired wedge of two sections of the alternating bundle that are C^n at a point is C^n at that point.

theorem TauCeti.IsSmoothForm.wedgeWith {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} {F₃ : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] [IsManifold I 1 M] {k l : ℕ} {n : WithTop ℕ∞} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) {φ : RoughForm I M F₁ k} {ψ : RoughForm I M F₂ l} (hφ : IsSmoothForm I n φ) (hψ : IsSmoothForm I n ψ) : IsSmoothForm I n (RoughForm.wedgeWith μ φ ψ)

The paired wedge of two fixed-coefficient forms of class C^n is of class C^n.

theorem TauCeti.IsSmoothForm.wedge {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {k l : ℕ} {n : WithTop ℕ∞} {φ : RoughForm I M ℝ k} {ψ : RoughForm I M ℝ l} (hφ : IsSmoothForm I n φ) (hψ : IsSmoothForm I n ψ) : IsSmoothForm I n (φ.wedge ψ)

The real wedge of two real-valued forms of class C^n is of class C^n.

theorem TauCeti.smoothForms_wedgeWith_mem {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} {F₃ : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] [IsManifold I 1 M] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (φ : SmoothForm I M F₁ k) (ψ : SmoothForm I M F₂ l) : RoughForm.wedgeWith μ ↑φ ↑ψ ∈ smoothBundleForms I F₃ (Bundle.Trivial M F₃) (k + l)

Smooth fixed-coefficient forms are closed under the paired wedge, for every continuous bilinear pairing of the coefficient spaces.

theorem TauCeti.smoothForms_wedge_mem {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {k l : ℕ} (φ : SmoothForm I M ℝ k) (ψ : SmoothForm I M ℝ l) : RoughForm.wedge ↑φ ↑ψ ∈ smoothBundleForms I ℝ (Bundle.Trivial M ℝ) (k + l)

Smooth real-valued forms are closed under the real wedge.

noncomputable def TauCeti.SmoothForm.wedgeWith {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} {F₃ : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] [IsManifold I 1 M] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) : SmoothForm I M F₁ k →ₗ[ℝ] SmoothForm I M F₂ l →ₗ[ℝ] SmoothForm I M F₃ (k + l)

The paired wedge of smooth fixed-coefficient forms, as a bilinear map.

@[simp]

theorem TauCeti.SmoothForm.coe_wedgeWith {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} {F₃ : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] [IsManifold I 1 M] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (φ : SmoothForm I M F₁ k) (ψ : SmoothForm I M F₂ l) : ↑(((wedgeWith μ) φ) ψ) = RoughForm.wedgeWith μ ↑φ ↑ψ

The underlying rough form of the smooth paired wedge is the rough paired wedge.

theorem TauCeti.SmoothForm.wedgeWith_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} {F₃ : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] [IsManifold I 1 M] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (φ : SmoothForm I M F₁ k) (ψ : SmoothForm I M F₂ l) (x : M) (v : Fin (k + l) → TangentSpace I x) : (↑(((wedgeWith μ) φ) ψ) x) v = (↑k.factorial * ↑l.factorial)⁻¹ • ∑ σ : Equiv.Perm (Fin (k + l)), Equiv.Perm.sign σ • (μ ((↑φ x) fun (i : Fin k) => v (σ (Fin.castAdd l i)))) ((↑ψ x) fun (j : Fin l) => v (σ (Fin.natAdd k j)))

Evaluation of the smooth fixed-coefficient paired wedge.

@[simp]

theorem TauCeti.SmoothForm.wedgeWith_apply_zero_right {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} {F₃ : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] [IsManifold I 1 M] {k : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (φ : SmoothForm I M F₁ k) (ψ : SmoothForm I M F₂ 0) (x : M) (v : Fin k → TangentSpace I x) : (↑(((wedgeWith μ) φ) ψ) x) v = (μ ((↑φ x) v)) ((↑ψ x) 0)

Pairing a smooth form with a degree-zero form pairs its value with the function value.

theorem TauCeti.SmoothForm.wedgeWith_apply_one_one {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} {F₃ : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] [IsManifold I 1 M] (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (φ : SmoothForm I M F₁ 1) (ψ : SmoothForm I M F₂ 1) (x : M) (v w : TangentSpace I x) : (↑(((wedgeWith μ) φ) ψ) x) ![v, w] = (μ ((↑φ x) ![v])) ((↑ψ x) ![w]) - (μ ((↑φ x) ![w])) ((↑ψ x) ![v])

Evaluation of the smooth paired wedge on two one-forms.

noncomputable def TauCeti.SmoothForm.wedge {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {k l : ℕ} : SmoothForm I M ℝ k →ₗ[ℝ] SmoothForm I M ℝ l →ₗ[ℝ] SmoothForm I M ℝ (k + l)

The real wedge of smooth real-valued forms, as a bilinear map.

theorem TauCeti.SmoothForm.wedge_def {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {k l : ℕ} (φ : SmoothForm I M ℝ k) (ψ : SmoothForm I M ℝ l) : (wedge φ) ψ = ((wedgeWith (ContinuousLinearMap.mul ℝ ℝ)) φ) ψ

The smooth real wedge specializes the paired wedge to multiplication.

@[simp]

theorem TauCeti.SmoothForm.coe_wedge {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {k l : ℕ} (φ : SmoothForm I M ℝ k) (ψ : SmoothForm I M ℝ l) : ↑((wedge φ) ψ) = RoughForm.wedge ↑φ ↑ψ

The underlying rough form of the smooth real wedge is the rough real wedge.

theorem TauCeti.SmoothForm.wedge_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {k l : ℕ} (φ : SmoothForm I M ℝ k) (ψ : SmoothForm I M ℝ l) (x : M) (v : Fin (k + l) → TangentSpace I x) : (↑((wedge φ) ψ) x) v = (↑k.factorial * ↑l.factorial)⁻¹ • ∑ σ : Equiv.Perm (Fin (k + l)), Equiv.Perm.sign σ • (((↑φ x) fun (i : Fin k) => v (σ (Fin.castAdd l i))) * (↑ψ x) fun (j : Fin l) => v (σ (Fin.natAdd k j)))

Evaluation of the smooth real-valued wedge in every degree.

@[simp]

theorem TauCeti.SmoothForm.wedge_apply_zero_right {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {k : ℕ} (φ : SmoothForm I M ℝ k) (ψ : SmoothForm I M ℝ 0) (x : M) (v : Fin k → TangentSpace I x) : (↑((wedge φ) ψ) x) v = (↑φ x) v * (↑ψ x) 0

Wedging a smooth real-valued form with a degree-zero form multiplies its value by the function value.

theorem TauCeti.SmoothForm.wedge_apply_one_one {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ ψ : SmoothForm I M ℝ 1) (x : M) (v w : TangentSpace I x) : (↑((wedge φ) ψ) x) ![v, w] = (↑φ x) ![v] * (↑ψ x) ![w] - (↑φ x) ![w] * (↑ψ x) ![v]

The smooth real-valued wedge of two one-forms evaluates as a determinant.

theorem TauCeti.SmoothForm.eval₂_wedge_one_one {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ ψ : SmoothForm I M ℝ 1) (x : M) (v w : TangentSpace I x) : SmoothBundleForm.eval₂ ((wedge φ) ψ) x v w = (↑φ x) ![v] * (↑ψ x) ![w] - (↑φ x) ![w] * (↑ψ x) ![v]

The smooth real-valued wedge of two one-forms, evaluated on an ordered pair of tangent vectors, is a determinant.

theorem TauCeti.SmoothForm.wedgeWith_flip {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} {F₃ : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] [IsManifold I 1 M] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (φ : SmoothForm I M F₁ k) (ψ : SmoothForm I M F₂ l) (x : M) (v : Fin (k + l) → TangentSpace I x) : (↑(((wedgeWith μ) φ) ψ) x) v = (-1) ^ (k * l) • (↑(((wedgeWith μ.flip) ψ) φ) x) (v ∘ Fin.cast ⋯)

Swapping smooth paired forms flips the coefficient pairing and contributes the graded sign.

theorem TauCeti.SmoothForm.wedgeWith_comm {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_4} {F₃ : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] [IsManifold I 1 M] {k l : ℕ} (μ : F₁ →L[ℝ] F₁ →L[ℝ] F₃) (hμ : ∀ (a b : F₁), (μ a) b = (μ b) a) (φ : SmoothForm I M F₁ k) (ψ : SmoothForm I M F₁ l) (x : M) (v : Fin (k + l) → TangentSpace I x) : (↑(((wedgeWith μ) φ) ψ) x) v = (-1) ^ (k * l) • (↑(((wedgeWith μ) ψ) φ) x) (v ∘ Fin.cast ⋯)

A symmetric coefficient pairing makes the smooth paired wedge graded-commutative.

theorem TauCeti.SmoothForm.wedge_comm {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {k l : ℕ} (φ : SmoothForm I M ℝ k) (ψ : SmoothForm I M ℝ l) (x : M) (v : Fin (k + l) → TangentSpace I x) : (↑((wedge φ) ψ) x) v = (-1) ^ (k * l) • (↑((wedge ψ) φ) x) (v ∘ Fin.cast ⋯)

Real-valued smooth forms commute with the usual graded sign.