theorem CommutingRepetition.StdTracialAlgebra.ext_of_eq_on_ι (M : StdTracialAlgebra) {F G : M.H →L[ℂ] M.H} (h : ∀ (a : M.A), F (M.ι a) = G (M.ι a)) : F = G

Two operators agreeing on ι(M.A) are equal.

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

theorem CommutingRepetition.StdTracialAlgebra.vnAlg_comm_conjJ (M : StdTracialAlgebra) {T T' : M.H →L[ℂ] M.H} (hT : T ∈ M.vnAlg) (hT' : T' ∈ M.vnAlg) : T * M.conjJ T' = M.conjJ T' * T

Tracial commutation: R(M)′ commutes with J R(M)′ J.

theorem CommutingRepetition.StdTracialAlgebra.mem_vnAlg_of_tendsto (M : StdTracialAlgebra) {T : ℕ → M.H →L[ℂ] M.H} {L : M.H →L[ℂ] M.H} (hT : ∀ (n : ℕ), T n ∈ M.vnAlg) (h : ∀ (ξ : M.H), Filter.Tendsto (fun (n : ℕ) => (T n) ξ) Filter.atTop (nhds (L ξ))) : L ∈ M.vnAlg

R(M)′ is closed under pointwise limits of sequences.

theorem CommutingRepetition.StdTracialAlgebra.vnModel_Rop_eq (M : StdTracialAlgebra) (T : ↥M.vnAlg) : M.vnModel.Rop T = M.conjJ (star ↑T)

The right action of the concrete model is conjugation by J of the adjoint.

noncomputable def CommutingRepetition.StdTracialAlgebra.LvHom (M : StdTracialAlgebra) : M.A →⋆ₐ[ℂ] ↥M.vnAlg

Lv as a unital star algebra homomorphism M.A →⋆ₐ[ℂ] vnAlg M.

Equations

• M.LvHom = { toFun := M.Lv, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯, map_star' := ⋯ }

noncomputable def CommutingRepetition.StdTracialAlgebra.vnExtension (M : StdTracialAlgebra) : TracialExtension M

The tracial extension of WP-B7: the concrete von Neumann model on the same L².

Equations

• M.vnExtension = { N' := M.vnModel, emb := M.LvHom, U := LinearIsometryEquiv.refl ℂ M.H, U_ι := ⋯, L_emb := ⋯, R_emb := ⋯ }