The conjugate of a continuous representation

Complex conjugation of the matrix entries of a representation gives another representation, the conjugate (equivalently, for a unitary representation, the contragredient). It is what the span of the matrix coefficients needs in order to be closed under the involution of C(G, 𝕜): conjugating a matrix coefficient of π produces a matrix coefficient of the conjugate of π, not of π itself.

There is no canonical conjugation on an abstract inner product space, so the construction takes an orthonormal basis e as data and conjugates each action operator by the coordinatewise conjugation TauCeti.conjugation of that basis, using TauCeti.conjCLM. Different bases give conjugates that are isomorphic representations, so the choice is immaterial for the uses downstream, which only need one conjugate to exist.

Main definitions

• OrthonormalBasis.conjugate: the conjugate representation.

Main statements

• OrthonormalBasis.continuous_conjugate and OrthonormalBasis.isUnitary_conjugate: the conjugate of a continuous representation is continuous, and of a unitary one is unitary.
• OrthonormalBasis.conjugate_conjugate: conjugating twice returns the original representation.
• OrthonormalBasis.star_matrixCoeff_eq_matrixCoeff_conjugate: the conjugate of a matrix coefficient of π is a matrix coefficient of the conjugate of π.

The mathematical development follows Daniel Bump, Lie Groups, second edition, Chapter 2.

noncomputable def OrthonormalBasis.conjugate {𝕜 : 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) : ContRepresentation 𝕜 G V

The conjugate of a continuous representation with respect to an orthonormal basis: the action operators are conjugated entrywise in that basis.

Equations

• e.conjugate π = { toMonoidHom := { toFun := fun (g : G) => TauCeti.conjCLM e (π g), map_one' := ⋯, map_mul' := ⋯ } }

@[simp]

theorem OrthonormalBasis.conjugate_apply {𝕜 : 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) (g : G) : (e.conjugate π) g = TauCeti.conjCLM e (π g)

The action operators of the conjugate representation.

@[simp]

theorem OrthonormalBasis.conjugate_conjugate {𝕜 : 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) : e.conjugate (e.conjugate π) = π

Conjugating twice returns the original representation, because conjugation of operators is an involution.

theorem OrthonormalBasis.continuous_conjugate {𝕜 : Type u_1} {ι : Type u_2} {G : Type u_3} {V : Type u_4} [RCLike 𝕜] [Fintype ι] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) : Continuous ⇑(e.conjugate π)

The conjugate of a continuous representation has a continuous operator-valued action.

theorem OrthonormalBasis.isUnitary_conjugate {𝕜 : 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) : (e.conjugate π).IsUnitary

The conjugate of a unitary representation is unitary.

theorem OrthonormalBasis.star_matrixCoeff_eq_matrixCoeff_conjugate {𝕜 : Type u_1} {ι : Type u_2} {G : Type u_3} {V : Type u_4} [RCLike 𝕜] [Fintype ι] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v w : V) : star (π.matrixCoeff hπ v w) = (e.conjugate π).matrixCoeff ⋯ (TauCeti.conjugation e v) (TauCeti.conjugation e w)

The conjugate of a matrix coefficient is a matrix coefficient of the conjugate representation, at the conjugated vectors. This is the identity that makes the span of all matrix coefficients stable under the involution of C(G, 𝕜).