The product trace

noncomputable def CommutingRepetition.StdTracialAlgebra.stepτ (M₁ M₂ : StdTracialAlgebra) : TensorProduct ℂ M₁.A M₂.A →ₗ[ℂ] ℂ

The product trace τ(a ⊗ b) = τ₁(a) τ₂(b) on the algebraic tensor product.

Equations

• M₁.stepτ M₂ = ↑(TensorProduct.lid ℂ ℂ) ∘ₗ TensorProduct.map M₁.τ M₂.τ

@[simp]

theorem CommutingRepetition.StdTracialAlgebra.stepτ_tmul (M₁ M₂ : StdTracialAlgebra) (a : M₁.A) (b : M₂.A) : (M₁.stepτ M₂) (a ⊗ₜ[ℂ] b) = M₁.τ a * M₂.τ b

theorem CommutingRepetition.StdTracialAlgebra.stepτ_one (M₁ M₂ : StdTracialAlgebra) : (M₁.stepτ M₂) 1 = 1

theorem CommutingRepetition.StdTracialAlgebra.stepτ_mul_comm (M₁ M₂ : StdTracialAlgebra) (x y : TensorProduct ℂ M₁.A M₂.A) : (M₁.stepτ M₂) (x * y) = (M₁.stepτ M₂) (y * x)

theorem CommutingRepetition.StdTracialAlgebra.stepτ_star (M₁ M₂ : StdTracialAlgebra) (x : TensorProduct ℂ M₁.A M₂.A) : (M₁.stepτ M₂) (star x) = star ((M₁.stepτ M₂) x)

The GNS space

@[reducible, inline]

abbrev CommutingRepetition.StdTracialAlgebra.StepH (M₁ M₂ : StdTracialAlgebra) : Type u

The GNS space of the product trace: the completion of the inner-product tensor product of the two GNS spaces.

Equations

• M₁.StepH M₂ = UniformSpace.Completion (TensorProduct ℂ M₁.H M₂.H)

noncomputable def CommutingRepetition.StdTracialAlgebra.stepι (M₁ M₂ : StdTracialAlgebra) : TensorProduct ℂ M₁.A M₂.A →ₗ[ℂ] M₁.StepH M₂

The GNS embedding: ι₁ ⊗ ι₂ into the completion.

Equations

• M₁.stepι M₂ = UniformSpace.Completion.toComplₗᵢ.toLinearMap ∘ₗ TensorProduct.map M₁.ι M₂.ι

@[simp]

theorem CommutingRepetition.StdTracialAlgebra.stepι_tmul (M₁ M₂ : StdTracialAlgebra) (a : M₁.A) (b : M₂.A) : (M₁.stepι M₂) (a ⊗ₜ[ℂ] b) = ↑(M₁.ι a ⊗ₜ[ℂ] M₂.ι b)

theorem CommutingRepetition.StdTracialAlgebra.stepι_inner (M₁ M₂ : StdTracialAlgebra) (x y : TensorProduct ℂ M₁.A M₂.A) : inner ℂ ((M₁.stepι M₂) x) ((M₁.stepι M₂) y) = (M₁.stepτ M₂) (star x * y)

theorem CommutingRepetition.StdTracialAlgebra.denseRange_map_ι (M₁ M₂ : StdTracialAlgebra) : DenseRange ⇑(TensorProduct.map M₁.ι M₂.ι)

Density of the algebraic image inside the tensor product (before completion): the range of ι₁ ⊗ ι₂ is dense in H₁ ⊗ H₂. Two-slot closed-preimage argument: for fixed a, the set of y with ι₁ a ⊗ y in the closure is closed and contains the dense range of ι₂; then the set of x with x ⊗ y in the closure is closed and contains the dense range of ι₁; conclude on pure tensors and extend by the submodule structure of the closure.

theorem CommutingRepetition.StdTracialAlgebra.stepι_dense (M₁ M₂ : StdTracialAlgebra) : DenseRange ⇑(M₁.stepι M₂)

The GNS embedding has dense range (density in the algebraic tensor product composed with density of the completion coercion).

Extending operators to the completion

noncomputable def CommutingRepetition.StdTracialAlgebra.toStepH (M₁ M₂ : StdTracialAlgebra) : TensorProduct ℂ M₁.H M₂.H →L[ℂ] M₁.StepH M₂

The completion coercion as a continuous linear map.

Equations

• M₁.toStepH M₂ = UniformSpace.Completion.toComplₗᵢ.toContinuousLinearMap

@[simp]

theorem CommutingRepetition.StdTracialAlgebra.toStepH_apply (M₁ M₂ : StdTracialAlgebra) (w : TensorProduct ℂ M₁.H M₂.H) : (M₁.toStepH M₂) w = ↑w

theorem CommutingRepetition.StdTracialAlgebra.denseRange_toStepH (M₁ M₂ : StdTracialAlgebra) : DenseRange ⇑(M₁.toStepH M₂)

theorem CommutingRepetition.StdTracialAlgebra.isUniformInducing_toStepH (M₁ M₂ : StdTracialAlgebra) : IsUniformInducing ⇑(M₁.toStepH M₂)

noncomputable def CommutingRepetition.StdTracialAlgebra.extendStep (M₁ M₂ : StdTracialAlgebra) (T : TensorProduct ℂ M₁.H M₂.H →L[ℂ] TensorProduct ℂ M₁.H M₂.H) : M₁.StepH M₂ →L[ℂ] M₁.StepH M₂

The unique bounded extension of an operator on the algebraic tensor product to the completed GNS space.

Equations

• M₁.extendStep M₂ T = (M₁.toStepH M₂ ∘SL T).extend (M₁.toStepH M₂)

theorem CommutingRepetition.StdTracialAlgebra.extendStep_coe (M₁ M₂ : StdTracialAlgebra) (T : TensorProduct ℂ M₁.H M₂.H →L[ℂ] TensorProduct ℂ M₁.H M₂.H) (w : TensorProduct ℂ M₁.H M₂.H) : (M₁.extendStep M₂ T) ↑w = ↑(T w)

theorem CommutingRepetition.StdTracialAlgebra.ext_of_coe (M₁ M₂ : StdTracialAlgebra) {P Q : M₁.StepH M₂ →L[ℂ] M₁.StepH M₂} (h : ∀ (w : TensorProduct ℂ M₁.H M₂.H), P ↑w = Q ↑w) : P = Q

Two operators on the completion agreeing on coercions are equal.

theorem CommutingRepetition.StdTracialAlgebra.extendStep_id (M₁ M₂ : StdTracialAlgebra) : M₁.extendStep M₂ (ContinuousLinearMap.id ℂ (TensorProduct ℂ M₁.H M₂.H)) = ContinuousLinearMap.id ℂ (M₁.StepH M₂)

theorem CommutingRepetition.StdTracialAlgebra.extendStep_comp (M₁ M₂ : StdTracialAlgebra) (S T : TensorProduct ℂ M₁.H M₂.H →L[ℂ] TensorProduct ℂ M₁.H M₂.H) : M₁.extendStep M₂ (S ∘SL T) = M₁.extendStep M₂ S ∘SL M₁.extendStep M₂ T

theorem CommutingRepetition.StdTracialAlgebra.extendStep_add (M₁ M₂ : StdTracialAlgebra) (S T : TensorProduct ℂ M₁.H M₂.H →L[ℂ] TensorProduct ℂ M₁.H M₂.H) : M₁.extendStep M₂ (S + T) = M₁.extendStep M₂ S + M₁.extendStep M₂ T

theorem CommutingRepetition.StdTracialAlgebra.extendStep_smul (M₁ M₂ : StdTracialAlgebra) (c : ℂ) (T : TensorProduct ℂ M₁.H M₂.H →L[ℂ] TensorProduct ℂ M₁.H M₂.H) : M₁.extendStep M₂ (c • T) = c • M₁.extendStep M₂ T

theorem CommutingRepetition.StdTracialAlgebra.extendStep_zero (M₁ M₂ : StdTracialAlgebra) : M₁.extendStep M₂ 0 = 0

theorem CommutingRepetition.StdTracialAlgebra.inner_mapL_star (M₁ M₂ : StdTracialAlgebra) (S : M₁.H →L[ℂ] M₁.H) (T : M₂.H →L[ℂ] M₂.H) (w w' : TensorProduct ℂ M₁.H M₂.H) : inner ℂ ((TensorProduct.mapL (star S) (star T)) w) w' = inner ℂ w ((TensorProduct.mapL S T) w')

Adjoint duality for factorwise operators on the algebraic tensor product: ⟪(S* ⊗ T*) w, w'⟫ = ⟪w, (S ⊗ T) w'⟫.

theorem CommutingRepetition.StdTracialAlgebra.extendStep_star_of_inner (M₁ M₂ : StdTracialAlgebra) {P Q : TensorProduct ℂ M₁.H M₂.H →L[ℂ] TensorProduct ℂ M₁.H M₂.H} (hPQ : ∀ (w w' : TensorProduct ℂ M₁.H M₂.H), inner ℂ (P w) w' = inner ℂ w (Q w')) : M₁.extendStep M₂ P = star (M₁.extendStep M₂ Q)

Adjoint compatibility of the extension, from inner-product duality of the unextended operators: if ⟪P w, w'⟫ = ⟪w, Q w'⟫ on the algebraic tensor product then the extension of P is the adjoint of the extension of Q.

The factorwise representation

theorem CommutingRepetition.StdTracialAlgebra.extendStep_one (M₁ M₂ : StdTracialAlgebra) : M₁.extendStep M₂ 1 = 1

noncomputable def CommutingRepetition.StdTracialAlgebra.tensorRep0 (M₁ M₂ : StdTracialAlgebra) {A₁ : Type u_1} [Ring A₁] [StarRing A₁] [Algebra ℂ A₁] {A₂ : Type u_2} [Ring A₂] [StarRing A₂] [Algebra ℂ A₂] (φ₁ : A₁ →⋆ₐ[ℂ] M₁.H →L[ℂ] M₁.H) (φ₂ : A₂ →⋆ₐ[ℂ] M₂.H →L[ℂ] M₂.H) : TensorProduct ℂ A₁ A₂ →ₗ[ℂ] TensorProduct ℂ M₁.H M₂.H →L[ℂ] TensorProduct ℂ M₁.H M₂.H

The factorwise action on the algebraic tensor product: a ⊗ b ↦ φ₁(a) ⊗ φ₂(b) as a bounded operator.

Equations

• M₁.tensorRep0 M₂ φ₁ φ₂ = TensorProduct.lift (LinearMap.mk₂ ℂ (fun (a : A₁) (b : A₂) => TensorProduct.mapL (φ₁ a) (φ₂ b)) ⋯ ⋯ ⋯ ⋯)

@[simp]

theorem CommutingRepetition.StdTracialAlgebra.tensorRep0_tmul (M₁ M₂ : StdTracialAlgebra) {A₁ : Type u_1} [Ring A₁] [StarRing A₁] [Algebra ℂ A₁] [StarModule ℂ A₁] {A₂ : Type u_2} [Ring A₂] [StarRing A₂] [Algebra ℂ A₂] [StarModule ℂ A₂] (φ₁ : A₁ →⋆ₐ[ℂ] M₁.H →L[ℂ] M₁.H) (φ₂ : A₂ →⋆ₐ[ℂ] M₂.H →L[ℂ] M₂.H) (a : A₁) (b : A₂) : (M₁.tensorRep0 M₂ φ₁ φ₂) (a ⊗ₜ[ℂ] b) = TensorProduct.mapL (φ₁ a) (φ₂ b)

theorem CommutingRepetition.StdTracialAlgebra.tensorRep0_one (M₁ M₂ : StdTracialAlgebra) {A₁ : Type u_1} [Ring A₁] [StarRing A₁] [Algebra ℂ A₁] [StarModule ℂ A₁] {A₂ : Type u_2} [Ring A₂] [StarRing A₂] [Algebra ℂ A₂] [StarModule ℂ A₂] (φ₁ : A₁ →⋆ₐ[ℂ] M₁.H →L[ℂ] M₁.H) (φ₂ : A₂ →⋆ₐ[ℂ] M₂.H →L[ℂ] M₂.H) : (M₁.tensorRep0 M₂ φ₁ φ₂) 1 = 1

theorem CommutingRepetition.StdTracialAlgebra.tensorRep0_mul (M₁ M₂ : StdTracialAlgebra) {A₁ : Type u_1} [Ring A₁] [StarRing A₁] [Algebra ℂ A₁] [StarModule ℂ A₁] {A₂ : Type u_2} [Ring A₂] [StarRing A₂] [Algebra ℂ A₂] [StarModule ℂ A₂] (φ₁ : A₁ →⋆ₐ[ℂ] M₁.H →L[ℂ] M₁.H) (φ₂ : A₂ →⋆ₐ[ℂ] M₂.H →L[ℂ] M₂.H) (x y : TensorProduct ℂ A₁ A₂) : (M₁.tensorRep0 M₂ φ₁ φ₂) (x * y) = (M₁.tensorRep0 M₂ φ₁ φ₂) x * (M₁.tensorRep0 M₂ φ₁ φ₂) y

theorem CommutingRepetition.StdTracialAlgebra.tensorRep0_inner_star (M₁ M₂ : StdTracialAlgebra) {A₁ : Type u_1} [Ring A₁] [StarRing A₁] [Algebra ℂ A₁] [StarModule ℂ A₁] {A₂ : Type u_2} [Ring A₂] [StarRing A₂] [Algebra ℂ A₂] [StarModule ℂ A₂] (φ₁ : A₁ →⋆ₐ[ℂ] M₁.H →L[ℂ] M₁.H) (φ₂ : A₂ →⋆ₐ[ℂ] M₂.H →L[ℂ] M₂.H) (x : TensorProduct ℂ A₁ A₂) (w w' : TensorProduct ℂ M₁.H M₂.H) : inner ℂ (((M₁.tensorRep0 M₂ φ₁ φ₂) (star x)) w) w' = inner ℂ w (((M₁.tensorRep0 M₂ φ₁ φ₂) x) w')

noncomputable def CommutingRepetition.StdTracialAlgebra.tensorRep (M₁ M₂ : StdTracialAlgebra) {A₁ : Type u_1} [Ring A₁] [StarRing A₁] [Algebra ℂ A₁] [StarModule ℂ A₁] {A₂ : Type u_2} [Ring A₂] [StarRing A₂] [Algebra ℂ A₂] [StarModule ℂ A₂] (φ₁ : A₁ →⋆ₐ[ℂ] M₁.H →L[ℂ] M₁.H) (φ₂ : A₂ →⋆ₐ[ℂ] M₂.H →L[ℂ] M₂.H) : TensorProduct ℂ A₁ A₂ →⋆ₐ[ℂ] M₁.StepH M₂ →L[ℂ] M₁.StepH M₂

The factorwise representation on the completed GNS space, as a ∗-algebra homomorphism: a ⊗ b acts by the extension of φ₁(a) ⊗ φ₂(b).

Equations

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

theorem CommutingRepetition.StdTracialAlgebra.tensorRep_apply (M₁ M₂ : StdTracialAlgebra) {A₁ : Type u_1} [Ring A₁] [StarRing A₁] [Algebra ℂ A₁] [StarModule ℂ A₁] {A₂ : Type u_2} [Ring A₂] [StarRing A₂] [Algebra ℂ A₂] [StarModule ℂ A₂] (φ₁ : A₁ →⋆ₐ[ℂ] M₁.H →L[ℂ] M₁.H) (φ₂ : A₂ →⋆ₐ[ℂ] M₂.H →L[ℂ] M₂.H) (x : TensorProduct ℂ A₁ A₂) : (M₁.tensorRep M₂ φ₁ φ₂) x = M₁.extendStep M₂ ((M₁.tensorRep0 M₂ φ₁ φ₂) x)

theorem CommutingRepetition.StdTracialAlgebra.tensorRep_coe (M₁ M₂ : StdTracialAlgebra) {A₁ : Type u_1} [Ring A₁] [StarRing A₁] [Algebra ℂ A₁] [StarModule ℂ A₁] {A₂ : Type u_2} [Ring A₂] [StarRing A₂] [Algebra ℂ A₂] [StarModule ℂ A₂] (φ₁ : A₁ →⋆ₐ[ℂ] M₁.H →L[ℂ] M₁.H) (φ₂ : A₂ →⋆ₐ[ℂ] M₂.H →L[ℂ] M₂.H) (x : TensorProduct ℂ A₁ A₂) (w : TensorProduct ℂ M₁.H M₂.H) : ((M₁.tensorRep M₂ φ₁ φ₂) x) ↑w = ↑(((M₁.tensorRep0 M₂ φ₁ φ₂) x) w)

The left and right representations and the assembly

noncomputable def CommutingRepetition.StdTracialAlgebra.opDistrib (M₁ M₂ : StdTracialAlgebra) : (TensorProduct ℂ M₁.A M₂.A)ᵐᵒᵖ →⋆ₐ[ℂ] TensorProduct ℂ M₁.Aᵐᵒᵖ M₂.Aᵐᵒᵖ

The opposite-algebra distribution (A₁ ⊗ A₂)ᵐᵒᵖ → A₁ᵐᵒᵖ ⊗ A₂ᵐᵒᵖ as a ∗-algebra homomorphism.

Equations

• M₁.opDistrib M₂ = { toAlgHom := ↑(Algebra.TensorProduct.opAlgEquiv ℂ ℂ M₁.A M₂.A).symm, map_star' := ⋯ }

@[simp]

theorem CommutingRepetition.StdTracialAlgebra.opDistrib_op_tmul (M₁ M₂ : StdTracialAlgebra) (a : M₁.A) (b : M₂.A) : (M₁.opDistrib M₂) (MulOpposite.op (a ⊗ₜ[ℂ] b)) = MulOpposite.op a ⊗ₜ[ℂ] MulOpposite.op b

noncomputable def CommutingRepetition.StdTracialAlgebra.stepL (M₁ M₂ : StdTracialAlgebra) : TensorProduct ℂ M₁.A M₂.A →⋆ₐ[ℂ] M₁.StepH M₂ →L[ℂ] M₁.StepH M₂

The left representation of the tensor step.

Equations

• M₁.stepL M₂ = M₁.tensorRep M₂ M₁.L M₂.L

noncomputable def CommutingRepetition.StdTracialAlgebra.stepR (M₁ M₂ : StdTracialAlgebra) : (TensorProduct ℂ M₁.A M₂.A)ᵐᵒᵖ →⋆ₐ[ℂ] M₁.StepH M₂ →L[ℂ] M₁.StepH M₂

The right representation of the tensor step.

Equations

• M₁.stepR M₂ = (M₁.tensorRep M₂ M₁.R M₂.R).comp (M₁.opDistrib M₂)

theorem CommutingRepetition.StdTracialAlgebra.tensorRep0_L_map_ι (M₁ M₂ : StdTracialAlgebra) (x y : TensorProduct ℂ M₁.A M₂.A) : ((M₁.tensorRep0 M₂ M₁.L M₂.L) x) ((TensorProduct.map M₁.ι M₂.ι) y) = (TensorProduct.map M₁.ι M₂.ι) (x * y)

The left evaluation identity on the algebraic image.

theorem CommutingRepetition.StdTracialAlgebra.stepL_apply (M₁ M₂ : StdTracialAlgebra) (x y : TensorProduct ℂ M₁.A M₂.A) : ((M₁.stepL M₂) x) ((M₁.stepι M₂) y) = (M₁.stepι M₂) (x * y)

theorem CommutingRepetition.StdTracialAlgebra.tensorRep0_R_map_ι (M₁ M₂ : StdTracialAlgebra) (x y : TensorProduct ℂ M₁.A M₂.A) : ((M₁.tensorRep0 M₂ M₁.R M₂.R) ((M₁.opDistrib M₂) (MulOpposite.op x))) ((TensorProduct.map M₁.ι M₂.ι) y) = (TensorProduct.map M₁.ι M₂.ι) (y * x)

The right evaluation identity on the algebraic image.

theorem CommutingRepetition.StdTracialAlgebra.stepR_apply (M₁ M₂ : StdTracialAlgebra) (x y : TensorProduct ℂ M₁.A M₂.A) : ((M₁.stepR M₂) (MulOpposite.op x)) ((M₁.stepι M₂) y) = (M₁.stepι M₂) (y * x)

theorem CommutingRepetition.StdTracialAlgebra.tensorRep0_commute (M₁ M₂ : StdTracialAlgebra) {A₁ : Type u_1} [Ring A₁] [StarRing A₁] [Algebra ℂ A₁] [StarModule ℂ A₁] {A₂ : Type u_2} [Ring A₂] [StarRing A₂] [Algebra ℂ A₂] [StarModule ℂ A₂] {B₁ : Type u_3} [Ring B₁] [StarRing B₁] [Algebra ℂ B₁] [StarModule ℂ B₁] {B₂ : Type u_4} [Ring B₂] [StarRing B₂] [Algebra ℂ B₂] [StarModule ℂ B₂] (φ₁ : A₁ →⋆ₐ[ℂ] M₁.H →L[ℂ] M₁.H) (φ₂ : A₂ →⋆ₐ[ℂ] M₂.H →L[ℂ] M₂.H) (ψ₁ : B₁ →⋆ₐ[ℂ] M₁.H →L[ℂ] M₁.H) (ψ₂ : B₂ →⋆ₐ[ℂ] M₂.H →L[ℂ] M₂.H) (h₁ : ∀ (a : A₁) (c : B₁), Commute (φ₁ a) (ψ₁ c)) (h₂ : ∀ (b : A₂) (d : B₂), Commute (φ₂ b) (ψ₂ d)) (x : TensorProduct ℂ A₁ A₂) (z : TensorProduct ℂ B₁ B₂) : Commute ((M₁.tensorRep0 M₂ φ₁ φ₂) x) ((M₁.tensorRep0 M₂ ψ₁ ψ₂) z)

Factorwise commutation on the algebraic tensor product, from pointwise commutation of the factor actions.

theorem CommutingRepetition.StdTracialAlgebra.stepLR_commute (M₁ M₂ : StdTracialAlgebra) (x y : TensorProduct ℂ M₁.A M₂.A) : Commute ((M₁.stepL M₂) x) ((M₁.stepR M₂) (MulOpposite.op y))

noncomputable def CommutingRepetition.StdTracialAlgebra.tensorStep (M₁ M₂ : StdTracialAlgebra) : StdTracialAlgebra

The binary tensor step: the algebraic tensor product with the product trace, in standard form on the completed inner-product tensor of the GNS spaces (Stage B, WP-B3b).

Equations

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

@[simp]

theorem CommutingRepetition.StdTracialAlgebra.tensorStep_A (M₁ M₂ : StdTracialAlgebra) : (M₁.tensorStep M₂).A = TensorProduct ℂ M₁.A M₂.A

@[simp]

theorem CommutingRepetition.StdTracialAlgebra.tensorStep_τ (M₁ M₂ : StdTracialAlgebra) (x : TensorProduct ℂ M₁.A M₂.A) : (M₁.tensorStep M₂).τ x = (M₁.stepτ M₂) x