The right regular representation on the pre-GNS space

theorem CommutingRepetition.Density.norm_sq_mul_le {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (hτ : ∀ (a b : 𝒞), τ (a * b) = τ (b * a)) (a x : 𝒞) : τ (star (x * a) * (x * a)) ≤ ↑(‖a‖ ^ 2) * τ (star x * x)

The bound ‖x a‖_τ ≤ ‖a‖ ‖x‖_τ for right multiplication, from traciality.

noncomputable def CommutingRepetition.Density.rightMulMapPreGNS {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (hτ : ∀ (a b : 𝒞), τ (a * b) = τ (b * a)) (a : 𝒞) : τ.PreGNS →L[ℂ] τ.PreGNS

Right multiplication by a on the pre-GNS space of a tracial state.

Equations

• CommutingRepetition.Density.rightMulMapPreGNS τ hτ a = (↑τ.toPreGNS ∘ₗ LinearMap.mulRight ℂ a ∘ₗ ↑τ.ofPreGNS).mkContinuous ‖a‖ ⋯

theorem CommutingRepetition.Density.rightMulMapPreGNS_apply {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (hτ : ∀ (a b : 𝒞), τ (a * b) = τ (b * a)) (a : 𝒞) (x : τ.PreGNS) : (rightMulMapPreGNS τ hτ a) x = τ.toPreGNS (τ.ofPreGNS x * a)

noncomputable def CommutingRepetition.Density.rightMul {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (hτ : ∀ (a b : 𝒞), τ (a * b) = τ (b * a)) (a : 𝒞) : τ.GNS →L[ℂ] τ.GNS

The right regular representation on the GNS space.

Equations

• CommutingRepetition.Density.rightMul τ hτ a = (CommutingRepetition.Density.rightMulMapPreGNS τ hτ a).completion

theorem CommutingRepetition.Density.rightMul_apply_coe {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (hτ : ∀ (a b : 𝒞), τ (a * b) = τ (b * a)) (a : 𝒞) (x : τ.PreGNS) : (rightMul τ hτ a) ↑x = ↑(τ.toPreGNS (τ.ofPreGNS x * a))

theorem CommutingRepetition.Density.rightMul_mul {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (hτ : ∀ (a b : 𝒞), τ (a * b) = τ (b * a)) (a b : 𝒞) : rightMul τ hτ (a * b) = rightMul τ hτ b * rightMul τ hτ a

theorem CommutingRepetition.Density.rightMul_one {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (hτ : ∀ (a b : 𝒞), τ (a * b) = τ (b * a)) : rightMul τ hτ 1 = 1

theorem CommutingRepetition.Density.rightMul_add {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (hτ : ∀ (a b : 𝒞), τ (a * b) = τ (b * a)) (a b : 𝒞) : rightMul τ hτ (a + b) = rightMul τ hτ a + rightMul τ hτ b

theorem CommutingRepetition.Density.rightMul_smul {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (hτ : ∀ (a b : 𝒞), τ (a * b) = τ (b * a)) (c : ℂ) (a : 𝒞) : rightMul τ hτ (c • a) = c • rightMul τ hτ a

theorem CommutingRepetition.Density.rightMul_star {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (hτ : ∀ (a b : 𝒞), τ (a * b) = τ (b * a)) (a : 𝒞) : rightMul τ hτ (star a) = star (rightMul τ hτ a)

⟪x a, y⟫ = ⟪x, y a*⟫: the adjoint of right multiplication by a is right multiplication by a* (uses traciality).

noncomputable def CommutingRepetition.Density.rightHom {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (hτ : ∀ (a b : 𝒞), τ (a * b) = τ (b * a)) : 𝒞ᵐᵒᵖ →⋆ₐ[ℂ] τ.GNS →L[ℂ] τ.GNS

The right regular representation as a unital star-algebra homomorphism from the opposite algebra.

Equations

• One or more equations did not get rendered due to their size.

theorem CommutingRepetition.Density.rightHom_apply {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (hτ : ∀ (a b : 𝒞), τ (a * b) = τ (b * a)) (a : 𝒞) : (rightHom τ hτ) (MulOpposite.op a) = rightMul τ hτ a

The standard tracial algebra of a tracial state

noncomputable def CommutingRepetition.Density.ιGNS {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) : 𝒞 →ₗ[ℂ] τ.GNS

The GNS embedding 𝒞 → L²(𝒞, τ) as a linear map.

Equations

• CommutingRepetition.Density.ιGNS τ = ↑UniformSpace.Completion.toComplL ∘ₗ ↑τ.toPreGNS

theorem CommutingRepetition.Density.ιGNS_apply {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (a : 𝒞) : (ιGNS τ) a = ↑(τ.toPreGNS a)

theorem CommutingRepetition.Density.denseRange_ιGNS {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) : DenseRange ⇑(ιGNS τ)

theorem CommutingRepetition.Density.inner_ιGNS {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (a b : 𝒞) : inner ℂ ((ιGNS τ) a) ((ιGNS τ) b) = τ (star a * b)

theorem CommutingRepetition.Density.gns_apply_ιGNS {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (a b : 𝒞) : (τ.gnsStarAlgHom a) ((ιGNS τ) b) = (ιGNS τ) (a * b)

theorem CommutingRepetition.Density.rightMul_ιGNS {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (hτ : ∀ (a b : 𝒞), τ (a * b) = τ (b * a)) (a b : 𝒞) : (rightMul τ hτ a) ((ιGNS τ) b) = (ιGNS τ) (b * a)

noncomputable def CommutingRepetition.Density.ofTracialState {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (hτ1 : τ 1 = 1) (hτ : ∀ (a b : 𝒞), τ (a * b) = τ (b * a)) : StdTracialAlgebra

The standard tracial algebra of a tracial state on a unital C*-algebra: the GNS space with the left and right regular representations.

Equations

• One or more equations did not get rendered due to their size.

theorem CommutingRepetition.Density.ofTracialState_A {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (hτ1 : τ 1 = 1) (hτ : ∀ (a b : 𝒞), τ (a * b) = τ (b * a)) : (ofTracialState τ hτ1 hτ).A = 𝒞

theorem CommutingRepetition.Density.ofTracialState_H {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (hτ1 : τ 1 = 1) (hτ : ∀ (a b : 𝒞), τ (a * b) = τ (b * a)) : (ofTracialState τ hτ1 hτ).H = τ.GNS

theorem CommutingRepetition.Density.ofTracialState_τ {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (hτ1 : τ 1 = 1) (hτ : ∀ (a b : 𝒞), τ (a * b) = τ (b * a)) (a : 𝒞) : (ofTracialState τ hτ1 hτ).τ a = τ a

theorem CommutingRepetition.Density.ofTracialState_ι {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (hτ1 : τ 1 = 1) (hτ : ∀ (a b : 𝒞), τ (a * b) = τ (b * a)) (a : 𝒞) : (ofTracialState τ hτ1 hτ).ι a = (ιGNS τ) a

theorem CommutingRepetition.Density.ofTracialState_L {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (hτ1 : τ 1 = 1) (hτ : ∀ (a b : 𝒞), τ (a * b) = τ (b * a)) (a : 𝒞) : (ofTracialState τ hτ1 hτ).L a = τ.gnsStarAlgHom a

theorem CommutingRepetition.Density.ofTracialState_Rop {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (hτ1 : τ 1 = 1) (hτ : ∀ (a b : 𝒞), τ (a * b) = τ (b * a)) (a : 𝒞) : (ofTracialState τ hτ1 hτ).Rop a = rightMul τ hτ a

theorem CommutingRepetition.Density.isPosElem_of_nonneg {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] {σ : 𝒞} (hσ : 0 ≤ σ) : IsPosElem σ

Positive elements of a C*-algebra are algebraically positive (single squares).

theorem CommutingRepetition.Density.rightMul_isPositive {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (hτ : ∀ (a b : 𝒞), τ (a * b) = τ (b * a)) {f : 𝒞} (hf : 0 ≤ f) : (rightMul τ hτ f).IsPositive

The right action of a positive element is a positive operator.

theorem CommutingRepetition.Density.rightMul_sum {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (hτ : ∀ (a b : 𝒞), τ (a * b) = τ (b * a)) {ι : Type u_1} (s : Finset ι) (f : ι → 𝒞) : rightMul τ hτ (∑ i ∈ s, f i) = ∑ i ∈ s, rightMul τ hτ (f i)