Density of ι

theorem CommutingRepetition.StdTracialAlgebra.ι_induction (M : StdTracialAlgebra) {p : M.H → Prop} (hp : IsClosed {v : M.H | p v}) (h : ∀ (a : M.A), p (M.ι a)) (v : M.H) : p v

Induction along the dense range of ι.

theorem CommutingRepetition.StdTracialAlgebra.ext_of_inner_ι (M : StdTracialAlgebra) {u v : M.H} (h : ∀ (a : M.A), inner ℂ u (M.ι a) = inner ℂ v (M.ι a)) : u = v

The antiunitary J

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

The range of ι as a submodule.

Equations

• M.ιRange = M.ι.range

noncomputable def CommutingRepetition.StdTracialAlgebra.ιRep (M : StdTracialAlgebra) (v : ↥M.ιRange) : M.A

Equations

• M.ιRep v = ⋯.choose

theorem CommutingRepetition.StdTracialAlgebra.ι_ιRep (M : StdTracialAlgebra) (v : ↥M.ιRange) : M.ι (M.ιRep v) = ↑v

theorem CommutingRepetition.StdTracialAlgebra.inner_ι_star (M : StdTracialAlgebra) (a b : M.A) : inner ℂ (M.ι (star a)) (M.ι (star b)) = inner ℂ (M.ι b) (M.ι a)

theorem CommutingRepetition.StdTracialAlgebra.norm_ι_star (M : StdTracialAlgebra) (a : M.A) : ‖M.ι (star a)‖ = ‖M.ι a‖

theorem CommutingRepetition.StdTracialAlgebra.ι_star_welldef (M : StdTracialAlgebra) {a b : M.A} (h : M.ι a = M.ι b) : M.ι (star a) = M.ι (star b)

noncomputable def CommutingRepetition.StdTracialAlgebra.J₀ (M : StdTracialAlgebra) : ↥M.ιRange →L⋆[ℂ] M.H

J on the range of ι: ι a ↦ ι a*, conjugate-linear.

Equations

• M.J₀ = { toFun := fun (v : ↥M.ιRange) => M.ι (star (M.ιRep v)), map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

theorem CommutingRepetition.StdTracialAlgebra.J₀_apply (M : StdTracialAlgebra) (v : ↥M.ιRange) : M.J₀ v = M.ι (star (M.ιRep v))

theorem CommutingRepetition.StdTracialAlgebra.denseRange_subtypeL_ιRange (M : StdTracialAlgebra) : DenseRange ⇑M.ιRange.subtypeL

theorem CommutingRepetition.StdTracialAlgebra.isUniformInducing_subtypeL_ιRange (M : StdTracialAlgebra) : IsUniformInducing ⇑M.ιRange.subtypeL

noncomputable def CommutingRepetition.StdTracialAlgebra.J (M : StdTracialAlgebra) : M.H →L⋆[ℂ] M.H

The antiunitary J, the continuous extension of ι a ↦ ι a*.

Equations

• M.J = M.J₀.extend M.ιRange.subtypeL

theorem CommutingRepetition.StdTracialAlgebra.J_ι (M : StdTracialAlgebra) (a : M.A) : M.J (M.ι a) = M.ι (star a)

theorem CommutingRepetition.StdTracialAlgebra.inner_J_J (M : StdTracialAlgebra) (v w : M.H) : inner ℂ (M.J v) (M.J w) = inner ℂ w v

theorem CommutingRepetition.StdTracialAlgebra.J_J (M : StdTracialAlgebra) (v : M.H) : M.J (M.J v) = v

theorem CommutingRepetition.StdTracialAlgebra.inner_J_left (M : StdTracialAlgebra) (v w : M.H) : inner ℂ (M.J v) w = inner ℂ (M.J w) v

The commutant of the right action

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

The concrete von Neumann algebra R(M)' ⊆ B(L²(M)).

Equations

• M.vnAlg = StarSubalgebra.centralizer ℂ (Set.range M.Rop)

theorem CommutingRepetition.StdTracialAlgebra.star_Rop (M : StdTracialAlgebra) (a : M.A) : star (M.Rop a) = M.Rop (star a)

theorem CommutingRepetition.StdTracialAlgebra.mem_vnAlg_iff (M : StdTracialAlgebra) {T : M.H →L[ℂ] M.H} : T ∈ M.vnAlg ↔ ∀ (a : M.A), M.Rop a * T = T * M.Rop a

theorem CommutingRepetition.StdTracialAlgebra.L_mem_vnAlg (M : StdTracialAlgebra) (a : M.A) : M.L a ∈ M.vnAlg

theorem CommutingRepetition.StdTracialAlgebra.isClosed_vnAlg (M : StdTracialAlgebra) : IsClosed ↑M.vnAlg

theorem CommutingRepetition.StdTracialAlgebra.Rop_traceVector (M : StdTracialAlgebra) (a : M.A) : (M.Rop a) M.traceVector = M.ι a

theorem CommutingRepetition.StdTracialAlgebra.mulA (M : StdTracialAlgebra) (f g : M.H →L[ℂ] M.H) (ξ : M.H) : (f * g) ξ = f (g ξ)

theorem CommutingRepetition.StdTracialAlgebra.J_apply_traceVector (M : StdTracialAlgebra) {T : M.H →L[ℂ] M.H} (hT : T ∈ M.vnAlg) : M.J (T M.traceVector) = (star T) M.traceVector

J (T Ω) = T* Ω for T in the commutant of the right action.

theorem CommutingRepetition.StdTracialAlgebra.traceState_mul_comm_vn (M : StdTracialAlgebra) {T U : M.H →L[ℂ] M.H} (hT : T ∈ M.vnAlg) (hU : U ∈ M.vnAlg) : M.traceState (T * U) = M.traceState (U * T)

Traciality of the trace-vector state on R(M)'.

noncomputable def CommutingRepetition.StdTracialAlgebra.vnData (M : StdTracialAlgebra) : M.TracialSub

The tracial-subalgebra datum of the commutant.

Equations

• M.vnData = { S := M.vnAlg, isClosed := ⋯, L_mem := ⋯, tracial := ⋯ }

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

The concrete von Neumann model: R(M)' as a standard tracial algebra on L²(M).

Equations

• M.vnModel = M.vnData.model

theorem CommutingRepetition.StdTracialAlgebra.vnModel_A (M : StdTracialAlgebra) : M.vnModel.A = ↥M.vnAlg

theorem CommutingRepetition.StdTracialAlgebra.vnModel_H (M : StdTracialAlgebra) : M.vnModel.H = M.H

theorem CommutingRepetition.StdTracialAlgebra.vnModel_τ (M : StdTracialAlgebra) (T : ↥M.vnAlg) : M.vnModel.τ T = M.traceState ↑T

theorem CommutingRepetition.StdTracialAlgebra.vnModel_ι (M : StdTracialAlgebra) (T : ↥M.vnAlg) : M.vnModel.ι T = ↑T M.traceVector

theorem CommutingRepetition.StdTracialAlgebra.vnModel_L (M : StdTracialAlgebra) (T : ↥M.vnAlg) : M.vnModel.L T = ↑T

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