The Hodge star of an oriented real inner product space

Mathlib's exteriorPower.hodgeStar is built from a bilinear form and a trivialization vol of the top exterior power, and is characterized by B (⋆x) y = vol (x ∧ y). On an oriented real inner product space V of dimension n both inputs are canonical: the bilinear form is the inner product, and the trivialization is the one induced by Mathlib's Orientation.volumeForm, which takes the value 1 on every positively oriented orthonormal basis. This file packages the resulting pointwise Hodge star ⋆ : ⋀ᵏ V ≃ ⋀ˡ V (for k + l = n), so that ⟪⋆x, y⟫ = vol (x ∧ y), equivalently x ∧ y = ⟪⋆x, y⟫ vol.

Its value on the orthonormal basis of ⋀ᵏ V induced by a positively oriented orthonormal basis e of V is the familiar formula: ⋆ e_I = ε(I) e_{Iᶜ}, where e_I is the increasing wedge of the eᵢ with i ∈ I and ε(I) is the sign of the shuffle permutation listing I before its complement. For instance, in an oriented four-dimensional space ⋆(e₁ ∧ e₂) = e₃ ∧ e₄, so the self-dual and anti-self-dual two-forms are the ±1 eigenvectors of ⋆ on ⋀² V. The Hodge star is trace free on a positive middle degree, since Iᶜ ≠ I, so these eigenspaces have equal dimension: three each for two-forms in dimension four.

In dimension four a unit vector s splits a two-form as F = s ∧ a + b, where a = s ⌟ F is the contraction of F by ⟪s, ·⟫ and b has no s-component. Since b ∧ b = 0, the pairing of s ∧ a with F + ⋆F is ‖a‖² + vol (F ∧ F) / 2. On a product S¹ × Y with s = ds, this is the pointwise identity 2 ⟨ds ∧ ι_T F, F⁺⟩ = |ι_T F|² + (F ∧ F) / 2 between the mixed component of a curvature form, its self-dual part and its Chern–Weil density.

Main definitions

• Orientation.volumeEquiv: the trivialization of ⋀ⁿ V induced by Orientation.volumeForm.
• Orientation.hodgeStar: the Hodge star ⋀ᵏ V ≃ ⋀ˡ V of the oriented inner product space.

Main results

• TauCeti.exteriorPower_innerₗ: the bilinear form that the inner product induces on ⋀ᵏ V is the inner product of ⋀ᵏ V.
• Orientation.volumeEquiv_topVector: the volume of the wedge of a positively oriented orthonormal basis is 1.
• Orientation.volumeEquiv_neg_orientation: reversing the orientation negates the volume.
• Orientation.inner_hodgeStar_apply: the characterization ⟪⋆x, y⟫ = vol (x ∧ y).
• Orientation.hodgeStar_basis: the formula ⋆ e_I = ε(I) e_{Iᶜ} on an orthonormal basis.
• Orientation.hodgeStar_hodgeStar: ⋆⋆x = (-1) ^ (k * l) x, and Orientation.hodgeStar_hodgeStar_of_even: ⋆⋆x = x in an even middle degree.
• Orientation.hodgeStar_smul_add_hodgeStar, Orientation.hodgeStar_smul_sub_hodgeStar: in an even middle degree, (x + ⋆x) / 2 is self-dual and (x - ⋆x) / 2 is anti-self-dual.
• Orientation.trace_hodgeStar: in a positive middle degree the Hodge star is trace free, so Orientation.two_mul_finrank_eigenspace_hodgeStar_one and Orientation.two_mul_finrank_eigenspace_hodgeStar_neg_one: in an even positive middle degree the self-dual and anti-self-dual forms each make up half of ⋀ᵏ V. In dimension four, Λ⁺ and Λ⁻ have dimension three.
• Orientation.hodgeStar_coe_of_mem_eigenspace_one: forms in the 1-eigenspace of ⋆ are self-dual, ⋆x = x.
• Orientation.inner_ιMulti_twoVectorContraction_add_hodgeStar: for a unit vector s in dimension four, ⟪s ∧ (s ⌟ F), F + ⋆F⟫ = ‖s ⌟ F‖² + vol (F ∧ F) / 2.

References

• F. W. Warner, Foundations of Differentiable Manifolds and Lie Groups, Graduate Texts in Mathematics 94, Springer (1983), §6.1.

theorem TauCeti.exteriorPower_innerₗ {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] (k : ℕ) : LinearMap.BilinForm.exteriorPower (innerₗ V) k = innerₗ ↥(⋀[ℝ]^k V)

The bilinear form induced by the inner product on the k-th exterior power, given on pure wedges by the Gram determinant, is the inner product of ⋀ᵏ V.

noncomputable def Orientation.volumeEquiv {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [_i : Fact (Module.finrank ℝ V = n)] (o : Orientation ℝ V (Fin n)) : ↥(⋀[ℝ]^(Module.finrank ℝ V) V) ≃ₗ[ℝ] ℝ

The volume of an oriented real inner product space, as a trivialization of its top exterior power: it sends the wedge v₁ ∧ ⋯ ∧ vₙ to Orientation.volumeForm of (v₁, …, vₙ).

theorem Orientation.volumeEquiv_ιMulti {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [_i : Fact (Module.finrank ℝ V = n)] (o : Orientation ℝ V (Fin n)) (v : Fin (Module.finrank ℝ V) → V) : o.volumeEquiv ((exteriorPower.ιMulti ℝ (Module.finrank ℝ V)) v) = o.volumeForm (v ∘ ⇑(finCongr ⋯))

The volume of a wedge of vectors is their Orientation.volumeForm.

theorem Orientation.volumeEquiv_topVector {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [_i : Fact (Module.finrank ℝ V = n)] (o : Orientation ℝ V (Fin n)) (b : OrthonormalBasis (Fin n) ℝ V) (hb : b.toBasis.orientation = o) : o.volumeEquiv b.toBasis.topVector = 1

The volume of the wedge of a positively oriented orthonormal basis is 1.

@[simp]

theorem Orientation.volumeEquiv_neg_orientation {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [_i : Fact (Module.finrank ℝ V = n)] (o : Orientation ℝ V (Fin n)) (x : ↥(⋀[ℝ]^(Module.finrank ℝ V) V)) : (-o).volumeEquiv x = -o.volumeEquiv x

Reversing the orientation negates the volume.

@[simp]

theorem Orientation.volumeEquiv_symm_neg_orientation {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [_i : Fact (Module.finrank ℝ V = n)] (o : Orientation ℝ V (Fin n)) (t : ℝ) : (-o).volumeEquiv.symm t = -o.volumeEquiv.symm t

Reversing the orientation negates the unit volume element of the top exterior power.

noncomputable def Orientation.hodgeStar {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [_i : Fact (Module.finrank ℝ V = n)] (o : Orientation ℝ V (Fin n)) {k l : ℕ} (hkl : k + l = Module.finrank ℝ V) : ↥(⋀[ℝ]^k V) ≃ₗ[ℝ] ↥(⋀[ℝ]^l V)

The Hodge star ⋀ᵏ V ≃ ⋀ˡ V, k + l = finrank ℝ V, of an oriented real inner product space: Mathlib's exteriorPower.hodgeStar for the inner product and Orientation.volumeEquiv. It is characterized by ⟪⋆x, y⟫ = vol (x ∧ y) (Orientation.inner_hodgeStar_apply).

theorem Orientation.inner_hodgeStar_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [_i : Fact (Module.finrank ℝ V = n)] (o : Orientation ℝ V (Fin n)) {k l : ℕ} (hkl : k + l = Module.finrank ℝ V) (x : ↥(⋀[ℝ]^k V)) (y : ↥(⋀[ℝ]^l V)) : inner ℝ ((o.hodgeStar hkl) x) y = ((exteriorPower.wedgePairing o.volumeEquiv hkl) x) y

The characterization of the Hodge star: ⟪⋆x, y⟫ = vol (x ∧ y).

theorem Orientation.hodgeStar_orthonormalBasis {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [_i : Fact (Module.finrank ℝ V = n)] (o : Orientation ℝ V (Fin n)) (b : OrthonormalBasis (Fin n) ℝ V) {k l : ℕ} (hkl : k + l = Module.finrank ℝ V) (s : ↑(Set.powersetCard (Fin n) k)) : (o.hodgeStar hkl) ((Module.Basis.exteriorPower k b.toBasis) s) = o.volumeForm ⇑b • Set.powersetCard.sign s • (Module.Basis.exteriorPower l b.toBasis) ((Set.powersetCard.compl ⋯) s)

On the basis of ⋀ᵏ V induced by any orthonormal basis e, ⋆ e_I = vol(e) ε(I) e_{Iᶜ}, where vol(e) = ±1 is the volume form of e and ε(I) is the shuffle sign of I.

theorem Orientation.hodgeStar_basis {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [_i : Fact (Module.finrank ℝ V = n)] (o : Orientation ℝ V (Fin n)) (b : OrthonormalBasis (Fin n) ℝ V) (hb : b.toBasis.orientation = o) {k l : ℕ} (hkl : k + l = Module.finrank ℝ V) (s : ↑(Set.powersetCard (Fin n) k)) : (o.hodgeStar hkl) ((Module.Basis.exteriorPower k b.toBasis) s) = Set.powersetCard.sign s • (Module.Basis.exteriorPower l b.toBasis) ((Set.powersetCard.compl ⋯) s)

The Hodge star on an orthonormal basis: if e is a positively oriented orthonormal basis, then ⋆ e_I = ε(I) e_{Iᶜ}, where e_I is the increasing wedge of the eᵢ with i ∈ I and ε(I) = Set.powersetCard.sign I is the sign of the shuffle listing I before its complement.

theorem Orientation.hodgeStar_hodgeStar {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [_i : Fact (Module.finrank ℝ V = n)] (o : Orientation ℝ V (Fin n)) {k l : ℕ} (hkl : k + l = Module.finrank ℝ V) (hlk : l + k = Module.finrank ℝ V) (x : ↥(⋀[ℝ]^k V)) : (o.hodgeStar hlk) ((o.hodgeStar hkl) x) = (-1) ^ (k * l) • x

The square of the Hodge star: ⋆⋆x = (-1) ^ (k * l) x for x ∈ ⋀ᵏ V and k + l = finrank ℝ V.

@[simp]

theorem Orientation.hodgeStar_hodgeStar_of_even {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [_i : Fact (Module.finrank ℝ V = n)] (o : Orientation ℝ V (Fin n)) {k : ℕ} (hk : Even k) (hkk : k + k = Module.finrank ℝ V) (x : ↥(⋀[ℝ]^k V)) : (o.hodgeStar hkk) ((o.hodgeStar hkk) x) = x

In an even middle degree, k + k = finrank ℝ V with k even, the Hodge star is an involution, ⋆⋆x = x. This covers two-forms in dimension four, where the self-dual and anti-self-dual two-forms are the ±1 eigenspaces of ⋆.

theorem Orientation.hodgeStar_smul_add_hodgeStar {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [_i : Fact (Module.finrank ℝ V = n)] (o : Orientation ℝ V (Fin n)) {k : ℕ} (hk : Even k) (hkk : k + k = Module.finrank ℝ V) (x : ↥(⋀[ℝ]^k V)) : (o.hodgeStar hkk) (2⁻¹ • (x + (o.hodgeStar hkk) x)) = 2⁻¹ • (x + (o.hodgeStar hkk) x)

In an even middle degree, k + k = finrank ℝ V with k even, the part (x + ⋆x) / 2 of x is self-dual.

theorem Orientation.hodgeStar_smul_sub_hodgeStar {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [_i : Fact (Module.finrank ℝ V = n)] (o : Orientation ℝ V (Fin n)) {k : ℕ} (hk : Even k) (hkk : k + k = Module.finrank ℝ V) (x : ↥(⋀[ℝ]^k V)) : (o.hodgeStar hkk) (2⁻¹ • (x - (o.hodgeStar hkk) x)) = -(2⁻¹ • (x - (o.hodgeStar hkk) x))

In an even middle degree, k + k = finrank ℝ V with k even, the part (x - ⋆x) / 2 of x is anti-self-dual.

theorem Orientation.trace_hodgeStar {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [_i : Fact (Module.finrank ℝ V = n)] (o : Orientation ℝ V (Fin n)) {k : ℕ} (hk : 0 < k) (hkk : k + k = Module.finrank ℝ V) : (LinearMap.trace ℝ ↥(⋀[ℝ]^k V)) ↑(o.hodgeStar hkk) = 0

In a positive middle degree, k + k = finrank ℝ V with 0 < k, the Hodge star is trace free: it sends each vector e_I of the basis of ⋀ᵏ V induced by an orthonormal basis to a multiple of e_{Iᶜ}, and Iᶜ ≠ I.

theorem Orientation.two_mul_finrank_eigenspace_hodgeStar_one {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [_i : Fact (Module.finrank ℝ V = n)] (o : Orientation ℝ V (Fin n)) {k : ℕ} (hk : Even k) (hk₀ : 0 < k) (hkk : k + k = Module.finrank ℝ V) : 2 * Module.finrank ℝ ↥(Module.End.eigenspace (↑(o.hodgeStar hkk)) 1) = n.choose k

In an even positive middle degree, the self-dual forms make up half of ⋀ᵏ V: twice the dimension of the +1 eigenspace of ⋆ is n.choose k. For two-forms in dimension four, the self-dual two-forms Λ⁺ have dimension three.

theorem Orientation.two_mul_finrank_eigenspace_hodgeStar_neg_one {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [_i : Fact (Module.finrank ℝ V = n)] (o : Orientation ℝ V (Fin n)) {k : ℕ} (hk : Even k) (hk₀ : 0 < k) (hkk : k + k = Module.finrank ℝ V) : 2 * Module.finrank ℝ ↥(Module.End.eigenspace (↑(o.hodgeStar hkk)) (-1)) = n.choose k

In an even positive middle degree, the anti-self-dual forms make up half of ⋀ᵏ V: twice the dimension of the -1 eigenspace of ⋆ is n.choose k. For two-forms in dimension four, the anti-self-dual two-forms Λ⁻ have dimension three.

@[simp]

theorem Orientation.hodgeStar_coe_of_mem_eigenspace_one {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [_i : Fact (Module.finrank ℝ V = n)] (o : Orientation ℝ V (Fin n)) {k : ℕ} (hkk : k + k = Module.finrank ℝ V) (x : ↥(Module.End.eigenspace (↑(o.hodgeStar hkk)) 1)) : (o.hodgeStar hkk) ↑x = ↑x

A form in the 1-eigenspace of the Hodge star is self-dual: ⋆x = x.

Two-forms split along a unit vector

theorem Orientation.inner_ιMulti_twoVectorContraction_add_hodgeStar {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [_i : Fact (Module.finrank ℝ V = n)] (o : Orientation ℝ V (Fin n)) (hkk : 2 + 2 = Module.finrank ℝ V) {s : V} (hs : ‖s‖ = 1) (F : ↥(⋀[ℝ]^2 V)) : inner ℝ ((exteriorPower.ιMulti ℝ 2) ![s, (TauCeti.twoVectorContraction F) s]) (F + (o.hodgeStar hkk) F) = ‖(TauCeti.twoVectorContraction F) s‖ ^ 2 + ((exteriorPower.wedgePairing o.volumeEquiv hkk) F) F / 2

The pointwise energy identity of a two-form split along a unit vector. Let s be a unit vector of an oriented four-dimensional real inner product space, let F ∈ ⋀² V, and let a = s ⌟ F be the contraction of F by ⟪s, ·⟫ (TauCeti.twoVectorContraction). Then ⟪s ∧ a, F + ⋆F⟫ = ‖a‖² + vol (F ∧ F) / 2; equivalently, with the self-dual part F⁺ = (F + ⋆F) / 2, 2 ⟪s ∧ a, F⁺⟫ = ‖a‖² + vol (F ∧ F) / 2.

On a product S¹ × Y with s = ds and T = ∂ₛ, this is the pointwise identity 2 ⟨ds ∧ ι_T F, F⁺⟩ dvol = |ι_T F|² dvol + (F ∧ F) / 2 for a real two-form F.