The bilinear form of a tensor on an inner product space

On an inner product space the inner product turns a tensor t : V ⊗[𝕜] V into a bilinear form on V,

B_t (v, w) = ⟪t, v ⊗ₜ w⟫,

TauCeti.BilinForm.ofTensor. The construction is conjugate-linear in t and always injective, so a tensor is determined by its form; it is surjective only in finite dimensions, where it therefore identifies the tensor square with all of BilinForm 𝕜 V (TauCeti.BilinForm.ofTensorEquiv). In infinite dimensions it is just an injection: the tensor square is spanned by the finite sums of pure tensors, while a general bilinear form need not be one.

The construction carries the flip x ⊗ y ↦ y ⊗ x to the exchange of the two arguments of a form, so the symmetric tensors TauCeti.symmetricTensors become the symmetric forms and the antisymmetric tensors TauCeti.antisymmetricTensors the alternating ones.

Nothing here needs a group or a representation: this is the purely bilinear half of the dictionary that TauCeti/RepresentationTheory/Continuous/Square/BilinearForm.lean makes equivariant for a unitary representation.

Main definitions

• TauCeti.BilinForm.ofTensor: the bilinear form B_t (v, w) = ⟪t, v ⊗ₜ w⟫ of a tensor.
• TauCeti.BilinForm.ofTensorEquiv: in finite dimensions, that construction as a conjugate-linear equivalence of the tensor square with the bilinear forms.

Main statements

• TauCeti.BilinForm.ofTensor_injective and TauCeti.BilinForm.ofTensor_surjective: the construction is injective, and surjective in finite dimensions.
• TauCeti.BilinForm.isSymm_ofTensor_iff and TauCeti.BilinForm.isAlt_ofTensor_iff: the form of a tensor is symmetric, respectively alternating, exactly when the tensor is symmetric, respectively antisymmetric.

Implementation notes

TauCeti.BilinForm.ofTensor is conjugate-linear, not linear, so it is bundled as a semilinear map V ⊗[𝕜] V →ₛₗ[starRingEnd 𝕜] BilinForm 𝕜 V; it is the composition of innerSL with the currying TensorProduct.lcurry, so its behaviour on 0, on sums, on negation and on differences is the generic map_zero, map_add, map_neg and map_sub. Injectivity comes from TensorProduct.ext_iff_inner_right; surjectivity in finite dimensions is read off TauCeti.BilinForm.ofTensorEquiv, which is assembled from the Riesz representation InnerProductSpace.toDual, the identification LinearMap.toContinuousLinearMap of the linear with the continuous linear functionals, and the currying TensorProduct.lift.equiv.

The two symmetry statements go through Mathlib's flip characterizations LinearMap.BilinForm.isSymm_iff_flip and LinearMap.isAlt_iff_eq_neg_flip, so the only geometric input is TauCeti.BilinForm.ofTensor_comm, that the construction intertwines the flip of the tensor square with the flip of a form.

References

This is the linear-algebra half of the invariant-form dictionary that Layer 6b of the compact-groups roadmap needs for its frobeniusSchurIndicator_eq_one_iff and frobeniusSchurIndicator_eq_neg_one_iff targets. The mathematical development follows Daniel Bump, Lie Groups, second edition, Chapter 2, and T. Bröcker and T. tom Dieck, Representations of Compact Lie Groups, Springer GTM 98 (1985), Chapter II.

noncomputable def TauCeti.BilinForm.ofTensor {𝕜 : Type u_1} {V : Type u_2} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] : TensorProduct 𝕜 V V →ₗ⋆[𝕜] LinearMap.BilinForm 𝕜 V

The bilinear form of a tensor: B_t (v, w) = ⟪t, v ⊗ₜ w⟫. The inner product is conjugate-linear in its first argument and linear in its second, so this is bilinear in (v, w) and conjugate-linear in t.

Equations

• TauCeti.BilinForm.ofTensor = TensorProduct.lcurry (RingHom.id 𝕜) V V 𝕜 ∘ₛₗ ContinuousLinearMap.coeLM 𝕜 ∘ₛₗ ↑(innerSL 𝕜)

@[simp]

theorem TauCeti.BilinForm.ofTensor_apply {𝕜 : Type u_1} {V : Type u_2} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (t : TensorProduct 𝕜 V V) (v w : V) : ((ofTensor t) v) w = inner 𝕜 t (v ⊗ₜ[𝕜] w)

theorem TauCeti.BilinForm.ofTensor_injective {𝕜 : Type u_1} {V : Type u_2} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] : Function.Injective ⇑ofTensor

A tensor is determined by its form.

@[simp]

theorem TauCeti.BilinForm.ofTensor_eq_zero_iff {𝕜 : Type u_1} {V : Type u_2} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {t : TensorProduct 𝕜 V V} : ofTensor t = 0 ↔ t = 0

The form of a tensor vanishes only for the zero tensor.

@[simp]

theorem TauCeti.BilinForm.ofTensor_comm {𝕜 : Type u_1} {V : Type u_2} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (t : TensorProduct 𝕜 V V) : ofTensor ((TensorProduct.comm 𝕜 V V) t) = LinearMap.BilinForm.flipHom (ofTensor t)

The flip of the tensor square is the flip of the form.

@[simp]

theorem TauCeti.BilinForm.isSymm_ofTensor_iff {𝕜 : Type u_1} {V : Type u_2} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {t : TensorProduct 𝕜 V V} : (ofTensor t).IsSymm ↔ t ∈ symmetricTensors 𝕜 V

The form of a tensor is symmetric exactly when the tensor is symmetric.

@[simp]

theorem TauCeti.BilinForm.isAlt_ofTensor_iff {𝕜 : Type u_1} {V : Type u_2} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {t : TensorProduct 𝕜 V V} : (ofTensor t).IsAlt ↔ t ∈ antisymmetricTensors 𝕜 V

The form of a tensor is alternating exactly when the tensor is antisymmetric.

noncomputable def TauCeti.BilinForm.ofTensorEquiv {𝕜 : Type u_1} {V : Type u_2} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] : TensorProduct 𝕜 V V ≃ₗ⋆[𝕜] LinearMap.BilinForm 𝕜 V

In finite dimensions the tensor square is the space of bilinear forms, conjugate-linearly, through TauCeti.BilinForm.ofTensor: the Riesz representation InnerProductSpace.toDual identifies a tensor with a functional on the tensor square, and the currying TensorProduct.lift.equiv identifies such a functional with a bilinear form.

Equations

• TauCeti.BilinForm.ofTensorEquiv = (InnerProductSpace.toDual 𝕜 (TensorProduct 𝕜 V V)).trans (LinearMap.toContinuousLinearMap.symm.trans (TensorProduct.lift.equiv (RingHom.id 𝕜) V V 𝕜).symm)

@[simp]

theorem TauCeti.BilinForm.ofTensorEquiv_apply {𝕜 : Type u_1} {V : Type u_2} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] (t : TensorProduct 𝕜 V V) : ofTensorEquiv t = ofTensor t

@[simp]

theorem TauCeti.BilinForm.coe_ofTensorEquiv {𝕜 : Type u_1} {V : Type u_2} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] : ↑ofTensorEquiv = ofTensor

theorem TauCeti.BilinForm.ofTensor_surjective {𝕜 : Type u_1} {V : Type u_2} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] : Function.Surjective ⇑ofTensor

Every bilinear form on a finite-dimensional inner product space is the form of a tensor, because TauCeti.BilinForm.ofTensorEquiv is an equivalence.