Norms and linear isometries of exterior powers

The exterior powers ⋀[ℝ]^n E of a finite-dimensional real inner product space carry Mathlib's induced inner product, with ⟪v₁ ∧ ⋯ ∧ vₙ, w₁ ∧ ⋯ ∧ wₙ⟫ = det ⟪vⱼ, wᵢ⟫. This file proves that the map ⋀ⁿ f induced by a linear isometry f preserves it, so that rotations of an oriented space act isometrically on its forms, and that infinitesimal rotations, the skew-adjoint endomorphisms, act skew-adjointly on forms of every degree. It also records that the norm of a wedge v₁ ∧ ⋯ ∧ vₙ is the volume of the parallelepiped spanned by the vᵢ, bounded by Hadamard's inequality. For a real-linear P : E → ℂ, it names the two-vector p₁ ∧ p₂ of the gradients of Re P and Im P, which represents the two-form Im (conj (P u) P w). Finally, it packages the skew endomorphism u ↦ u ⌟ F of a two-vector F, the operator that represents the two-form ω(u, w) = ⟪F, u ∧ w⟫ through the inner product.

Main definitions

• ContinuousLinearMap.gradientWedge P: the wedge p₁ ∧ p₂ of the vectors representing the real and imaginary parts of a complex-valued covector P.
• TauCeti.twoVectorContraction F: the skew endomorphism u ↦ u ⌟ F of a two-vector, with ⟪u ⌟ F, w⟫ = ⟪F, u ∧ w⟫.

Main results

• exteriorPower.inner_map_map: ⟪⋀ⁿ f x, ⋀ⁿ f y⟫ = ⟪x, y⟫ for a linear isometry f.
• exteriorPower.inner_ιMulti_two: ⟪a ∧ b, u ∧ w⟫ = ⟪a, u⟫ ⟪b, w⟫ - ⟪a, w⟫ ⟪b, u⟫.
• exteriorPower.ext_inner_ιMulti: elements of ⋀ⁿ E with the same inner products against all wedges of vectors are equal, and exteriorPower.linearMap_ext_inner_ιMulti is the corresponding extensionality principle for linear maps between exterior powers; exteriorPower.ext_inner_ιMulti_two and exteriorPower.linearMap_ext_inner_ιMulti_two test only against wedges u ∧ w of two vectors.
• exteriorPower.inner_lieMap_left: the derivation action D_A of a skew-adjoint A on ⋀ⁿ E is skew-adjoint, ⟪D_A x, y⟫ = -⟪x, D_A y⟫.
• OrthonormalBasis.sum_norm_sq_ιMulti_two: contraction of squared wedge norms in a basis.
• OrthonormalBasis.inner_toBasis_exteriorPower: the induced basis of ⋀ⁿ E is orthonormal.
• OrthonormalBasis.ιMulti_two_eq_sum, OrthonormalBasis.inner_ιMulti_two_eq_sum, OrthonormalBasis.norm_sq_eq_sum_sq_inner_ιMulti_two: the coordinates of two-vectors in the basis bᵢ ∧ bⱼ induced by an orthonormal basis b of a four-dimensional space.
• exteriorPower.norm_ιMulti_sq: ‖v₁ ∧ ⋯ ∧ vₙ‖ ^ 2 is the Gram determinant of v.
• exteriorPower.norm_ιMulti_le_prod_norm: Hadamard's inequality ‖v₁ ∧ ⋯ ∧ vₙ‖ ≤ ∏ ‖vᵢ‖, and exteriorPower.norm_ιMulti_two_le: its case ‖u ∧ w‖ ≤ ‖u‖ ‖w‖ of two vectors.
• ContinuousLinearMap.inner_gradientWedge_ιMulti: for a real-linear P : E → ℂ, the two-form Im (conj (P u) P w) is represented by p₁ ∧ p₂, ⟪p₁ ∧ p₂, u ∧ w⟫ = Im (conj (P u) P w).
• TauCeti.inner_twoVectorContraction_apply: the contraction u ⌟ F of a two-vector F ∈ ⋀² V by ⟪u, ·⟫ (TauCeti.twoVectorContraction) represents the two-form of F, ⟪u ⌟ F, w⟫ = ⟪F, u ∧ w⟫: on two-forms, wedging with u is adjoint to contracting with ⟪u, ·⟫. So u ↦ u ⌟ F is skew-adjoint (TauCeti.inner_twoVectorContraction_apply_left).

theorem exteriorPower.inner_map_map {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {n : ℕ} (f : E →ₗᵢ[ℝ] F) (x y : ↥(⋀[ℝ]^n E)) : inner ℝ ((map n f.toLinearMap) x) ((map n f.toLinearMap) y) = inner ℝ x y

The map of exterior powers induced by a linear isometry preserves the inner product.

theorem exteriorPower.inner_ιMulti_two {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (a b u w : E) : inner ℝ ((ιMulti ℝ 2) ![a, b]) ((ιMulti ℝ 2) ![u, w]) = inner ℝ a u * inner ℝ b w - inner ℝ a w * inner ℝ b u

The inner product of two wedges of two vectors is their 2 × 2 Gram determinant.

theorem exteriorPower.ext_inner_ιMulti {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} {x y : ↥(⋀[ℝ]^n E)} (h : ∀ (v : Fin n → E), inner ℝ x ((ιMulti ℝ n) v) = inner ℝ y ((ιMulti ℝ n) v)) : x = y

Elements of ⋀ⁿ E are determined by their inner products with wedges of vectors, since these wedges span ⋀ⁿ E.

theorem exteriorPower.linearMap_ext_inner_ιMulti {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {n m : ℕ} {f g : ↥(⋀[ℝ]^n E) →ₗ[ℝ] ↥(⋀[ℝ]^m F)} (h : ∀ (v : Fin n → E) (w : Fin m → F), inner ℝ (f ((ιMulti ℝ n) v)) ((ιMulti ℝ m) w) = inner ℝ (g ((ιMulti ℝ n) v)) ((ιMulti ℝ m) w)) : f = g

Linear maps ⋀ⁿ E → ⋀ᵐ F agree when their values on wedges of vectors have the same inner products with all wedges of vectors.

theorem exteriorPower.ext_inner_ιMulti_two {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {x y : ↥(⋀[ℝ]^2 E)} (h : ∀ (u w : E), inner ℝ x ((ιMulti ℝ 2) ![u, w]) = inner ℝ y ((ιMulti ℝ 2) ![u, w])) : x = y

Two-vectors are determined by their inner products with the wedges u ∧ w of two vectors: the form of ext_inner_ιMulti whose hypothesis matches the lemmas stated for ιMulti ℝ 2 ![u, w], such as inner_ιMulti_two.

theorem exteriorPower.linearMap_ext_inner_ιMulti_two {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {f g : ↥(⋀[ℝ]^2 E) →ₗ[ℝ] ↥(⋀[ℝ]^2 F)} (h : ∀ (a b : E) (u w : F), inner ℝ (f ((ιMulti ℝ 2) ![a, b])) ((ιMulti ℝ 2) ![u, w]) = inner ℝ (g ((ιMulti ℝ 2) ![a, b])) ((ιMulti ℝ 2) ![u, w])) : f = g

Linear maps ⋀² E → ⋀² F agree when their values on wedges a ∧ b have the same inner products with all wedges u ∧ w: the two-vector form of linearMap_ext_inner_ιMulti.

theorem exteriorPower.inner_lieMap_left {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} {A : E →ₗ[ℝ] E} (hA : ∀ (u w : E), inner ℝ (A u) w = -inner ℝ u (A w)) (x y : ↥(⋀[ℝ]^n E)) : inner ℝ (((lieMap n) A) x) y = -inner ℝ x (((lieMap n) A) y)

Skew-adjoint endomorphisms act skew-adjointly on exterior powers: if ⟪A u, w⟫ = -⟪u, A w⟫ for all u, w, then the derivation action D_A on ⋀ⁿ E, which applies A to one factor of a wedge at a time, satisfies ⟪D_A x, y⟫ = -⟪x, D_A y⟫.

theorem exteriorPower.norm_ιMulti_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (v : Fin n → E) : ‖(ιMulti ℝ n) v‖ ^ 2 = (Matrix.gram ℝ v).det

The squared norm of a wedge of vectors is their Gram determinant.

theorem exteriorPower.norm_ιMulti_le_prod_norm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (v : Fin n → E) : ‖(ιMulti ℝ n) v‖ ≤ ∏ i : Fin n, ‖v i‖

Hadamard's inequality for wedges: ‖v₁ ∧ ⋯ ∧ vₙ‖ ≤ ‖v₁‖ ⋯ ‖vₙ‖.

theorem exteriorPower.norm_ιMulti_two_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (u w : E) : ‖(ιMulti ℝ 2) ![u, w]‖ ≤ ‖u‖ * ‖w‖

Hadamard's inequality for two vectors: ‖u ∧ w‖ ≤ ‖u‖ ‖w‖.

noncomputable def ContinuousLinearMap.gradientWedge {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (P : E →L[ℝ] ℂ) : ↥(⋀[ℝ]^2 E)

The two-vector p₁ ∧ p₂ of the gradients of the real and imaginary parts of a complex-valued covector P = p₁ + i p₂. It represents the two-form Im (conj (P u) P w) (ContinuousLinearMap.inner_gradientWedge_ιMulti).

@[simp]

theorem ContinuousLinearMap.inner_gradientWedge_ιMulti {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (P : E →L[ℝ] ℂ) (u w : E) : inner ℝ P.gradientWedge ((exteriorPower.ιMulti ℝ 2) ![u, w]) = ((starRingEnd ℂ) (P u) * P w).im

The two-form Im (conj (P u) P w) is represented by the two-vector p₁ ∧ p₂ of the gradients of the real and imaginary parts of P.

theorem OrthonormalBasis.sum_norm_sq_ιMulti_two {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Fintype ι] (b : OrthonormalBasis ι ℝ E) (u : E) : ∑ i : ι, ‖(exteriorPower.ιMulti ℝ 2) ![b i, u]‖ ^ 2 = (↑(Fintype.card ι) - 1) * ‖u‖ ^ 2

Contracting the squared norms of eᵢ ∧ u in an orthonormal basis gives (dim E - 1) |u|². This includes dimensions zero and one.

theorem OrthonormalBasis.inner_toBasis_exteriorPower {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Fintype ι] [LinearOrder ι] (b : OrthonormalBasis ι ℝ E) (n : ℕ) (u v : ↑(Set.powersetCard ι n)) : inner ℝ ((Module.Basis.exteriorPower n b.toBasis) u) ((Module.Basis.exteriorPower n b.toBasis) v) = if u = v then 1 else 0

The basis of ⋀ⁿ E induced by an orthonormal basis b of E is orthonormal.

Two-vectors in an orthonormal frame of a four-dimensional space

theorem OrthonormalBasis.ιMulti_two_eq_sum {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (b : OrthonormalBasis (Fin 4) ℝ E) (u w : E) : (exteriorPower.ιMulti ℝ 2) ![u, w] = ((b.repr u).ofLp 0 * (b.repr w).ofLp 1 - (b.repr u).ofLp 1 * (b.repr w).ofLp 0) • (exteriorPower.ιMulti ℝ 2) ![b 0, b 1] + ((b.repr u).ofLp 0 * (b.repr w).ofLp 2 - (b.repr u).ofLp 2 * (b.repr w).ofLp 0) • (exteriorPower.ιMulti ℝ 2) ![b 0, b 2] + ((b.repr u).ofLp 0 * (b.repr w).ofLp 3 - (b.repr u).ofLp 3 * (b.repr w).ofLp 0) • (exteriorPower.ιMulti ℝ 2) ![b 0, b 3] + ((b.repr u).ofLp 1 * (b.repr w).ofLp 2 - (b.repr u).ofLp 2 * (b.repr w).ofLp 1) • (exteriorPower.ιMulti ℝ 2) ![b 1, b 2] + ((b.repr u).ofLp 1 * (b.repr w).ofLp 3 - (b.repr u).ofLp 3 * (b.repr w).ofLp 1) • (exteriorPower.ιMulti ℝ 2) ![b 1, b 3] + ((b.repr u).ofLp 2 * (b.repr w).ofLp 3 - (b.repr u).ofLp 3 * (b.repr w).ofLp 2) • (exteriorPower.ιMulti ℝ 2) ![b 2, b 3]

A wedge of two vectors in the basis bᵢ ∧ bⱼ, i < j, of ⋀² E induced by an orthonormal basis b indexed by Fin 4.

theorem OrthonormalBasis.inner_ιMulti_two_eq_sum {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (b : OrthonormalBasis (Fin 4) ℝ E) (x : ↥(⋀[ℝ]^2 E)) (u w : E) : inner ℝ x ((exteriorPower.ιMulti ℝ 2) ![u, w]) = ((b.repr u).ofLp 0 * (b.repr w).ofLp 1 - (b.repr u).ofLp 1 * (b.repr w).ofLp 0) * inner ℝ x ((exteriorPower.ιMulti ℝ 2) ![b 0, b 1]) + ((b.repr u).ofLp 0 * (b.repr w).ofLp 2 - (b.repr u).ofLp 2 * (b.repr w).ofLp 0) * inner ℝ x ((exteriorPower.ιMulti ℝ 2) ![b 0, b 2]) + ((b.repr u).ofLp 0 * (b.repr w).ofLp 3 - (b.repr u).ofLp 3 * (b.repr w).ofLp 0) * inner ℝ x ((exteriorPower.ιMulti ℝ 2) ![b 0, b 3]) + ((b.repr u).ofLp 1 * (b.repr w).ofLp 2 - (b.repr u).ofLp 2 * (b.repr w).ofLp 1) * inner ℝ x ((exteriorPower.ιMulti ℝ 2) ![b 1, b 2]) + ((b.repr u).ofLp 1 * (b.repr w).ofLp 3 - (b.repr u).ofLp 3 * (b.repr w).ofLp 1) * inner ℝ x ((exteriorPower.ιMulti ℝ 2) ![b 1, b 3]) + ((b.repr u).ofLp 2 * (b.repr w).ofLp 3 - (b.repr u).ofLp 3 * (b.repr w).ofLp 2) * inner ℝ x ((exteriorPower.ιMulti ℝ 2) ![b 2, b 3])

The pairing of a two-vector with a wedge of two vectors, in the coordinates of an orthonormal basis b indexed by Fin 4.

theorem OrthonormalBasis.norm_sq_eq_sum_sq_inner_ιMulti_two {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (b : OrthonormalBasis (Fin 4) ℝ E) (x : ↥(⋀[ℝ]^2 E)) : ‖x‖ ^ 2 = inner ℝ x ((exteriorPower.ιMulti ℝ 2) ![b 0, b 1]) ^ 2 + inner ℝ x ((exteriorPower.ιMulti ℝ 2) ![b 0, b 2]) ^ 2 + inner ℝ x ((exteriorPower.ιMulti ℝ 2) ![b 0, b 3]) ^ 2 + inner ℝ x ((exteriorPower.ιMulti ℝ 2) ![b 1, b 2]) ^ 2 + inner ℝ x ((exteriorPower.ιMulti ℝ 2) ![b 1, b 3]) ^ 2 + inner ℝ x ((exteriorPower.ιMulti ℝ 2) ![b 2, b 3]) ^ 2

The squared norm of a two-vector is the sum of the squares of its coordinates in the basis bᵢ ∧ bⱼ, i < j, induced by an orthonormal basis b indexed by Fin 4.

noncomputable def TauCeti.twoVectorContraction {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (F : ↥(⋀[ℝ]^2 V)) : V →ₗ[ℝ] V

The skew endomorphism of a two-vector F ∈ ⋀² V: the contraction u ↦ u ⌟ F of F by the functional ⟪u, ·⟫, read as a vector of V with ExteriorAlgebra.ιInv. It is the operator A with ⟪A u, w⟫ = ω(u, w) for the two-form ω(u, w) = ⟪F, u ∧ w⟫ that F represents (TauCeti.inner_twoVectorContraction_apply).

theorem TauCeti.twoVectorContraction_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (F : ↥(⋀[ℝ]^2 V)) (u : V) : (twoVectorContraction F) u = ExteriorAlgebra.ιInv ((CliffordAlgebra.contractLeft ((innerₗ V) u)) ↑F)

@[simp]

theorem TauCeti.twoVectorContraction_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] : twoVectorContraction 0 = 0

@[simp]

theorem TauCeti.twoVectorContraction_add {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (F G : ↥(⋀[ℝ]^2 V)) : twoVectorContraction (F + G) = twoVectorContraction F + twoVectorContraction G

@[simp]

theorem TauCeti.twoVectorContraction_smul {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (c : ℝ) (F : ↥(⋀[ℝ]^2 V)) : twoVectorContraction (c • F) = c • twoVectorContraction F

@[simp]

theorem TauCeti.twoVectorContraction_neg {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (F : ↥(⋀[ℝ]^2 V)) : twoVectorContraction (-F) = -twoVectorContraction F

@[simp]

theorem TauCeti.inner_twoVectorContraction_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] (F : ↥(⋀[ℝ]^2 V)) (u w : V) : inner ℝ ((twoVectorContraction F) u) w = inner ℝ F ((exteriorPower.ιMulti ℝ 2) ![u, w])

The contraction represents the two-form of F: ⟪u ⌟ F, w⟫ = ⟪F, u ∧ w⟫. Equivalently, on two-forms, wedging with u is adjoint to contracting with ⟪u, ·⟫.

theorem TauCeti.inner_twoVectorContraction_apply_self {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (F : ↥(⋀[ℝ]^2 V)) (u : V) : inner ℝ ((twoVectorContraction F) u) u = 0

The contraction by a two-vector is orthogonal to its argument, ⟪u ⌟ F, u⟫ = 0.

theorem TauCeti.inner_twoVectorContraction_apply_left {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (F : ↥(⋀[ℝ]^2 V)) (u w : V) : inner ℝ ((twoVectorContraction F) u) w = -inner ℝ u ((twoVectorContraction F) w)

The contraction by a two-vector is skew-adjoint: ⟪u ⌟ F, w⟫ = -⟪u, w ⌟ F⟫.