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, thenE ⊗[ℝ] E
is canonically isomorphic to its dual. Accordingly, there exists an elementInnerProductSpace.canonicalCovariantTensor E : E ⊗[ℝ] E
that corresponds toInnerProductSpace.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)
.
The canonical contravariant tensor corresponding to the inner product
Instances For
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
Instances For
Representation of the canonical covariant tensor in terms of an orthonormal basis.