Inner product space structure on exterior powers

Given a real inner product space E, we construct a canonical inner product on ⋀[ℝ]^n E via the Gram determinant formula: on decomposable elements, ⟪v₁ ∧ ⋯ ∧ vₙ, w₁ ∧ ⋯ ∧ wₙ⟫ = det (⟪vⱼ, wᵢ⟫)ᵢⱼ.

Main results

• exteriorPower.inner_ιMulti_ιMulti: The inner product on decomposable elements equals the Gram determinant.
• exteriorPower.inner_ιMulti_self: ⟪v₁ ∧ ⋯ ∧ vₙ, v₁ ∧ ⋯ ∧ vₙ⟫ = det (gram ℝ v).
• OrthonormalBasis.exteriorPower: An orthonormal basis of E induces an orthonormal basis of ⋀[ℝ]^n E.

Future work

• Generalize to RCLike 𝕜. To define innerProductForm in this case, we would probably want a semilinear generalization of exteriorPower.map, which in turn requires generalizing AlternatingMap to the semilinear setting.
• Remove the FiniteDimensional hypothesis from the InnerProductSpace instance. Currently the proofs of re_inner_nonneg and definite require finite dimension, because we need to choose an orthonormal basis of E. But we can reduce the general case to the finite-dimensional case by noticing that any x : ⋀[𝕜]^n E is contained in some ⋀[𝕜]^n F for a finite-dimensional subspace F ≤ E.

@[instance_reducible]

noncomputable instance exteriorPower.instCoreRealSubtypeExteriorAlgebraMemSubmoduleExteriorPowerOfFiniteDimensional {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] : InnerProductSpace.Core ℝ ↥(⋀[ℝ]^n E)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance exteriorPower.instNormedAddCommGroupSubtypeExteriorAlgebraRealMemSubmoduleExteriorPowerOfFiniteDimensional {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] : NormedAddCommGroup ↥(⋀[ℝ]^n E)

Equations

• exteriorPower.instNormedAddCommGroupSubtypeExteriorAlgebraRealMemSubmoduleExteriorPowerOfFiniteDimensional = InnerProductSpace.Core.toNormedAddCommGroup

@[instance_reducible]

noncomputable instance exteriorPower.instInnerProductSpaceRealSubtypeExteriorAlgebraMemSubmoduleExteriorPower {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] : InnerProductSpace ℝ ↥(⋀[ℝ]^n E)

Equations

• One or more equations did not get rendered due to their size.

theorem exteriorPower.inner_ιMulti_ιMulti {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (x y : Fin n → E) : inner ℝ ((ιMulti ℝ n) x) ((ιMulti ℝ n) y) = (Matrix.of fun (i j : Fin n) => inner ℝ (x j) (y i)).det

theorem exteriorPower.inner_ιMulti_self {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (x : Fin n → E) : inner ℝ ((ιMulti ℝ n) x) ((ιMulti ℝ n) x) = (Matrix.gram ℝ x).det

noncomputable def OrthonormalBasis.exteriorPower {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {I : Type u_2} [Fintype I] [LinearOrder I] (b : OrthonormalBasis I ℝ E) (n : ℕ) : OrthonormalBasis ↑(Set.powersetCard I n) ℝ ↥(⋀[ℝ]^n E)

An orthonormal basis of a finite-dimensional real inner product space E induces an orthonormal basis of ⋀[ℝ]^n E, indexed by n-element subsets of the index type.

Equations

• b.exteriorPower n = (Module.Basis.exteriorPower n b.toBasis).toOrthonormalBasis ⋯

@[simp]

theorem OrthonormalBasis.toBasis_exteriorPower {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {I : Type u_2} [Fintype I] [LinearOrder I] (b : OrthonormalBasis I ℝ E) (n : ℕ) : (b.exteriorPower n).toBasis = Module.Basis.exteriorPower n b.toBasis