Unitary continuous representations

This file defines when a continuous representation preserves a real or complex inner product. It characterizes unitarity through norm preservation, isometries, and Mathlib's unitary submonoid of continuous linear operators, and records the basic inner-product identities, the coefficient bound, and that unitarity passes to restrictions.

The operator characterizations reuse Mathlib's adjoint and unitary-operator theory.

The mathematical development follows Daniel Bump, Lie Groups, second edition, Chapters 2–4.

def ContRepresentation.IsUnitary {𝕜 : Type u_4} {G : Type u_5} {V : Type u_6} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) : Prop

A continuous representation is unitary when every action operator preserves the inner product.

Equations

• π.IsUnitary = ∀ (g : G) (v w : V), inner 𝕜 ((π g) v) ((π g) w) = inner 𝕜 v w

theorem ContRepresentation.isUnitary_iff_norm_map {𝕜 : Type u_4} {G : Type u_5} {V : Type u_6} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) : π.IsUnitary ↔ ∀ (g : G) (v : V), ‖(π g) v‖ = ‖v‖

A representation is unitary exactly when every action map preserves norms.

theorem ContRepresentation.isUnitary_iff_isometry {𝕜 : Type u_4} {G : Type u_5} {V : Type u_6} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) : π.IsUnitary ↔ ∀ (g : G), Isometry ⇑(π g)

A representation is unitary exactly when every action map is an isometry.

@[simp]

theorem ContRepresentation.IsUnitary.inner_map_map {𝕜 : Type u_4} {G : Type u_5} {V : Type u_6} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} (hπ : π.IsUnitary) (g : G) (v w : V) : inner 𝕜 ((π g) v) ((π g) w) = inner 𝕜 v w

A unitary representation preserves the inner product.

@[simp]

theorem ContRepresentation.IsUnitary.norm_map {𝕜 : Type u_4} {G : Type u_5} {V : Type u_6} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} (hπ : π.IsUnitary) (g : G) (v : V) : ‖(π g) v‖ = ‖v‖

Every action map of a unitary representation preserves norms.

theorem ContRepresentation.IsUnitary.norm_le_one {𝕜 : Type u_4} {G : Type u_5} {V : Type u_6} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} (hπ : π.IsUnitary) (g : G) : ‖π g‖ ≤ 1

Every action operator of a unitary representation has operator norm at most 1.

theorem ContRepresentation.IsUnitary.exists_norm_le {𝕜 : Type u_4} {G : Type u_5} {V : Type u_6} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} (hπ : π.IsUnitary) : ∃ (C : ℝ), ∀ (g : G), ‖π g‖ ≤ C

The action operators of a unitary representation are uniformly bounded, in the form taken by the integrated-form API.

theorem ContRepresentation.IsUnitary.isometry {𝕜 : Type u_4} {G : Type u_5} {V : Type u_6} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} (hπ : π.IsUnitary) (g : G) : Isometry ⇑(π g)

Every action map of a unitary representation is an isometry.

theorem ContRepresentation.IsUnitary.injective {𝕜 : Type u_4} {G : Type u_5} {V : Type u_6} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} (hπ : π.IsUnitary) (g : G) : Function.Injective ⇑(π g)

Every action map of a unitary representation is injective.

theorem ContRepresentation.IsUnitary.restrict {𝕜 : Type u_4} {G : Type u_5} {V : Type u_6} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} {H : Type u_7} [Monoid H] (hπ : π.IsUnitary) (φ : H →* G) : (π.restrict φ).IsUnitary

Restriction along a monoid homomorphism preserves unitarity.

theorem ContRepresentation.IsUnitary.subrepresentation {𝕜 : Type u_4} {G : Type u_5} {V : Type u_6} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} (hπ : π.IsUnitary) {W : Submodule 𝕜 V} (hW : ∀ (g : G), ∀ v ∈ W, (π g) v ∈ W) : (π.subrepresentation W hW).IsUnitary

The restriction of a unitary representation to an invariant submodule is unitary.

theorem ContRepresentation.IsUnitary.norm_inner_map_le {𝕜 : Type u_4} {G : Type u_5} {V : Type u_6} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} (hπ : π.IsUnitary) (g : G) (v w : V) : ‖inner 𝕜 ((π g) v) w‖ ≤ ‖v‖ * ‖w‖

A matrix coefficient of a unitary representation is bounded by the product of the vector norms.

theorem ContRepresentation.IsUnitary.adjoint_comp_self {𝕜 : Type u_4} {G : Type u_5} {V : Type u_6} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} [CompleteSpace V] (hπ : π.IsUnitary) (g : G) : ContinuousLinearMap.adjoint (π g) ∘SL π g = 1

The adjoint of a unitary action operator is a left inverse.

theorem ContRepresentation.isUnitary_trivial {𝕜 : Type u_4} {G : Type u_5} {V : Type u_6} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] : (trivial 𝕜 G V).IsUnitary

The trivial continuous representation is unitary.

theorem ContRepresentation.isUnitary_iff_mem_unitary {𝕜 : Type u_4} {G : Type u_5} {V : Type u_6} [RCLike 𝕜] [Group G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) : π.IsUnitary ↔ ∀ (g : G), π g ∈ unitary (V →L[𝕜] V)

For a group representation, inner-product preservation is equivalent to every action operator belonging to Mathlib's unitary submonoid.

theorem ContRepresentation.IsUnitary.mem_unitary {𝕜 : Type u_4} {G : Type u_5} {V : Type u_6} [RCLike 𝕜] [Group G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] {π : ContRepresentation 𝕜 G V} (hπ : π.IsUnitary) (g : G) : π g ∈ unitary (V →L[𝕜] V)

Every action operator of a unitary group representation belongs to Mathlib's unitary submonoid.

theorem ContRepresentation.IsUnitary.self_comp_adjoint {𝕜 : Type u_4} {G : Type u_5} {V : Type u_6} [RCLike 𝕜] [Group G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] {π : ContRepresentation 𝕜 G V} (hπ : π.IsUnitary) (g : G) : π g ∘SL ContinuousLinearMap.adjoint (π g) = 1

The adjoint of a unitary action operator is a right inverse.

theorem ContRepresentation.IsUnitary.inner_map_left {𝕜 : Type u_4} {G : Type u_5} {V : Type u_6} [RCLike 𝕜] [Group G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} (hπ : π.IsUnitary) (g : G) (v w : V) : inner 𝕜 ((π g) v) w = inner 𝕜 v ((π g⁻¹) w)

Moving a unitary action from the first inner-product argument to the second replaces the group element by its inverse.

theorem ContRepresentation.IsUnitary.inner_map_right {𝕜 : Type u_4} {G : Type u_5} {V : Type u_6} [RCLike 𝕜] [Group G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} (hπ : π.IsUnitary) (g : G) (v w : V) : inner 𝕜 v ((π g) w) = inner 𝕜 ((π g⁻¹) v) w

Moving a unitary action from the second inner-product argument to the first replaces the group element by its inverse.

@[simp]

theorem ContRepresentation.IsUnitary.adjoint_eq_inv {𝕜 : Type u_4} {G : Type u_5} {V : Type u_6} [RCLike 𝕜] [Group G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] {π : ContRepresentation 𝕜 G V} (hπ : π.IsUnitary) (g : G) : ContinuousLinearMap.adjoint (π g) = π g⁻¹

The adjoint of a unitary action operator is the action of the inverse group element.