Transporting a continuous representation along a continuous linear equivalence

A continuous linear equivalence e : V ≃L[𝕜] W carries a continuous representation on V to one on W by conjugating every action operator, π g ↦ e ∘ π g ∘ e⁻¹, that is, by applying Mathlib's continuous algebra equivalence ContinuousLinearEquiv.conjContinuousAlgEquiv. This file builds that transport and records what it preserves: continuity of the operator-valued action, and — for an equivalence that is moreover isometric, so that inner products are available — unitarity and, the point of the construction, the matrix coefficients, which are unchanged once the defining vectors are moved along e.

The transport is what lets a statement about representations on the standard models EuclideanSpace 𝕜 (Fin n) be applied to a representation on an arbitrary finite-dimensional inner product space: stdOrthonormalBasis supplies the isometry (stdOrthonormalBasis 𝕜 V).repr, so nothing is lost by pinning a model.

Main definitions

• ContinuousLinearEquiv.congr: the transported representation e ∘ π · ∘ e⁻¹.
• ContRepresentation.congrEquiv: the equivalence of continuous representations π ≃ congr e π witnessed by e itself, which is what carries a statement about the transport back to π.

Main statements

• ContinuousLinearEquiv.continuous_congr, ContinuousLinearEquiv.isIrreducible_congr and ContRepresentation.IsUnitary.congr: the transport preserves continuity, irreducibility, and unitarity.
• ContRepresentation.congr_refl and ContinuousLinearEquiv.congr_congr: the transport is functorial, so "transportable onto" is an equivalence relation on representations (symmetry is simp from these two).
• LinearIsometryEquiv.matrixCoeff_congr: the matrix coefficients of the transport at the transported vectors are those of the original representation.
• ContinuousLinearEquiv.matrixCoeff_congr_adjoint: the same for an equivalence that is not isometric, where the second vector moves along the adjoint of e⁻¹ instead of along e.

noncomputable def ContinuousLinearEquiv.congr {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [NormedField 𝕜] [Monoid G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (e : V ≃L[𝕜] W) (π : ContRepresentation 𝕜 G V) : ContRepresentation 𝕜 G W

Transport along a continuous linear equivalence. The representation on W obtained from a representation on V by conjugating each action operator with e : V ≃L[𝕜] W.

Equations

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

theorem ContinuousLinearEquiv.congr_apply {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [NormedField 𝕜] [Monoid G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (e : V ≃L[𝕜] W) (π : ContRepresentation 𝕜 G V) (g : G) (x : W) : ((e.congr π) g) x = e ((π g) (e.symm x))

The action operators of a transported representation.

@[simp]

theorem ContinuousLinearEquiv.coe_congr {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [NormedField 𝕜] [Monoid G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (e : V ≃L[𝕜] W) (π : ContRepresentation 𝕜 G V) : ⇑(e.congr π) = fun (g : G) => e.conjContinuousAlgEquiv (π g)

The operator-valued function underlying a transported representation.

theorem ContinuousLinearEquiv.continuous_congr {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [NormedField 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (e : V ≃L[𝕜] W) {π : ContRepresentation 𝕜 G V} (hπ : Continuous ⇑π) : Continuous ⇑(e.congr π)

Transport preserves continuity of the operator-valued action: conjugation by e is the continuous algebra equivalence ContinuousLinearEquiv.conjContinuousAlgEquiv.

theorem ContinuousLinearEquiv.isIrreducible_congr {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [NormedField 𝕜] [Monoid G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (e : V ≃L[𝕜] W) {π : ContRepresentation 𝕜 G V} (hπ : (ContRepresentation.toRepresentation 𝕜 G V π).IsIrreducible) : (ContRepresentation.toRepresentation 𝕜 G W (e.congr π)).IsIrreducible

Transport preserves irreducibility: e is an equivariant linear equivalence from π to its transport, and irreducibility is invariant under such an equivalence.

@[simp]

theorem ContRepresentation.congr_refl {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [NormedField 𝕜] [Monoid G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) : (ContinuousLinearEquiv.refl 𝕜 V).congr π = π

Transport along the identity changes nothing.

@[simp]

theorem ContinuousLinearEquiv.congr_congr {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [NormedField 𝕜] [Monoid G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] {X : Type u_5} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (e : V ≃L[𝕜] W) (f : W ≃L[𝕜] X) (π : ContRepresentation 𝕜 G V) : f.congr (e.congr π) = (e.trans f).congr π

Transporting twice is transporting along the composite.

theorem ContRepresentation.IsUnitary.congr {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] {π : ContRepresentation 𝕜 G V} (hπ : π.IsUnitary) (e : V ≃ₗᵢ[𝕜] W) : ((↑e).congr π).IsUnitary

Transport along a linear isometry equivalence preserves unitarity: e and e⁻¹ preserve the inner product, so the conjugated operators do exactly when the original ones do.

@[simp]

theorem LinearIsometryEquiv.matrixCoeff_congr {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] (e : V ≃ₗᵢ[𝕜] W) {π : ContRepresentation 𝕜 G V} (hπ : Continuous ⇑((↑e).congr π)) (v w : V) : ((↑e).congr π).matrixCoeff hπ (e v) (e w) = π.matrixCoeff ⋯ v w

Transport along a linear isometry equivalence does not change matrix coefficients. The matrix coefficient of the transported representation at the transported vectors is the matrix coefficient of the original.

@[simp]

theorem ContinuousLinearEquiv.matrixCoeff_congr_adjoint {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [CompleteSpace W] (e : V ≃L[𝕜] W) {π : ContRepresentation 𝕜 G V} (hπ : Continuous ⇑(e.congr π)) (v w : V) : (e.congr π).matrixCoeff hπ (e v) ((ContinuousLinearMap.adjoint ↑e.symm) w) = π.matrixCoeff ⋯ v w

Transport along an arbitrary continuous linear equivalence moves matrix coefficients along e and along the adjoint of e⁻¹. For an e that is not isometric the second vector has to be moved by (e⁻¹)† rather than by e, since it is paired with the transported vector rather than transported itself.

This is LinearIsometryEquiv.matrixCoeff_congr with the isometry hypothesis dropped: for a linear isometry equivalence (e⁻¹)† = e, and the two statements agree. It is what says that being a matrix coefficient depends only on the equivalence class of a representation, so a representation may be replaced by any conjugate of it — for instance by a unitary one.

noncomputable def ContRepresentation.congrEquiv {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [NormedField 𝕜] [Monoid G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (e : V ≃L[𝕜] W) : π.Equiv (e.congr π)

The transport of a representation is equivalent to it, along e itself: e intertwines π with ContinuousLinearEquiv.congr e π by the very definition of the transported action.

This is the bundled form of that observation, and it is what carries a statement about the transport back to π: an Equiv is an isomorphism in the category of continuous representations, so π and congr e π have the same subrepresentation lattice, the same irreducible constituents and the same character. congrEquiv_apply and congrEquiv_symm_apply evaluate it and its inverse as e and e.symm.

Equations

• π.congrEquiv e = ContRepresentation.Equiv.mk e ⋯

@[simp]

theorem ContRepresentation.congrEquiv_toContinuousLinearEquiv {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [NormedField 𝕜] [Monoid G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (e : V ≃L[𝕜] W) : (π.congrEquiv e).toContinuousLinearEquiv = e

@[simp]

theorem ContRepresentation.congrEquiv_apply {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [NormedField 𝕜] [Monoid G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (e : V ≃L[𝕜] W) (v : V) : (π.congrEquiv e) v = e v

@[simp]

theorem ContRepresentation.congrEquiv_symm_apply {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [NormedField 𝕜] [Monoid G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (e : V ≃L[𝕜] W) (w : W) : (π.congrEquiv e).symm w = e.symm w