Generators of C⋆-algebra actions

The generator of a point-norm continuous real action on a possibly nonunital C⋆-algebra is a closed, densely defined complex LinearPMap. Its domain is a nonunital star subalgebra, and the generator satisfies the Leibniz rule and commutes with star. The domain is invariant under the action, which commutes with the generator.

Time is written as Multiplicative ℝ to use the existing CStarAction interface. The construction uses StronglyContinuousGroup and its forward semigroup's complexGenerator to connect the derivation with the existing unbounded-operator API. Domain membership is characterized by differentiability of the orbit at zero.

References

Bratteli--Robinson, Operator Algebras and Quantum Statistical Mechanics 2, second edition, Section 5.3, for generators of one-parameter automorphism groups.

noncomputable def TauCeti.CStarAction.toStronglyContinuousGroup {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) : Semigroups.StronglyContinuousGroup A

A continuous real C⋆-action, viewed as a strongly continuous group of real operators.

@[simp]

theorem TauCeti.CStarAction.toStronglyContinuousGroup_apply {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (t : ℝ) (a : A) : (α.toStronglyContinuousGroup t) a = (α (Multiplicative.ofAdd t)) a

theorem TauCeti.CStarAction.toStronglyContinuousGroup_isComplexLinear {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) : α.toStronglyContinuousGroup.toSemigroup.IsComplexLinear

The operators of a C⋆-action are complex linear.

noncomputable def TauCeti.CStarAction.generator {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) : A →ₗ.[ℂ] A

The infinitesimal generator of a real C⋆-action, as a complex linear partial map.

theorem TauCeti.CStarAction.generator_def {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) : α.generator = α.toStronglyContinuousGroup.toSemigroup.complexGenerator ⋯

@[simp]

theorem TauCeti.CStarAction.generator_restrictScalars {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) : LinearPMap.restrictScalars ℝ α.generator = α.toStronglyContinuousGroup.generator

Restricting the generator to real scalars recovers the underlying group generator.

theorem TauCeti.CStarAction.hasDerivAt_zero {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (a : ↥α.generator.domain) : HasDerivAt (fun (t : ℝ) => (α (Multiplicative.ofAdd t)) ↑a) (↑α.generator a) 0

Every orbit of a domain element is differentiable at zero with derivative its generator.

theorem TauCeti.CStarAction.mem_generator_domain_iff_differentiableAt {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (a : A) : a ∈ α.generator.domain ↔ DifferentiableAt ℝ (fun (t : ℝ) => (α (Multiplicative.ofAdd t)) a) 0

An element belongs to the generator domain exactly when its orbit is differentiable at zero.

theorem TauCeti.CStarAction.generator_eq_of_hasDerivAt {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) {a b : A} (ha : a ∈ α.generator.domain) (h : HasDerivAt (fun (t : ℝ) => (α (Multiplicative.ofAdd t)) a) b 0) : ↑α.generator ⟨a, ha⟩ = b

Any derivative of an orbit at zero is its generator value.

theorem TauCeti.CStarAction.dense_generator_domain {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) : Dense ↑α.generator.domain

The generator domain is norm dense.

theorem TauCeti.CStarAction.isClosed_generator {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) : α.generator.IsClosed

The infinitesimal generator is closed in the norm topology.

theorem TauCeti.CStarAction.hasDerivAt {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (a : ↥α.generator.domain) (t : ℝ) : HasDerivAt (fun (s : ℝ) => (α (Multiplicative.ofAdd s)) ↑a) ((α (Multiplicative.ofAdd t)) (↑α.generator a)) t

At every real time the derivative of an orbit is the action on its generator value.

theorem TauCeti.CStarAction.mul_mem_generator_domain {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) {a b : A} (ha : a ∈ α.generator.domain) (hb : b ∈ α.generator.domain) : a * b ∈ α.generator.domain

The generator domain is closed under multiplication.

@[simp]

theorem TauCeti.CStarAction.generator_mul {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (a b : ↥α.generator.domain) : ↑α.generator ⟨↑a * ↑b, ⋯⟩ = ↑α.generator a * ↑b + ↑a * ↑α.generator b

The infinitesimal generator satisfies the Leibniz rule.

theorem TauCeti.CStarAction.star_mem_generator_domain {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) {a : A} (ha : a ∈ α.generator.domain) : star a ∈ α.generator.domain

The generator domain is closed under star.

@[simp]

theorem TauCeti.CStarAction.star_mem_generator_domain_iff {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (a : A) : star a ∈ α.generator.domain ↔ a ∈ α.generator.domain

Star preserves the generator domain in both directions.

@[simp]

theorem TauCeti.CStarAction.generator_star {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (a : ↥α.generator.domain) : ↑α.generator ⟨star ↑a, ⋯⟩ = star (↑α.generator a)

The infinitesimal generator commutes with star.

noncomputable def TauCeti.CStarAction.generatorDomain {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) : NonUnitalStarSubalgebra ℂ A

The generator domain as a complex nonunital star subalgebra of the ambient algebra.

@[simp]

theorem TauCeti.CStarAction.mem_generatorDomain {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (a : A) : a ∈ α.generatorDomain ↔ a ∈ α.generator.domain

@[simp]

theorem TauCeti.CStarAction.generatorDomain_toSubmodule {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) : α.generatorDomain.toSubmodule = α.generator.domain

theorem TauCeti.CStarAction.apply_mem_generator_domain {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) {a : A} (ha : a ∈ α.generator.domain) (t : ℝ) : (α (Multiplicative.ofAdd t)) a ∈ α.generator.domain

The generator domain is invariant under every time of the action.

@[simp]

theorem TauCeti.CStarAction.apply_mem_generator_domain_iff {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (t : ℝ) (a : A) : (α (Multiplicative.ofAdd t)) a ∈ α.generator.domain ↔ a ∈ α.generator.domain

Acting at any real time preserves membership in the generator domain in both directions.

theorem TauCeti.CStarAction.generator_apply_action {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (a : ↥α.generator.domain) (t : ℝ) : ↑α.generator ⟨(α (Multiplicative.ofAdd t)) ↑a, ⋯⟩ = (α (Multiplicative.ofAdd t)) (↑α.generator a)

The action commutes with its infinitesimal generator on the invariant domain.

@[simp]

theorem TauCeti.CStarAction.one_mem_generator_domain {B : Type u_2} [CStarAlgebra B] (α : CStarAction (Multiplicative ℝ) B) : 1 ∈ α.generator.domain

In a unital algebra the identity belongs to the generator domain.

@[simp]

theorem TauCeti.CStarAction.generator_one {B : Type u_2} [CStarAlgebra B] (α : CStarAction (Multiplicative ℝ) B) : ↑α.generator ⟨1, ⋯⟩ = 0

The generator of a unital action vanishes at the identity.