Canonical tensors in real inner product spaces

Given an InnerProductSpace ℝ E, this file defines two canonical tensors.

• InnerProductSpace.canonicalContravariantTensor E : E ⊗[ℝ] E →ₗ[ℝ] ℝ. This is the element corresponding to the inner product.

• If E is finite-dimensional, then E ⊗[ℝ] E is canonically isomorphic to its dual. Accordingly, there exists an element InnerProductSpace.canonicalCovariantTensor E : E ⊗[ℝ] E that corresponds to InnerProductSpace.canonicalContravariantTensor E under this identification.

The theorem canonicalCovariantTensor_eq_sum shows that InnerProductSpace.canonicalCovariantTensor E can be computed from any orthonormal basis v as ∑ i, (v i) ⊗ₜ[ℝ] (v i).

noncomputable def InnerProductSpace.canonicalContravariantTensor (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] : TensorProduct ℝ E E →ₗ[ℝ] ℝ

The canonical contravariant tensor corresponding to the inner product

Equations

• InnerProductSpace.canonicalContravariantTensor E = TensorProduct.lift bilinFormOfRealInner

noncomputable def InnerProductSpace.canonicalCovariantTensor (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] : TensorProduct ℝ E E

The canonical covariant tensor corresponding to InnerProductSpace.canonicalContravariantTensor under the identification of E with its dual.

Equations

• InnerProductSpace.canonicalCovariantTensor E = ∑ i : Fin (Module.finrank ℝ E), (stdOrthonormalBasis ℝ E) i ⊗ₜ[ℝ] (stdOrthonormalBasis ℝ E) i

theorem InnerProductSpace.canonicalCovariantTensor_eq_sum (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {ι : Type u_2} [Fintype ι] (v : OrthonormalBasis ι ℝ E) : canonicalCovariantTensor E = ∑ i : ι, v i ⊗ₜ[ℝ] v i

Representation of the canonical covariant tensor in terms of an orthonormal basis.