Documentation

TauCeti.Geometry.Manifold.DifferentialForm.Wedge.Leibniz

The Leibniz rule for wedge products of differential forms #

For fixed-coefficient forms φ of degree k and ψ, and a fixed continuous bilinear pairing μ of their coefficient spaces, the manifold exterior derivative satisfies

d (φ ∧ ψ) = dφ ∧ ψ + (-1) ^ k • φ ∧ dψ.

The coordinate expression of a paired wedge in a chart is the paired wedge of the coordinate expressions, so the rule follows from the flat Leibniz rule TauCeti.extDerivWithin_pairedWedge. The within-set statement only needs differentiability of both forms at the point and unique derivatives there, so it applies at boundary and corner points. The degrees k + 1 + l and k + (l + 1) of the two terms are identified with k + l + 1 by Fin.cast. The real wedge TauCeti.RoughForm.wedge is the specialization to multiplication.

With this rule the wedge product descends to closed and exact forms, which is what makes de Rham cohomology a ring.

References #

source
@[simp]
theorem TauCeti.RoughForm.inChartAt_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] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (φ : RoughForm I M F₁ k) (ψ : RoughForm I M F₂ l) (x₀ : M) (z : E) :
(wedgeWith μ φ ψ).inChartAt x₀ z = ContinuousAlternatingMap.pairedWedge μ ⋯ (φ.inChartAt x₀ z) (ψ.inChartAt x₀ z)

The coordinate expression of a paired wedge is the paired wedge of the coordinate expressions.

source
theorem TauCeti.mextDerivWithin_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] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k l : ℕ} {s : Set M} {x : M} [IsManifold I 1 M] (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) {φ : RoughForm I M F₁ k} {ψ : RoughForm I M F₂ l} (hφ : (MDiffAt[s] fun (y : M) => ⟨y, φ y⟩) x) (hψ : (MDiffAt[s] fun (y : M) => ⟨y, ψ y⟩) x) (hs : UniqueMDiffAt[s] x) (v : Fin (k + l + 1) → TangentSpace I x) :
(mextDerivWithin (RoughForm.wedgeWith μ φ ψ) s x) v = (RoughForm.wedgeWith μ (mextDerivWithin φ s) ψ x) (v ∘ Fin.cast ⋯) + (-1) ^ k • (RoughForm.wedgeWith μ φ (mextDerivWithin ψ 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 μ, at a point of unique differentiability where both forms are differentiable.

source
theorem TauCeti.mextDeriv_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] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k l : ℕ} {x : M} [IsManifold I 1 M] (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) {φ : RoughForm I M F₁ k} {ψ : RoughForm I M F₂ l} (hφ : (MDiffAt fun (y : M) => ⟨y, φ y⟩) x) (hψ : (MDiffAt fun (y : M) => ⟨y, ψ y⟩) x) (v : Fin (k + l + 1) → TangentSpace I x) :
(mextDeriv (RoughForm.wedgeWith μ φ ψ) x) v = (RoughForm.wedgeWith μ (mextDeriv φ) ψ x) (v ∘ Fin.cast ⋯) + (-1) ^ k • (RoughForm.wedgeWith μ φ (mextDeriv ψ) 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 μ, at a point where both forms are differentiable.

source
theorem TauCeti.mextDerivWithin_wedge {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {k l : ℕ} {s : Set M} {x : M} [IsManifold I 1 M] {φ : RoughForm I M ℝ k} {ψ : RoughForm I M ℝ l} (hφ : (MDiffAt[s] fun (y : M) => ⟨y, φ y⟩) x) (hψ : (MDiffAt[s] fun (y : M) => ⟨y, ψ y⟩) x) (hs : UniqueMDiffAt[s] x) (v : Fin (k + l + 1) → TangentSpace I x) :
(mextDerivWithin (φ.wedge ψ) s x) v = (RoughForm.wedge (mextDerivWithin φ s) ψ x) (v ∘ Fin.cast ⋯) + (-1) ^ k • (φ.wedge (mextDerivWithin ψ s) x) (v ∘ Fin.cast ⋯)

The Leibniz rule for the exterior derivative of the real wedge within a set: d (φ ∧ ψ) = dφ ∧ ψ + (-1) ^ k • φ ∧ dψ for a real k-form φ.

source
theorem TauCeti.mextDeriv_wedge {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {k l : ℕ} {x : M} [IsManifold I 1 M] {φ : RoughForm I M ℝ k} {ψ : RoughForm I M ℝ l} (hφ : (MDiffAt fun (y : M) => ⟨y, φ y⟩) x) (hψ : (MDiffAt fun (y : M) => ⟨y, ψ y⟩) x) (v : Fin (k + l + 1) → TangentSpace I x) :
(mextDeriv (φ.wedge ψ) x) v = ((mextDeriv φ).wedge ψ x) (v ∘ Fin.cast ⋯) + (-1) ^ k • (φ.wedge (mextDeriv ψ) x) (v ∘ Fin.cast ⋯)

The Leibniz rule for the exterior derivative of the real wedge: d (φ ∧ ψ) = dφ ∧ ψ + (-1) ^ k • φ ∧ dψ for a real k-form φ.

source
theorem TauCeti.mextDeriv_fun_smul {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {l : ℕ} {x : M} [IsManifold I 1 M] {f : M → ℝ} {φ : RoughForm I M ℝ l} (hf : MDiffAt f x) (hφ : (MDiffAt fun (y : M) => ⟨y, φ y⟩) x) (v : Fin (l + 1) → TangentSpace I x) :
(mextDeriv (fun (y : M) => f y • φ y) x) v = ((mextDeriv (RoughForm.ofFunction I f)).wedge φ x) (v ∘ Fin.cast ⋯) + f x * (mextDeriv φ x) v

The Leibniz rule for a function times a form: d (f φ) = df ∧ φ + f dφ, at a point where f and φ are differentiable. The degree 0 + 1 + l of df ∧ φ is identified with l + 1 by Fin.cast.

source
theorem TauCeti.mextDeriv_fun_smul_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {x : M} [IsManifold I 1 M] {f : M → ℝ} {α : RoughForm I M ℝ 1} (hf : MDiffAt f x) (hα : (MDiffAt fun (y : M) => ⟨y, α y⟩) x) (v w : TangentSpace I x) :
(mextDeriv (fun (y : M) => f y • α y) x) ![v, w] = (d% f x) v * (α x) ![w] - (d% f x) w * (α x) ![v] + f x * (mextDeriv α x) ![v, w]

The Leibniz rule for a function times a one-form: d (f α) = df ∧ α + f dα, evaluated on a pair of tangent vectors, at a point where f and α are differentiable.

Smooth-form interface #

source
theorem TauCeti.SmoothForm.mextDeriv_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] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k l : ℕ} [IsManifold I 1 M] (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (φ : SmoothForm I M F₁ k) (ψ : SmoothForm I M F₂ l) (x : M) (v : Fin (k + l + 1) → TangentSpace I x) :
(mextDeriv (RoughForm.wedgeWith μ ↑φ ↑ψ) x) v = (RoughForm.wedgeWith μ (mextDeriv ↑φ) (↑ψ) x) (v ∘ Fin.cast ⋯) + (-1) ^ k • (RoughForm.wedgeWith μ (↑φ) (mextDeriv ↑ψ) x) (v ∘ Fin.cast ⋯)

The exterior derivative of a paired wedge of smooth forms, evaluated on tangent vectors.

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

The exterior derivative of the real wedge RoughForm.wedge of the underlying forms of two smooth forms, evaluated on tangent vectors. See SmoothForm.mextDerivₗ_wedge for the bundled law.

source
theorem TauCeti.SmoothForm.mextDerivₗ_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] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k l : ℕ} [IsManifold I 1 M] [IsManifold I 2 M] (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (φ : SmoothForm I M F₁ k) (ψ : SmoothForm I M F₂ l) :
(mextDerivₗ I (k + l)) (((wedgeWith μ) φ) ψ) = (LinearEquiv.cast ⋯) (((wedgeWith μ) ((mextDerivₗ I k) φ)) ψ) + (-1) ^ k • (LinearEquiv.cast ⋯) (((wedgeWith μ) φ) ((mextDerivₗ I l) ψ))

The bundled exterior derivative of a paired wedge of smooth forms. The two terms on the right are transported across the degree associativity equalities.

source
theorem TauCeti.SmoothForm.mextDerivₗ_wedge {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {k l : ℕ} [IsManifold I 1 M] [IsManifold I 2 M] (φ : SmoothForm I M ℝ k) (ψ : SmoothForm I M ℝ l) :
(mextDerivₗ I (k + l)) ((wedge φ) ψ) = (LinearEquiv.cast ⋯) ((wedge ((mextDerivₗ I k) φ)) ψ) + (-1) ^ k • (LinearEquiv.cast ⋯) ((wedge φ) ((mextDerivₗ I l) ψ))

The bundled exterior derivative of the real wedge of smooth forms.