structure CommutingRepetition.StdTracialAlgebra.TracialSub (M : StdTracialAlgebra) : Type u

A closed star subalgebra of B(L²(M)) containing the left representation on which the trace-vector state is tracial.

• S : StarSubalgebra ℂ (M.H →L[ℂ] M.H)
• isClosed : IsClosed ↑self.S
• L_mem (a : M.A) : M.L a ∈ self.S
• tracial {T U : M.H →L[ℂ] M.H} : T ∈ self.S → U ∈ self.S → M.traceState (T * U) = M.traceState (U * T)

theorem CommutingRepetition.StdTracialAlgebra.TracialSub.smul_one_mem {M : StdTracialAlgebra} (D : M.TracialSub) (c : ℂ) : c • 1 ∈ D.S

theorem CommutingRepetition.StdTracialAlgebra.TracialSub.norm_mul_traceVector_le {M : StdTracialAlgebra} (D : M.TracialSub) {U T : M.H →L[ℂ] M.H} (hU : U ∈ D.S) (hT : T ∈ D.S) : ‖(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.TracialSub.evalΩ {M : StdTracialAlgebra} : (M.H →L[ℂ] M.H) →ₗ[ℂ] M.H

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

Equations

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

noncomputable def CommutingRepetition.StdTracialAlgebra.TracialSub.orbit {M : StdTracialAlgebra} (D : M.TracialSub) : 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

• D.orbit = Submodule.map M.evalΩ (Subalgebra.toSubmodule D.S.toSubalgebra)

theorem CommutingRepetition.StdTracialAlgebra.TracialSub.mem_orbit_iff {M : StdTracialAlgebra} (D : M.TracialSub) {v : M.H} : v ∈ D.orbit ↔ ∃ T ∈ D.S, T M.traceVector = v

theorem CommutingRepetition.StdTracialAlgebra.TracialSub.range_ι_subset_orbit {M : StdTracialAlgebra} (D : M.TracialSub) : Set.range ⇑M.ι ⊆ ↑D.orbit

theorem CommutingRepetition.StdTracialAlgebra.TracialSub.orbit_dense {M : StdTracialAlgebra} (D : M.TracialSub) : Dense ↑D.orbit

theorem CommutingRepetition.StdTracialAlgebra.TracialSub.rightMul_welldef {M : StdTracialAlgebra} (D : M.TracialSub) {P Q T : M.H →L[ℂ] M.H} (hP : P ∈ D.S) (hQ : Q ∈ D.S) (hT : T ∈ D.S) (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.TracialSub.orbitRep {M : StdTracialAlgebra} (D : M.TracialSub) (v : ↥D.orbit) : 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

• D.orbitRep v = ⋯.choose

theorem CommutingRepetition.StdTracialAlgebra.TracialSub.orbitRep_mem {M : StdTracialAlgebra} (D : M.TracialSub) (v : ↥D.orbit) : D.orbitRep v ∈ D.S

theorem CommutingRepetition.StdTracialAlgebra.TracialSub.orbitRep_apply {M : StdTracialAlgebra} (D : M.TracialSub) (v : ↥D.orbit) : (D.orbitRep v) M.traceVector = ↑v

noncomputable def CommutingRepetition.StdTracialAlgebra.TracialSub.rightMulOrbit {M : StdTracialAlgebra} (D : M.TracialSub) (T : ↥D.S) : ↥D.orbit →L[ℂ] M.H

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

Equations

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

theorem CommutingRepetition.StdTracialAlgebra.TracialSub.denseRange_subtypeL_orbit {M : StdTracialAlgebra} (D : M.TracialSub) : DenseRange ⇑D.orbit.subtypeL

theorem CommutingRepetition.StdTracialAlgebra.TracialSub.isUniformInducing_subtypeL_orbit {M : StdTracialAlgebra} (D : M.TracialSub) : IsUniformInducing ⇑D.orbit.subtypeL

noncomputable def CommutingRepetition.StdTracialAlgebra.TracialSub.right {M : StdTracialAlgebra} (D : M.TracialSub) (T : ↥D.S) : 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

• D.right T = (D.rightMulOrbit T).extend D.orbit.subtypeL

theorem CommutingRepetition.StdTracialAlgebra.TracialSub.right_apply {M : StdTracialAlgebra} (D : M.TracialSub) (T : ↥D.S) {P : M.H →L[ℂ] M.H} (hP : P ∈ D.S) : (D.right T) (P M.traceVector) = (P * ↑T) M.traceVector

The defining property of envRight on the orbit.

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

Two operators agreeing on the dense orbit are equal.

theorem CommutingRepetition.StdTracialAlgebra.TracialSub.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.TracialSub.traceState_add {M : StdTracialAlgebra} (T S : M.H →L[ℂ] M.H) : M.traceState (T + S) = M.traceState T + M.traceState S

theorem CommutingRepetition.StdTracialAlgebra.TracialSub.traceState_one {M : StdTracialAlgebra} : M.traceState 1 = 1

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

theorem CommutingRepetition.StdTracialAlgebra.TracialSub.right_one {M : StdTracialAlgebra} (D : M.TracialSub) : D.right 1 = 1

theorem CommutingRepetition.StdTracialAlgebra.TracialSub.right_mul {M : StdTracialAlgebra} (D : M.TracialSub) (T T' : ↥D.S) : D.right (T * T') = D.right T' ∘SL D.right T

theorem CommutingRepetition.StdTracialAlgebra.TracialSub.right_add {M : StdTracialAlgebra} (D : M.TracialSub) (T T' : ↥D.S) : D.right (T + T') = D.right T + D.right T'

theorem CommutingRepetition.StdTracialAlgebra.TracialSub.right_smul {M : StdTracialAlgebra} (D : M.TracialSub) (c : ℂ) (T : ↥D.S) : D.right (c • T) = c • D.right T

theorem CommutingRepetition.StdTracialAlgebra.TracialSub.right_star {M : StdTracialAlgebra} (D : M.TracialSub) (T : ↥D.S) : D.right (star T) = star (D.right T)

theorem CommutingRepetition.StdTracialAlgebra.TracialSub.left_right_commute {M : StdTracialAlgebra} (D : M.TracialSub) (S T : ↥D.S) : ↑S * D.right T = D.right T * ↑S

noncomputable def CommutingRepetition.StdTracialAlgebra.TracialSub.model {M : StdTracialAlgebra} (D : M.TracialSub) : 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.TracialSub.model_τ {M : StdTracialAlgebra} (D : M.TracialSub) (T : ↥D.S) : D.model.τ T = M.traceState ↑T

theorem CommutingRepetition.StdTracialAlgebra.TracialSub.model_ι {M : StdTracialAlgebra} (D : M.TracialSub) (T : ↥D.S) : D.model.ι T = ↑T M.traceVector

theorem CommutingRepetition.StdTracialAlgebra.TracialSub.model_L {M : StdTracialAlgebra} (D : M.TracialSub) (T : ↥D.S) : D.model.L T = ↑T

theorem CommutingRepetition.StdTracialAlgebra.TracialSub.model_A {M : StdTracialAlgebra} (D : M.TracialSub) : D.model.A = ↥D.S

theorem CommutingRepetition.StdTracialAlgebra.TracialSub.model_H {M : StdTracialAlgebra} (D : M.TracialSub) : D.model.H = M.H

theorem CommutingRepetition.StdTracialAlgebra.TracialSub.model_τ_L {M : StdTracialAlgebra} (D : M.TracialSub) (a : M.A) : D.model.τ ⟨M.L a, ⋯⟩ = M.τ a

The model's trace extends the original trace through the left representation.