Documentation

TauCeti.RepresentationTheory.Continuous.Square.Invariants

The invariant tensors of an irreducible unitary representation are at most a line #

For an irreducible unitary representation π of a monoid on a finite-dimensional inner product space over an algebraically closed field, the invariants of the tensor square are at most one-dimensional, and consequently so are the invariants of the symmetric and of the exterior square together:

dim (Sym²V)ᴳ + dim (Λ²V)ᴳ ≤ 1.

That inequality is the whole content of the Frobenius-Schur trichotomy: the indicator is the difference of those two dimensions (ContRepresentation.frobeniusSchurIndicator_eq_sub_finrank_invariants), so an inequality on their sum pins the difference to 1, 0 or -1.

The argument is Schur's lemma applied through a contraction. An orthonormal basis e carries the bilinear form B(v, w) = ⟪J v, w⟫ and the contraction TauCeti.tensorSquareEquivEnd e : V ⊗[𝕜] V ≃ₗ[𝕜] (V →ₗ[𝕜] V); unitarity of π makes B invariant for the pair (π, {}^J π), where {}^J π = OrthonormalBasis.conjugate e π is the conjugate representation, so an invariant tensor contracts to an intertwiner {}^J π ⟶ π. Schur's lemma makes a nonzero such intertwiner surjective, hence bijective, and then every other one is a scalar multiple of it, because the two composed through the inverse commute with π. Pulling that back along the contraction, which is injective, says the invariant tensors are a line.

Only the target π of those intertwiners has to be irreducible, which is why the conjugate representation is never itself shown irreducible: surjectivity of a nonzero intertwiner needs irreducibility of the target only, and injectivity then comes from finite-dimensionality.

The symmetric and the antisymmetric tensors are invariant submodules that meet in 0 (TauCeti.isCompl_symmetricTensors_antisymmetricTensors), so their invariants sit inside the invariants of the tensor square as two submodules in direct sum, and the bound on the sum follows from the bound on the tensor square.

Main statements #

Implementation notes #

All declarations sit in the root ContRepresentation namespace, so that dot notation on Mathlib's ContRepresentation elaborates and scripts/lint-dot-notation.py is satisfied; the ambient TauCeti names are brought in by open, following TauCeti/RepresentationTheory/Continuous/Square/Basic.lean.

The statements that do not name a contraction take no orthonormal basis: a finite-dimensional inner product space has stdOrthonormalBasis, and the bounds do not depend on which basis is used. The conjugate representation appears only through TauCeti.conjCLM, never through a statement about its irreducibility or its character.

References #

The Frobenius-Schur reality trichotomy itself is in TauCeti/RepresentationTheory/Compact/FrobeniusSchur/Trichotomy.lean. 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.

source
theorem ContRepresentation.inner_conjugation_apply_conjCLM {𝕜 : Type u_1} {ι : Type u_2} {G : Type u_3} {V : Type u_4} [RCLike 𝕜] [Fintype ι] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (π : ContRepresentation 𝕜 G V) (hπ : π.IsUnitary) (g : G) (v u : V) :
inner 𝕜 (TauCeti.conjugation e ((π g) v)) ((TauCeti.conjCLM e (π g)) u) = inner 𝕜 (TauCeti.conjugation e v) u

The bilinear form of an orthonormal basis is invariant for π against its conjugate. The two conjugations cancel against the unitarity of π, which is the identity that makes the contraction of an invariant tensor an intertwiner.

source
theorem ContRepresentation.tensorSquareEquivEnd_tprod_apply {𝕜 : Type u_1} {ι : Type u_2} {G : Type u_3} {V : Type u_4} [RCLike 𝕜] [Fintype ι] [DecidableEq ι] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (π : ContRepresentation 𝕜 G V) (hπ : π.IsUnitary) (g : G) (t : TensorProduct 𝕜 V V) (u : V) :
((TauCeti.tensorSquareEquivEnd e) (((π.tprod π) g) t)) ((TauCeti.conjCLM e (π g)) u) = (π g) (((TauCeti.tensorSquareEquivEnd e) t) u)

Contracting the tensor square commutes with the action, up to conjugating the argument: the contraction of (π g ⊗ π g) t at {}^J(π g) u is π g of the contraction of t at u.

source
theorem ContRepresentation.tensorSquareEquivEnd_conjCLM_of_mem_invariants {𝕜 : Type u_1} {ι : Type u_2} {G : Type u_3} {V : Type u_4} [RCLike 𝕜] [Fintype ι] [DecidableEq ι] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (π : ContRepresentation 𝕜 G V) (hπ : π.IsUnitary) {t : TensorProduct 𝕜 V V} (ht : t ∈ (π.tprod π).invariants) (g : G) (u : V) :
((TauCeti.tensorSquareEquivEnd e) t) ((TauCeti.conjCLM e (π g)) u) = (π g) (((TauCeti.tensorSquareEquivEnd e) t) u)

The contraction of an invariant tensor intertwines the conjugate representation with π.

source
noncomputable def ContRepresentation.invariantTensorIntertwiner {𝕜 : Type u_1} {ι : Type u_2} {G : Type u_3} {V : Type u_4} [RCLike 𝕜] [Fintype ι] [DecidableEq ι] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (π : ContRepresentation 𝕜 G V) (hπ : π.IsUnitary) {t : TensorProduct 𝕜 V V} (ht : t ∈ (π.tprod π).invariants) :
(toRepresentation 𝕜 G V (e.conjugate π)).IntertwiningMap (toRepresentation 𝕜 G V π)

The intertwiner {}^J π ⟶ π that an invariant tensor contracts to.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem ContRepresentation.invariantTensorIntertwiner_apply {𝕜 : Type u_1} {ι : Type u_2} {G : Type u_3} {V : Type u_4} [RCLike 𝕜] [Fintype ι] [DecidableEq ι] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (π : ContRepresentation 𝕜 G V) (hπ : π.IsUnitary) {t : TensorProduct 𝕜 V V} (ht : t ∈ (π.tprod π).invariants) (u : V) :
    (invariantTensorIntertwiner e π hπ ht) u = ((TauCeti.tensorSquareEquivEnd e) t) u
    source
    theorem ContRepresentation.tensorSquareEquivEnd_bijective_of_mem_invariants {𝕜 : Type u_1} {ι : Type u_2} {G : Type u_3} {V : Type u_4} [RCLike 𝕜] [Fintype ι] [DecidableEq ι] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (π : ContRepresentation 𝕜 G V) (hπ : π.IsUnitary) (hirr : (toRepresentation 𝕜 G V π).IsIrreducible) {t : TensorProduct 𝕜 V V} (ht : t ∈ (π.tprod π).invariants) (ht0 : t ≠ 0) :
    Function.Bijective ⇑((TauCeti.tensorSquareEquivEnd e) t)

    A nonzero invariant tensor contracts to a bijection: its contraction is a nonzero intertwiner into the irreducible π, hence surjective, and in finite dimensions surjective is bijective.

    source
    theorem ContRepresentation.exists_smul_eq_of_mem_invariants_tprod {𝕜 : Type u_1} {G : Type u_3} {V : Type u_4} [RCLike 𝕜] [IsAlgClosed 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] {π : ContRepresentation 𝕜 G V} (hπ : π.IsUnitary) (hirr : (toRepresentation 𝕜 G V π).IsIrreducible) {t t' : TensorProduct 𝕜 V V} (ht : t ∈ (π.tprod π).invariants) (ht0 : t ≠ 0) (ht' : t' ∈ (π.tprod π).invariants) :
    ∃ (c : 𝕜), t' = c • t

    Any two invariant tensors of an irreducible unitary representation are proportional, once one of them is nonzero: composing the contraction of the second with the inverse of the contraction of the first gives a self-intertwiner of π, which Schur's lemma makes a scalar.

    source
    theorem ContRepresentation.finrank_invariants_tprod_self_le_one {𝕜 : Type u_1} {G : Type u_3} {V : Type u_4} [RCLike 𝕜] [IsAlgClosed 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] {π : ContRepresentation 𝕜 G V} (hπ : π.IsUnitary) (hirr : (toRepresentation 𝕜 G V π).IsIrreducible) :
    Module.finrank 𝕜 ↥(π.tprod π).invariants ≤ 1

    The invariant tensors of an irreducible unitary representation are at most a line. They are all proportional to any nonzero one of them.

    source
    theorem ContRepresentation.finrank_invariants_squares_le_one {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [IsAlgClosed 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] {π : ContRepresentation 𝕜 G V} (hπ : π.IsUnitary) (hirr : (toRepresentation 𝕜 G V π).IsIrreducible) :
    Module.finrank 𝕜 ↥π.symmetricSquare.invariants + Module.finrank 𝕜 ↥π.exteriorSquare.invariants ≤ 1

    The two invariant counts the Frobenius-Schur indicator subtracts add up to at most 1. The symmetric and the antisymmetric tensors meet in 0, so their invariants sit in direct sum inside the invariants of the tensor square, which are at most a line.