Factor embeddings of the binary step

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

The left factor embedding a ↦ a ⊗ 1 as a ∗-algebra hom.

Equations

• M₁.stepInclLeft M₂ = { toAlgHom := Algebra.TensorProduct.includeLeft, map_star' := ⋯ }

@[simp]

theorem CommutingRepetition.StdTracialAlgebra.stepInclLeft_apply (M₁ M₂ : StdTracialAlgebra) (a : M₁.A) : (M₁.stepInclLeft M₂) a = a ⊗ₜ[ℂ] 1

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

The right factor embedding b ↦ 1 ⊗ b as a ∗-algebra hom.

Equations

• M₁.stepInclRight M₂ = { toAlgHom := Algebra.TensorProduct.includeRight, map_star' := ⋯ }

@[simp]

theorem CommutingRepetition.StdTracialAlgebra.stepInclRight_apply (M₁ M₂ : StdTracialAlgebra) (b : M₂.A) : (M₁.stepInclRight M₂) b = 1 ⊗ₜ[ℂ] b

theorem CommutingRepetition.StdTracialAlgebra.stepIncl_commute (M₁ M₂ : StdTracialAlgebra) (a : M₁.A) (b : M₂.A) : Commute ((M₁.stepInclLeft M₂) a) ((M₁.stepInclRight M₂) b)

theorem CommutingRepetition.StdTracialAlgebra.stepτ_inclLeft_mul_inclRight (M₁ M₂ : StdTracialAlgebra) (a : M₁.A) (b : M₂.A) : (M₁.stepτ M₂) ((M₁.stepInclLeft M₂) a * (M₁.stepInclRight M₂) b) = M₁.τ a * M₂.τ b

Iterated powers

noncomputable def CommutingRepetition.StdTracialAlgebra.tensorPow (N : StdTracialAlgebra) : ℕ → StdTracialAlgebra

The R-fold tensor power, by iterating the binary step on the right (junk value N itself at R = 0).

Equations

• N.tensorPow 0 = N
• N.tensorPow k.succ = (N.tensorPow k).tensorStep N

noncomputable def CommutingRepetition.StdTracialAlgebra.tensorPowIncl (N : StdTracialAlgebra) (R : ℕ) : Fin R → N.A →⋆ₐ[ℂ] (N.tensorPow R).A

The factor embeddings of the iterated power: factor k of R+1 factors is the right slot of the outermost step, earlier factors embed through the left slot.

Equations

• N.tensorPowIncl 0 = Fin.elim0
• N.tensorPowIncl k.succ = Fin.snoc (fun (i : Fin k) => ((N.tensorPow k).stepInclLeft N).comp (N.tensorPowIncl k i)) ((N.tensorPow k).stepInclRight N)

@[simp]

theorem CommutingRepetition.StdTracialAlgebra.tensorPowIncl_last (N : StdTracialAlgebra) (k : ℕ) : N.tensorPowIncl (k + 1) (Fin.last k) = (N.tensorPow k).stepInclRight N

@[simp]

theorem CommutingRepetition.StdTracialAlgebra.tensorPowIncl_castSucc (N : StdTracialAlgebra) (k : ℕ) (i : Fin k) : N.tensorPowIncl (k + 1) i.castSucc = ((N.tensorPow k).stepInclLeft N).comp (N.tensorPowIncl k i)

theorem CommutingRepetition.StdTracialAlgebra.tensorPowIncl_commute (N : StdTracialAlgebra) (R : ℕ) ⦃i j : Fin R⦄ : i ≠ j → ∀ (a b : N.A), Commute ((N.tensorPowIncl R i) a) ((N.tensorPowIncl R j) b)

Images of distinct factors commute.

theorem CommutingRepetition.StdTracialAlgebra.tensorPow_trace_prod (N : StdTracialAlgebra) (R : ℕ) (f : Fin R → N.A) : (N.tensorPow R).τ (List.ofFn fun (j : Fin R) => (N.tensorPowIncl R j) (f j)).prod = ∏ j : Fin R, N.τ (f j)

The ordered-product trace law: the trace of the ordered product of one element per factor is the product of the factor traces (06_otqcs.tex, eq amplified-resource, in the consumed form of TensorPowerData.trace_prod).