Covariant representations of C⋆-actions

A covariant representation consists of a possibly degenerate coefficient representation and a strongly continuous unitary group representation, satisfying U g (π a v) = π (α g a) (U g v). Strong continuity is imposed separately from ContRepresentation, which only makes each individual operator continuous. These data admit vector-valued integrated forms without assuming operator-norm continuity of the group representation.

The conventions follow Dana Williams, Crossed Products of C-Algebras*, Chapter 2.

structure TauCeti.CStarAction.CovariantRepresentation {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : Type (max (max u_1 u_2) u_4)

A covariant pair for a point-norm continuous action on a possibly nonunital C⋆-algebra. The coefficient representation is not required to be nondegenerate.

• coefficient : A →⋆ₙₐ[ℂ] H →L[ℂ] H

  The coefficient representation.

• group : ContRepresentation ℂ G H

  The group representation by bounded operators.

• isUnitary : self.group.IsUnitary

  Each group operator preserves the inner product.

• continuous_orbit (v : H) : Continuous fun (g : G) => (self.group g) v

  Every group orbit is continuous in the Hilbert-space norm.

• covariance (g : G) (a : A) (v : H) : (self.group g) ((self.coefficient a) v) = (self.coefficient ((α g) a)) ((self.group g) v)

  Covariance of the coefficient and group representations.

theorem TauCeti.CStarAction.CovariantRepresentation.ext {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {α : CStarAction G A} {P Q : α.CovariantRepresentation H} (hπ : P.coefficient = Q.coefficient) (hU : P.group = Q.group) : P = Q

The coefficient and group representations determine a covariant pair.

theorem TauCeti.CStarAction.CovariantRepresentation.ext_iff {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {α : CStarAction G A} {P Q : α.CovariantRepresentation H} : P = Q ↔ P.coefficient = Q.coefficient ∧ P.group = Q.group

@[simp]

theorem TauCeti.CStarAction.CovariantRepresentation.group_mul_coefficient {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {α : CStarAction G A} (P : α.CovariantRepresentation H) (g : G) (a : A) : P.group g * P.coefficient a = P.coefficient ((α g) a) * P.group g

Covariance as an equality of bounded operators.

theorem TauCeti.CStarAction.CovariantRepresentation.coefficient_action {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {α : CStarAction G A} (P : α.CovariantRepresentation H) (g : G) (a : A) : P.coefficient ((α g) a) = P.group g * P.coefficient a * P.group g⁻¹

The coefficient at a transformed element is obtained by unitary conjugation.

def TauCeti.CStarAction.CovariantRepresentation.trivial {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : A →⋆ₙₐ[ℂ] H →L[ℂ] H) : CStarAction.trivial.CovariantRepresentation H

Every coefficient representation gives a covariant pair for the trivial action, with trivial group representation.

@[simp]

theorem TauCeti.CStarAction.CovariantRepresentation.trivial_coefficient {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : A →⋆ₙₐ[ℂ] H →L[ℂ] H) : (trivial π).coefficient = π

@[simp]

theorem TauCeti.CStarAction.CovariantRepresentation.trivial_group {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : A →⋆ₙₐ[ℂ] H →L[ℂ] H) : (trivial π).group = ContRepresentation.trivial ℂ G H