Continuous actions on C⋆-algebras

A CStarAction G A is a homomorphism into the complex star-algebra automorphisms of A whose orbits are norm-continuous. The algebra need not have an identity. Automorphisms are isometric, hence each one is a continuous complex linear map, and point-norm continuity implies joint continuity of evaluation. This is the continuity needed when an action is applied to a coefficient-valued convolution integrand.

Each automorphism of an action commutes with Bochner integrals.

Actions can be pulled back along continuous group homomorphisms and transported along star-algebra equivalences. The latter construction expresses conjugacy of dynamical systems. Membership in a subset invariant in the sense of Mathlib's IsInvariant is unchanged by the action.

The conventions follow Dana Williams, Crossed Products of C-Algebras*, Chapter 2. The joint-continuity argument uses Mathlib's StarAlgEquiv.isometry and continuous_prod_of_continuous_lipschitzWith'.

structure TauCeti.CStarAction (G : Type u_1) (A : Type u_2) [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] : Type (max u_1 u_2)

A point-norm continuous action on a possibly nonunital complex C⋆-algebra.

• toMonoidHom : G →* A ≃⋆ₐ[ℂ] A

  The homomorphism into star-algebra automorphisms.

• continuous_orbit (a : A) : Continuous fun (g : G) => (self.toMonoidHom g) a

  Continuity of every orbit in the norm topology.

@[instance_reducible]

instance TauCeti.CStarAction.instFunLikeStarAlgEquivComplex {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] : FunLike (CStarAction G A) G (A ≃⋆ₐ[ℂ] A)

theorem TauCeti.CStarAction.ext {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] {α β : CStarAction G A} (h : ∀ (g : G) (a : A), (α g) a = (β g) a) : α = β

Actions are determined by their values on group elements and coefficients.

theorem TauCeti.CStarAction.ext_iff {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] {α β : CStarAction G A} : α = β ↔ ∀ (g : G) (a : A), (α g) a = (β g) a

@[simp]

theorem TauCeti.CStarAction.toMonoidHom_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) (g : G) : α.toMonoidHom g = α g

@[simp]

theorem TauCeti.CStarAction.one_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) (a : A) : (α 1) a = a

theorem TauCeti.CStarAction.mul_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) (g h : G) (a : A) : (α (g * h)) a = (α g) ((α h) a)

The group product acts by composition, with the right factor acting first.

@[simp]

theorem TauCeti.CStarAction.inv_apply_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) (g : G) (a : A) : (α g⁻¹) ((α g) a) = a

@[simp]

theorem TauCeti.CStarAction.apply_inv_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) (g : G) (a : A) : (α g) ((α g⁻¹) a) = a

def TauCeti.CStarAction.toContinuousLinearMap {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) (g : G) : A →L[ℂ] A

The automorphism by which a group element acts, as a continuous complex linear map.

@[simp]

theorem TauCeti.CStarAction.toContinuousLinearMap_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) (g : G) (a : A) : (α.toContinuousLinearMap g) a = (α g) a

theorem TauCeti.CStarAction.integral_comp_comm {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) {X : Type u_3} [MeasurableSpace X] (ν : MeasureTheory.Measure X) (g : G) (F : X → A) : ∫ (x : X), (α g) (F x) ∂ν = (α g) (∫ (x : X), F x ∂ν)

Each automorphism of a C⋆-action commutes with Bochner integrals. No integrability is needed, since the automorphism is a linear isometry.

@[simp]

theorem IsInvariant.cstarAction_apply_mem_iff {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] {α : TauCeti.CStarAction G A} {s : Set A} (hs : IsInvariant (fun (g : G) (a : A) => (α g) a) s) (g : G) (a : A) : (α g) a ∈ s ↔ a ∈ s

Membership in an invariant subset is unchanged by the action.

theorem TauCeti.CStarAction.continuous {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) : Continuous fun (p : G × A) => (α p.1) p.2

Point-norm continuity implies joint continuity of the action.

theorem TauCeti.CStarAction.continuous_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) {X : Type u_3} [TopologicalSpace X] {g : X → G} {a : X → A} (hg : Continuous g) (ha : Continuous a) : Continuous fun (x : X) => (α (g x)) (a x)

Apply an action to two continuously varying arguments.

@[simp]

theorem TauCeti.CStarAction.symm_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) (g : G) (a : A) : (α g).symm a = (α g⁻¹) a

The inverse of an automorphism of the action is the action of the inverse element.

theorem TauCeti.CStarAction.continuous_inv_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) (a : A) : Continuous fun (g : G) => (α g⁻¹) a

Orbits through inverses are continuous. Continuity of inversion in G is not needed, since ‖α g⁻¹ a - α h⁻¹ a‖ = ‖α h b - α g b‖ for b = α h⁻¹ a.

def TauCeti.CStarAction.trivial {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] : CStarAction G A

The trivial action, including on the zero algebra.

@[simp]

theorem TauCeti.CStarAction.trivial_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (g : G) (a : A) : (trivial g) a = a

def TauCeti.CStarAction.comp {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] {H : Type u_3} [Group H] [TopologicalSpace H] (α : CStarAction G A) (φ : H →ₜ* G) : CStarAction H A

Pull back an action along a continuous homomorphism, in particular a subgroup inclusion.

@[simp]

theorem TauCeti.CStarAction.comp_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] {H : Type u_3} [Group H] [TopologicalSpace H] (α : CStarAction G A) (φ : H →ₜ* G) (h : H) (a : A) : ((α.comp φ) h) a = (α (φ h)) a

@[simp]

theorem TauCeti.CStarAction.comp_id {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) : α.comp (ContinuousMonoidHom.id G) = α

@[simp]

theorem TauCeti.CStarAction.comp_comp {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] {H : Type u_3} {K : Type u_4} [Group H] [TopologicalSpace H] [Group K] [TopologicalSpace K] (α : CStarAction G A) (φ : H →ₜ* G) (ψ : K →ₜ* H) : (α.comp φ).comp ψ = α.comp (φ.comp ψ)

def TauCeti.CStarAction.conjugate {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] {B : Type u_5} [NonUnitalCStarAlgebra B] (α : CStarAction G A) (e : A ≃⋆ₐ[ℂ] B) : CStarAction G B

Transport an action through a star-algebra equivalence: g acts by e ∘ α g ∘ e⁻¹.

@[simp]

theorem TauCeti.CStarAction.conjugate_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] {B : Type u_5} [NonUnitalCStarAlgebra B] (α : CStarAction G A) (e : A ≃⋆ₐ[ℂ] B) (g : G) (b : B) : ((α.conjugate e) g) b = e ((α g) (e.symm b))

@[simp]

theorem TauCeti.CStarAction.conjugate_refl {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) : α.conjugate (StarAlgEquiv.refl ℂ A) = α

theorem TauCeti.CStarAction.conjugate_conjugate {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] {B : Type u_5} {C : Type u_6} [NonUnitalCStarAlgebra B] [NonUnitalCStarAlgebra C] (α : CStarAction G A) (e : A ≃⋆ₐ[ℂ] B) (f : B ≃⋆ₐ[ℂ] C) : (α.conjugate e).conjugate f = α.conjugate (e.trans f)

Successive conjugacies equal conjugacy along the composite equivalence.

@[simp]

theorem TauCeti.CStarAction.conjugate_symm {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] {B : Type u_5} [NonUnitalCStarAlgebra B] (α : CStarAction G A) (e : A ≃⋆ₐ[ℂ] B) : (α.conjugate e).conjugate e.symm = α

Transporting an action back along the inverse equivalence recovers it.

theorem TauCeti.CStarAction.conjugate_comp {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] {H : Type u_3} [Group H] [TopologicalSpace H] {B : Type u_5} [NonUnitalCStarAlgebra B] (α : CStarAction G A) (e : A ≃⋆ₐ[ℂ] B) (φ : H →ₜ* G) : (α.conjugate e).comp φ = (α.comp φ).conjugate e

Pullback in the group and conjugacy in the algebra commute.