The symmetric and exterior squares of a continuous representation

The tensor square ContRepresentation.tprod π π of a continuous representation acts on V ⊗[𝕜] V by π g ⊗ π g, which commutes with the flip x ⊗ y ↦ y ⊗ x. The two eigenspaces of that flip, TauCeti.symmetricTensors and TauCeti.antisymmetricTensors, are therefore invariant submodules, and restricting the tensor square to them gives the symmetric square and the exterior square of π, again as continuous representations.

Realizing the two squares inside V ⊗[𝕜] V rather than as Sym[𝕜]^2 V and ⋀[𝕜]^2 V is what makes them continuous representations at all: the carrier of a continuous representation has to carry a topology, and a submodule of the tensor square of an inner product space does, whereas a quotient or a subobject of a PiTensorProduct carries none. Over RCLike 𝕜, which has characteristic zero, the two eigenspaces are the symmetric and exterior squares, which is what the names record: the identifications are TauCeti.symmetricTensorsEquivSymmetricPower and TauCeti.antisymmetricTensorsEquivExteriorPower of TauCeti/LinearAlgebra/TensorSquare.lean, and they turn the restriction of π g ⊗ π g into SymmetricPower.map (π g) and exteriorPower.map 2 (π g).

Main definitions

• ContRepresentation.symmetricSquare: the tensor square of a continuous representation restricted to the symmetric tensors of V ⊗[𝕜] V.
• ContRepresentation.exteriorSquare: its restriction to the antisymmetric tensors.

Main statements

• ContRepresentation.continuous_symmetricSquare and ContRepresentation.continuous_exteriorSquare: both squares of a continuous representation are continuous.
• ContRepresentation.symmetricSquare_apply and ContRepresentation.exteriorSquare_apply: each square acts by the restriction of π g ⊗ π g, which is how their characters are computed.
• ContRepresentation.mem_invariants_symmetricSquare_iff and ContRepresentation.mem_invariants_exteriorSquare_iff: a tensor of either eigenspace is invariant for that square exactly when it is invariant for the tensor square.

Implementation notes

Nothing here needs a group, a measure, or compactness, so the statements are made over a topological monoid with RCLike scalars; the consumer is TauCeti/RepresentationTheory/Compact/FrobeniusSchur/InvariantTensors.lean, where the invariants of the two squares are what the Frobenius-Schur indicator counts.

All declarations sit in the root ContRepresentation namespace, so that π.symmetricSquare elaborates: ContRepresentation is Mathlib's type, and scripts/lint-dot-notation.py asks that new declarations about it not recreate its namespace inside TauCeti. That is why the ambient TauCeti names this file consumes are brought in by open.

theorem ContRepresentation.tprod_self_mem_symmetricTensors {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (g : G) {x : TensorProduct 𝕜 V V} (hx : x ∈ TauCeti.symmetricTensors 𝕜 V) : ((π.tprod π) g) x ∈ TauCeti.symmetricTensors 𝕜 V

The tensor square of a continuous representation acts on the tensor square by f ⊗ f, so the symmetric tensors are one of its invariant submodules.

theorem ContRepresentation.tprod_self_mem_antisymmetricTensors {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (g : G) {x : TensorProduct 𝕜 V V} (hx : x ∈ TauCeti.antisymmetricTensors 𝕜 V) : ((π.tprod π) g) x ∈ TauCeti.antisymmetricTensors 𝕜 V

The antisymmetric tensors are the other invariant submodule of the tensor square.

noncomputable def ContRepresentation.symmetricSquare {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) : ContRepresentation 𝕜 G ↥(TauCeti.symmetricTensors 𝕜 V)

The symmetric square of a continuous representation: its tensor square restricted to the symmetric tensors.

Equations

• π.symmetricSquare = (π.tprod π).subrepresentation (TauCeti.symmetricTensors 𝕜 V) ⋯

noncomputable def ContRepresentation.exteriorSquare {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) : ContRepresentation 𝕜 G ↥(TauCeti.antisymmetricTensors 𝕜 V)

The exterior square of a continuous representation: its tensor square restricted to the antisymmetric tensors. Over RCLike 𝕜, which has characteristic zero, those are the exterior square ⋀[𝕜]^2 V realized inside V ⊗[𝕜] V, which is what the name records; the identification is TauCeti.antisymmetricTensorsEquivExteriorPower (see the module docstring).

Equations

• π.exteriorSquare = (π.tprod π).subrepresentation (TauCeti.antisymmetricTensors 𝕜 V) ⋯

theorem ContRepresentation.continuous_symmetricSquare {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) : Continuous ⇑π.symmetricSquare

The symmetric square of a continuous representation is continuous.

theorem ContRepresentation.continuous_exteriorSquare {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) : Continuous ⇑π.exteriorSquare

The exterior square of a continuous representation is continuous.

@[simp]

theorem ContRepresentation.symmetricSquare_apply {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (g : G) : ↑(π.symmetricSquare g) = TauCeti.symmetricTensorsRestrict ↑(π g)

The symmetric square acts by the restriction of π g ⊗ π g.

@[simp]

theorem ContRepresentation.exteriorSquare_apply {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (g : G) : ↑(π.exteriorSquare g) = TauCeti.antisymmetricTensorsRestrict ↑(π g)

The exterior square acts by the restriction of π g ⊗ π g.

theorem ContRepresentation.mem_invariants_symmetricSquare_iff {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) {x : ↥(TauCeti.symmetricTensors 𝕜 V)} : x ∈ π.symmetricSquare.invariants ↔ ↑x ∈ (π.tprod π).invariants

Membership in the invariants of the symmetric square, read in the tensor square.

theorem ContRepresentation.mem_invariants_exteriorSquare_iff {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) {x : ↥(TauCeti.antisymmetricTensors 𝕜 V)} : x ∈ π.exteriorSquare.invariants ↔ ↑x ∈ (π.tprod π).invariants

Membership in the invariants of the exterior square, read in the tensor square.