noncomputable def CommutingRepetition.StdTracialAlgebra.envAlg (M : StdTracialAlgebra) : StarSubalgebra ℂ (M.H →L[ℂ] M.H)

The C*-envelope: the norm closure of the left representation's range in B(L²(M)).

Equations

• M.envAlg = M.L.range.topologicalClosure

theorem CommutingRepetition.StdTracialAlgebra.isClosed_envAlg (M : StdTracialAlgebra) : IsClosed ↑M.envAlg

theorem CommutingRepetition.StdTracialAlgebra.L_mem_envAlg (M : StdTracialAlgebra) (a : M.A) : M.L a ∈ M.envAlg

theorem CommutingRepetition.StdTracialAlgebra.range_subset_envAlg (M : StdTracialAlgebra) : Set.range ⇑M.L ⊆ ↑M.envAlg

theorem CommutingRepetition.StdTracialAlgebra.envAlg_carrier_eq_closure (M : StdTracialAlgebra) : ↑M.envAlg = closure ↑M.L.range

noncomputable def CommutingRepetition.StdTracialAlgebra.traceState (M : StdTracialAlgebra) (T : M.H →L[ℂ] M.H) : ℂ

The trace-vector state on all of B(L²(M)): φ(T) = ⟪Ω_τ, T Ω_τ⟫. On the envelope it extends M.τ.

Equations

• M.traceState T = inner ℂ M.traceVector (T M.traceVector)

theorem CommutingRepetition.StdTracialAlgebra.traceState_L (M : StdTracialAlgebra) (a : M.A) : M.traceState (M.L a) = M.τ a

theorem CommutingRepetition.StdTracialAlgebra.norm_traceVector (M : StdTracialAlgebra) : ‖M.traceVector‖ = 1

theorem CommutingRepetition.StdTracialAlgebra.continuous_traceState (M : StdTracialAlgebra) : Continuous M.traceState

theorem CommutingRepetition.StdTracialAlgebra.traceState_star_mul_self (M : StdTracialAlgebra) (T : M.H →L[ℂ] M.H) : M.traceState (star T * T) = ↑‖T M.traceVector‖ ^ 2

The trace-vector state is positive: φ(T*T) = ‖T Ω‖² ≥ 0.

theorem CommutingRepetition.StdTracialAlgebra.traceState_mul_comm (M : StdTracialAlgebra) {T S : M.H →L[ℂ] M.H} (hT : T ∈ M.envAlg) (hS : S ∈ M.envAlg) : M.traceState (T * S) = M.traceState (S * T)

Traciality on the envelope (density + continuity): for T, S ∈ envAlg, φ(TS) = φ(ST).

theorem CommutingRepetition.StdTracialAlgebra.smul_one_mem_envAlg (M : StdTracialAlgebra) (c : ℂ) : c • 1 ∈ M.envAlg

theorem CommutingRepetition.StdTracialAlgebra.traceState_smul (M : StdTracialAlgebra) (c : ℂ) (T : M.H →L[ℂ] M.H) : M.traceState (c • T) = c * M.traceState T

theorem CommutingRepetition.StdTracialAlgebra.traceState_sub (M : StdTracialAlgebra) (T S : M.H →L[ℂ] M.H) : M.traceState (T - S) = M.traceState T - M.traceState S

theorem CommutingRepetition.StdTracialAlgebra.norm_mul_traceVector_le (M : StdTracialAlgebra) {U T : M.H →L[ℂ] M.H} (hU : U ∈ M.envAlg) (hT : T ∈ M.envAlg) : ‖(U * T) M.traceVector‖ ≤ ‖T‖ * ‖U M.traceVector‖

The trace inequality (the boundedness engine for the right regular representation): for U, T in the envelope, ‖(U T) Ω‖ ≤ ‖T‖ · ‖U Ω‖. Traciality moves the T-square to the other side (φ(T* U*U T) = φ(U*U · TT*)), the C*-gap ‖TT*‖·1 − TT* has a CFC.sqrt in the envelope (cfc_mem on the closed star subalgebra), and positivity of the state on envelope squares finishes.

noncomputable def CommutingRepetition.StdTracialAlgebra.evalΩ (M : StdTracialAlgebra) : (M.H →L[ℂ] M.H) →ₗ[ℂ] M.H

Evaluation at the trace vector, as a linear map on B(L²(M)).

Equations

• M.evalΩ = { toFun := fun (T : M.H →L[ℂ] M.H) => T M.traceVector, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def CommutingRepetition.StdTracialAlgebra.envOrbit (M : StdTracialAlgebra) : Submodule ℂ M.H

The envelope orbit of the trace vector: {S Ω ∣ S ∈ envAlg}, a dense submodule of L²(M) (it contains the range of M.ι).

Equations

• M.envOrbit = Submodule.map M.evalΩ (Subalgebra.toSubmodule M.envAlg.toSubalgebra)

theorem CommutingRepetition.StdTracialAlgebra.mem_envOrbit_iff (M : StdTracialAlgebra) {v : M.H} : v ∈ M.envOrbit ↔ ∃ T ∈ M.envAlg, T M.traceVector = v

theorem CommutingRepetition.StdTracialAlgebra.range_ι_subset_envOrbit (M : StdTracialAlgebra) : Set.range ⇑M.ι ⊆ ↑M.envOrbit

theorem CommutingRepetition.StdTracialAlgebra.envOrbit_dense (M : StdTracialAlgebra) : Dense ↑M.envOrbit

theorem CommutingRepetition.StdTracialAlgebra.rightMul_welldef (M : StdTracialAlgebra) {P Q T : M.H →L[ℂ] M.H} (hP : P ∈ M.envAlg) (hQ : Q ∈ M.envAlg) (hT : T ∈ M.envAlg) (hPQ : P M.traceVector = Q M.traceVector) : (P * T) M.traceVector = (Q * T) M.traceVector

Well-definedness of right multiplication on the orbit: if two envelope elements agree at the trace vector, so do their right translates (the trace inequality applied to the difference).

noncomputable def CommutingRepetition.StdTracialAlgebra.orbitRep (M : StdTracialAlgebra) (v : ↥M.envOrbit) : M.H →L[ℂ] M.H

A representative of an orbit element: an envelope operator whose value at the trace vector is the given vector (choice; unique up to rightMul_welldef).

Equations

• M.orbitRep v = ⋯.choose

theorem CommutingRepetition.StdTracialAlgebra.orbitRep_mem (M : StdTracialAlgebra) (v : ↥M.envOrbit) : M.orbitRep v ∈ M.envAlg

theorem CommutingRepetition.StdTracialAlgebra.orbitRep_apply (M : StdTracialAlgebra) (v : ↥M.envOrbit) : (M.orbitRep v) M.traceVector = ↑v

noncomputable def CommutingRepetition.StdTracialAlgebra.rightMulOrbit (M : StdTracialAlgebra) (T : ↥M.envAlg) : ↥M.envOrbit →L[ℂ] M.H

Right translation on the orbit: S Ω ↦ (S T) Ω, well-defined by rightMul_welldef and bounded by the trace inequality.

Equations

• M.rightMulOrbit T = { toFun := fun (v : ↥M.envOrbit) => (M.orbitRep v * ↑T) M.traceVector, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous ‖↑T‖ ⋯

theorem CommutingRepetition.StdTracialAlgebra.denseRange_subtypeL_envOrbit (M : StdTracialAlgebra) : DenseRange ⇑M.envOrbit.subtypeL

theorem CommutingRepetition.StdTracialAlgebra.isUniformInducing_subtypeL_envOrbit (M : StdTracialAlgebra) : IsUniformInducing ⇑M.envOrbit.subtypeL

noncomputable def CommutingRepetition.StdTracialAlgebra.envRight (M : StdTracialAlgebra) (T : ↥M.envAlg) : M.H →L[ℂ] M.H

The right regular representation of the envelope: the unique bounded extension of S Ω ↦ (S T) Ω along the dense orbit.

Equations

• M.envRight T = (M.rightMulOrbit T).extend M.envOrbit.subtypeL

theorem CommutingRepetition.StdTracialAlgebra.envRight_apply (M : StdTracialAlgebra) (T : ↥M.envAlg) {P : M.H →L[ℂ] M.H} (hP : P ∈ M.envAlg) : (M.envRight T) (P M.traceVector) = (P * ↑T) M.traceVector

The defining property of envRight on the orbit.

theorem CommutingRepetition.StdTracialAlgebra.eq_of_eq_on_orbit (M : StdTracialAlgebra) {F G : M.H →L[ℂ] M.H} (h : ∀ P ∈ M.envAlg, F (P M.traceVector) = G (P M.traceVector)) : F = G

Two operators agreeing on the dense orbit are equal.

theorem CommutingRepetition.StdTracialAlgebra.inner_traceVector (M : StdTracialAlgebra) (A B : M.H →L[ℂ] M.H) : inner ℂ (A M.traceVector) (B M.traceVector) = M.traceState (star A * B)

theorem CommutingRepetition.StdTracialAlgebra.traceState_add (M : StdTracialAlgebra) (T S : M.H →L[ℂ] M.H) : M.traceState (T + S) = M.traceState T + M.traceState S

theorem CommutingRepetition.StdTracialAlgebra.traceState_one (M : StdTracialAlgebra) : M.traceState 1 = 1

theorem CommutingRepetition.StdTracialAlgebra.traceState_star (M : StdTracialAlgebra) (T : M.H →L[ℂ] M.H) : M.traceState (star T) = star (M.traceState T)

theorem CommutingRepetition.StdTracialAlgebra.envRight_one (M : StdTracialAlgebra) : M.envRight 1 = 1

theorem CommutingRepetition.StdTracialAlgebra.envRight_mul (M : StdTracialAlgebra) (T T' : ↥M.envAlg) : M.envRight (T * T') = M.envRight T' ∘SL M.envRight T

theorem CommutingRepetition.StdTracialAlgebra.envRight_add (M : StdTracialAlgebra) (T T' : ↥M.envAlg) : M.envRight (T + T') = M.envRight T + M.envRight T'

theorem CommutingRepetition.StdTracialAlgebra.envRight_smul (M : StdTracialAlgebra) (c : ℂ) (T : ↥M.envAlg) : M.envRight (c • T) = c • M.envRight T

theorem CommutingRepetition.StdTracialAlgebra.envRight_star (M : StdTracialAlgebra) (T : ↥M.envAlg) : M.envRight (star T) = star (M.envRight T)

theorem CommutingRepetition.StdTracialAlgebra.left_envRight_commute (M : StdTracialAlgebra) (S T : ↥M.envAlg) : ↑S * M.envRight T = M.envRight T * ↑S

noncomputable def CommutingRepetition.StdTracialAlgebra.envModel (M : StdTracialAlgebra) : StdTracialAlgebra

The envelope model (Stage B, WP-B4): the C*-envelope of the left representation as a standard tracial algebra on the same GNS space. Its elements are norm limits of left multiplications, its trace is the trace-vector state (tracial by density), its ι is evaluation at the trace vector (dense by M.ι_dense), its left representation is the subalgebra inclusion, and its right representation is the extended right regular representation envRight. Continuous functional calculus operates on its elements through B(L²(M)) with cfc_mem keeping outputs in the envelope — the algebra in which the resolver-corner construction (nodes 1.2.5.x) runs.

Equations

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

theorem CommutingRepetition.StdTracialAlgebra.envModel_τ_L (M : StdTracialAlgebra) (a : M.A) : M.envModel.τ ⟨M.L a, ⋯⟩ = M.τ a

The envelope trace extends the original trace through the left representation.