A class function acts on an irreducible representation by a scalar

A continuous function f on a compact group G acts on a continuous representation π on V by the integrated operator

integratedOperator π hπ f = ∫ g, f g • π g ∂(haarProb G),

the Haar average of the action operators weighted by f. Its trace is the Haar integral of f · χ_π, with no hypothesis on f.

When f is a class function — constant on conjugacy classes — the integrated operator commutes with the action, because conjugating the integrand by π h translates its group variable by g ↦ h⁻¹ g h, which normalized Haar measure does not see and which f does not see either. So for an irreducible π over an algebraically closed field Schur's lemma makes it a scalar, and the trace computation fixes that scalar:

integratedOperator π hπ f = (dim V)⁻¹ · (∫ g, f g · χ_π g) • id.

Specializing f to conj χ_π turns the character orthogonality relations into the character projections; the irreducible block identities are in TauCeti/RepresentationTheory/Compact/Character/Projection.lean, and their assembly into the isotypic projector is in TauCeti/RepresentationTheory/Compact/Character/IsotypicProjection.lean.

Main definitions

• TauCeti.ContRepresentation.integratedOperator: the operator ∫ g, f g • π g by which a continuous scalar function acts on a continuous representation.
• TauCeti.ContRepresentation.integratedOperatorₗ: the same, linear in the acting function.
• TauCeti.ContRepresentation.integratedIntertwiner: the integrated operator of a class function, packaged as a continuous self-intertwiner.

Main results

• TauCeti.ContRepresentation.trace_integratedOperator: the trace of the integrated operator is ∫ g, f g · χ_π g.
• ContRepresentation.comp_integratedOperator: integrated operators are natural with respect to continuous intertwiners.
• TauCeti.ContRepresentation.integratedOperator_comp: a class function acts by an intertwiner.
• TauCeti.ContRepresentation.integratedOperator_eq_smul_id: a class function acts on a finite-dimensional irreducible representation by the scalar (dim V)⁻¹ · ∫ g, f g · χ_π g.
• TauCeti.ContRepresentation.integratedOperator_eq_zero: it acts as zero when that integral vanishes.

Implementation notes

Being a class function is carried as the bare hypothesis ∀ g h : G, f (h * g * h⁻¹) = f g, the same shape as in TauCeti/RepresentationTheory/Compact/ClassFunctionLp.lean, rather than as a new predicate: it is passed directly through this API, and the L²-level notion that deserves a bundling is the almost-everywhere one, TauCeti.classFunctionLp, which is already defined.

The definition asks only that V be a normed space: it is TauCeti.haarAverage of a continuous family valued in the operator space V →L[𝕜] V, so it inherits that average's convention. What the Bochner integral reads is completeness of that codomain, and [CompleteSpace V] is what supplies it; failing that, the average is the integral's junk value 0 rather than the classical integrated form π(f). Completeness therefore enters with TauCeti.ContRepresentation.integratedOperator_apply, finite-dimensionality with the trace, and algebraic closedness of the scalars with Schur's lemma. The integrated operator of the trivial group action and other structural identities are not developed here: what the character projections need is linearity in f, the trace, and the scalar theorem.

The scalar in integratedOperator_eq_smul_id is (dim V)⁻¹ · ∫ f · χ_π, not ∫ f · conj χ_π: the integrand pairs f with the character itself, and the conjugation appears only when the acting function is specialized to conj χ_π.

References

The integrated operators support averaging against dim V_π · conj χ_π to project onto isotypic components. 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.

noncomputable def TauCeti.ContRepresentation.integratedOperator {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (f : C(G, 𝕜)) : V →L[𝕜] V

The operator by which a continuous scalar function acts on a continuous representation, ∫ g, f g • π g ∂(haarProb G).

On a complete V this is the classical integrated form π(f) of the representation, and it is always defined there: the integrand is continuous and normalized Haar measure is finite. V is not assumed complete. The average is taken in the operator space V →L[𝕜] V, so it is TauCeti.haarAverage's junk value 0 unless that space is complete, which [CompleteSpace V] supplies; that is why the results below that read the operator's actual value carry it.

Equations

• TauCeti.ContRepresentation.integratedOperator π hπ f = (TauCeti.haarAverage G) (TauCeti.ContRepresentation.weightFamily✝ π hπ f)

theorem TauCeti.ContRepresentation.integratedOperator_apply {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (f : C(G, 𝕜)) (v : V) : (integratedOperator π hπ f) v = ∫ (g : G), f g • (π g) v ∂haarProb G

The integrated operator, evaluated at a vector.

theorem ContRepresentation.comp_integratedOperator {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) {W : Type u_4} [NormedAddCommGroup W] [NormedSpace 𝕜 W] [NormedSpace ℝ W] [SMulCommClass ℝ 𝕜 W] [CompleteSpace W] (rho : ContRepresentation 𝕜 G W) (hrho : Continuous ⇑rho) (T : ContIntertwiningMap π rho) (f : C(G, 𝕜)) : T.toContinuousLinearMap ∘SL TauCeti.ContRepresentation.integratedOperator π hπ f = TauCeti.ContRepresentation.integratedOperator rho hrho f ∘SL T.toContinuousLinearMap

Integrated operators are natural in the representation. A continuous intertwiner commutes with the operators obtained by integrating the same scalar function on its source and target.

Linearity in the acting function

@[simp]

theorem TauCeti.ContRepresentation.integratedOperator_zero {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) : integratedOperator π hπ 0 = 0

@[simp]

theorem TauCeti.ContRepresentation.integratedOperator_add {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (f₁ f₂ : C(G, 𝕜)) : integratedOperator π hπ (f₁ + f₂) = integratedOperator π hπ f₁ + integratedOperator π hπ f₂

@[simp]

theorem TauCeti.ContRepresentation.integratedOperator_smul {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (c : 𝕜) (f : C(G, 𝕜)) : integratedOperator π hπ (c • f) = c • integratedOperator π hπ f

noncomputable def TauCeti.ContRepresentation.integratedOperatorₗ {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) : C(G, 𝕜) →ₗ[𝕜] V →L[𝕜] V

The integrated operator, bundled as a linear map in the acting function. Bundling supplies the remaining additive identities (map_neg, map_sub, map_sum) through the LinearMap API.

Equations

• TauCeti.ContRepresentation.integratedOperatorₗ π hπ = { toFun := TauCeti.ContRepresentation.integratedOperator π hπ, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.ContRepresentation.integratedOperatorₗ_apply {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (f : C(G, 𝕜)) : (integratedOperatorₗ π hπ) f = integratedOperator π hπ f

A class function acts by an intertwiner

Conjugation by a fixed pair of action operators is a continuous linear map on operators, so it commutes with Haar averaging; on the integrand it acts as the conjugation g ↦ h⁻¹ g h of the group variable, which normalized Haar measure does not see and which a class function does not see either.

theorem TauCeti.ContRepresentation.integratedOperator_comp {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) {f : C(G, 𝕜)} (hf : ∀ (g h : G), f (h * g * h⁻¹) = f g) (h : G) : integratedOperator π hπ f ∘SL π h = π h ∘SL integratedOperator π hπ f

A class function acts by an intertwiner. The integrated operator of a function constant on conjugacy classes commutes with every action operator.

noncomputable def TauCeti.ContRepresentation.integratedIntertwiner {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) {f : C(G, 𝕜)} (hf : ∀ (g h : G), f (h * g * h⁻¹) = f g) : ContIntertwiningMap π π

The action of a class function, packaged as a term of Mathlib's ContIntertwiningMap.

Equations

• TauCeti.ContRepresentation.integratedIntertwiner π hπ hf = { toContinuousLinearMap := TauCeti.ContRepresentation.integratedOperator π hπ f, isIntertwining' := ⋯ }

@[simp]

theorem TauCeti.ContRepresentation.toContinuousLinearMap_integratedIntertwiner {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) {f : C(G, 𝕜)} (hf : ∀ (g h : G), f (h * g * h⁻¹) = f g) : (integratedIntertwiner π hπ hf).toContinuousLinearMap = integratedOperator π hπ f

theorem TauCeti.ContRepresentation.instCompleteSpaceIntegrated {𝕜 : Type u_1} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] : CompleteSpace V

Completeness of V is not an extra hypothesis on the results below: a finite-dimensional normed space over an RCLike field is already complete. Mathlib keeps FiniteDimensional.complete out of the global instance set, so it is installed here as a local instance instead.

theorem TauCeti.ContRepresentation.trace_integratedOperator {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (f : C(G, 𝕜)) : (LinearMap.trace 𝕜 V) ↑(integratedOperator π hπ f) = ∫ (g : G), f g * (π.character hπ) g ∂haarProb G

The trace of the integrated operator is the Haar integral of f · χ_π. No hypothesis on f is needed. This is what fixes the normalizing factor in TauCeti.ContRepresentation.integratedOperator_eq_smul_id.

theorem TauCeti.ContRepresentation.integratedOperator_eq_smul_id {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) [IsAlgClosed 𝕜] {f : C(G, 𝕜)} (hf : ∀ (g h : G), f (h * g * h⁻¹) = f g) (hirr : (ContRepresentation.toRepresentation 𝕜 G V π).IsIrreducible) : integratedOperator π hπ f = ((↑(Module.finrank 𝕜 V))⁻¹ * ∫ (g : G), f g * (π.character hπ) g ∂haarProb G) • ContinuousLinearMap.id 𝕜 V

A class function acts on a finite-dimensional irreducible representation by the scalar (dim V)⁻¹ · ∫ g, f g · χ_π g.

This is the operator form of the statement that the centre of the group algebra acts on an irreducible by central characters; specialized to f = conj χ_π it gives the blockwise identities of the character projection in TauCeti/RepresentationTheory/Compact/Character/Projection.lean.

theorem TauCeti.ContRepresentation.integratedOperator_eq_zero {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) [IsAlgClosed 𝕜] {f : C(G, 𝕜)} (hf : ∀ (g h : G), f (h * g * h⁻¹) = f g) (hirr : (ContRepresentation.toRepresentation 𝕜 G V π).IsIrreducible) (hzero : ∫ (g : G), f g * (π.character hπ) g ∂haarProb G = 0) : integratedOperator π hπ f = 0

A class function whose Haar integral against the character vanishes acts as zero on an irreducible representation.