Invariant tensors and invariant bilinear forms

On an inner product space the inner product turns a tensor t of the tensor square V ⊗[𝕜] V into the bilinear form B_t (v, w) = ⟪t, v ⊗ₜ w⟫, TauCeti.BilinForm.ofTensor, built in TauCeti/Analysis/InnerProductSpace/BilinearForm.lean together with its injectivity, its surjectivity in finite dimensions -- only there is it an identification of the tensor square with all of BilinForm 𝕜 V -- and the fact that it carries the symmetric tensors to the symmetric forms and the antisymmetric tensors to the alternating ones.

This file makes that construction equivariant: for a unitary representation π, the invariants of the tensor square π ⊗ π become the invariant forms of π, in the sense of TauCeti.Representation.IsInvariantForm. Together with the symmetry dictionary this says that the two eigenspaces of the flip that TauCeti/RepresentationTheory/Continuous/Square/Invariants.lean counts are, invariant vector by invariant vector, the invariant symmetric and the invariant alternating forms. That is the dictionary the compact-group Frobenius-Schur trichotomy is read off from in TauCeti/RepresentationTheory/Compact/FrobeniusSchur/InvariantForm.lean; it is the analytic counterpart of TauCeti/LinearAlgebra/BilinearForm/Squares.lean, which does the same job for finite groups through the dual of the symmetric and exterior powers rather than through an inner product.

Nothing here needs a topology on G, a measure, compactness, or even inverses: the acting object is a monoid, and unitarity is the only hypothesis on π. It is what makes the dictionary equivariant: π g ⊗ π g preserves the inner product of the tensor square, so moving it across ⟪t, v ⊗ₜ w⟫ costs nothing. It is also all the converse needs -- invariance of the form of t says that ⟪t, (π ⊗ π) g s⟫ = ⟪t, s⟫ on the pure tensors, hence on all of the tensor square, and an operator preserving the inner product and fixing ⟪t, -⟫ fixes t itself. Only the statements identifying every form as the form of a tensor ask for finite dimensions, and they ask for it through TauCeti.BilinForm.ofTensor_surjective.

Main definitions

• ContRepresentation.invariantsEquivInvariantForms: in finite dimensions, the invariants of the tensor square are the invariant forms, conjugate-linearly.
• ContRepresentation.symmetricSquareInvariantsEquivSymmetricInvariantForms and ContRepresentation.exteriorSquareInvariantsEquivAlternatingInvariantForms: the same for the two squares, whose invariants are the invariant symmetric, respectively alternating, forms.

Main statements

• ContRepresentation.isInvariantForm_ofTensor_iff: the form of a tensor is invariant for a unitary representation exactly when the tensor is invariant for the tensor square.
• ContRepresentation.map_ofTensor_invariants: the same statement for the two spaces, rather than vector by vector.
• ContRepresentation.exists_isInvariantForm_isSymm_ne_zero_iff and ContRepresentation.exists_isInvariantForm_isAlt_ne_zero_iff: a nonzero invariant symmetric, respectively alternating, form exists exactly when the symmetric, respectively exterior, square has a nonzero invariant tensor.

Implementation notes

The two equivalences for the squares are two readings of one argument, which is why they are both read off the private ContRepresentation.invariantsEquivOfMemIff, stated for an arbitrary subrepresentation of the tensor square cut out by a property of the corresponding forms. The last two statements carry no argument of their own: an equivalence identifies the two nontriviality statements, and a submodule is nontrivial exactly when it is not ⊥.

References

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.

@[simp]

theorem ContRepresentation.isInvariantForm_ofTensor_iff {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : π.IsUnitary) {t : TensorProduct 𝕜 V V} : TauCeti.Representation.IsInvariantForm (toRepresentation 𝕜 G V π) (TauCeti.BilinForm.ofTensor t) ↔ t ∈ (π.tprod π).invariants

The form of a tensor is invariant exactly when the tensor is invariant. This is a statement about one tensor at a time; that every invariant form is the form of an invariant tensor is ContRepresentation.map_ofTensor_invariants, which needs finite dimensions.

theorem ContRepresentation.map_ofTensor_invariants {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) [FiniteDimensional 𝕜 V] (hπ : π.IsUnitary) : Submodule.map TauCeti.BilinForm.ofTensor (π.tprod π).invariants = TauCeti.Representation.invariantForms (toRepresentation 𝕜 G V π)

The invariant tensors of the tensor square are exactly the invariant forms, as submodules: the image of the invariants under TauCeti.BilinForm.ofTensor is TauCeti.Representation.invariantForms.

noncomputable def ContRepresentation.invariantsEquivInvariantForms {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) [FiniteDimensional 𝕜 V] (hπ : π.IsUnitary) : ↥(π.tprod π).invariants ≃ₗ⋆[𝕜] ↥(TauCeti.Representation.invariantForms (toRepresentation 𝕜 G V π))

The invariants of the tensor square are the invariant forms, conjugate-linearly: the equivalence TauCeti.BilinForm.ofTensorEquiv restricted to the invariants.

Equations

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

@[simp]

theorem ContRepresentation.coe_invariantsEquivInvariantForms_apply {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) [FiniteDimensional 𝕜 V] (hπ : π.IsUnitary) (t : ↥(π.tprod π).invariants) : ↑((π.invariantsEquivInvariantForms hπ) t) = TauCeti.BilinForm.ofTensor ↑t

noncomputable def ContRepresentation.symmetricSquareInvariantsEquivSymmetricInvariantForms {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) [FiniteDimensional 𝕜 V] (hπ : π.IsUnitary) : ↥π.symmetricSquare.invariants ≃ₗ⋆[𝕜] ↥(TauCeti.Representation.symmetricInvariantForms (toRepresentation 𝕜 G V π))

The invariants of the symmetric square are the invariant symmetric forms, conjugate-linearly: the equivalence TauCeti.BilinForm.ofTensorEquiv restricted to them.

Equations

• π.symmetricSquareInvariantsEquivSymmetricInvariantForms hπ = ContRepresentation.invariantsEquivOfMemIff✝ π hπ ⋯ ⋯ ⋯

@[simp]

theorem ContRepresentation.coe_symmetricSquareInvariantsEquivSymmetricInvariantForms_apply {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) [FiniteDimensional 𝕜 V] (hπ : π.IsUnitary) (x : ↥π.symmetricSquare.invariants) : ↑((π.symmetricSquareInvariantsEquivSymmetricInvariantForms hπ) x) = TauCeti.BilinForm.ofTensor ↑↑x

noncomputable def ContRepresentation.exteriorSquareInvariantsEquivAlternatingInvariantForms {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) [FiniteDimensional 𝕜 V] (hπ : π.IsUnitary) : ↥π.exteriorSquare.invariants ≃ₗ⋆[𝕜] ↥(TauCeti.Representation.alternatingInvariantForms (toRepresentation 𝕜 G V π))

The invariants of the exterior square are the invariant alternating forms, conjugate-linearly: the equivalence TauCeti.BilinForm.ofTensorEquiv restricted to them.

Equations

• π.exteriorSquareInvariantsEquivAlternatingInvariantForms hπ = ContRepresentation.invariantsEquivOfMemIff✝ π hπ ⋯ ⋯ ⋯

@[simp]

theorem ContRepresentation.coe_exteriorSquareInvariantsEquivAlternatingInvariantForms_apply {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) [FiniteDimensional 𝕜 V] (hπ : π.IsUnitary) (x : ↥π.exteriorSquare.invariants) : ↑((π.exteriorSquareInvariantsEquivAlternatingInvariantForms hπ) x) = TauCeti.BilinForm.ofTensor ↑↑x

theorem ContRepresentation.exists_isInvariantForm_isSymm_ne_zero_iff {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) [FiniteDimensional 𝕜 V] (hπ : π.IsUnitary) : (∃ (B : LinearMap.BilinForm 𝕜 V), TauCeti.Representation.IsInvariantForm (toRepresentation 𝕜 G V π) B ∧ B.IsSymm ∧ B ≠ 0) ↔ π.symmetricSquare.invariants ≠ ⊥

A nonzero invariant symmetric form is the same thing as a nonzero invariant tensor of the symmetric square: both sides say that the two sides of ContRepresentation.symmetricSquareInvariantsEquivSymmetricInvariantForms are nontrivial.

theorem ContRepresentation.exists_isInvariantForm_isAlt_ne_zero_iff {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) [FiniteDimensional 𝕜 V] (hπ : π.IsUnitary) : (∃ (B : LinearMap.BilinForm 𝕜 V), TauCeti.Representation.IsInvariantForm (toRepresentation 𝕜 G V π) B ∧ B.IsAlt ∧ B ≠ 0) ↔ π.exteriorSquare.invariants ≠ ⊥

A nonzero invariant alternating form is the same thing as a nonzero invariant tensor of the exterior square: both sides say that the two sides of ContRepresentation.exteriorSquareInvariantsEquivAlternatingInvariantForms are nontrivial.