@[reducible, inline]

abbrev CommutingRepetition.StdTracialAlgebra.AmpH (M : StdTracialAlgebra) (d : ℕ) : Type u

The amplified GNS space: a d × d matrix of copies of L²(M), with the ℓ²-norm.

Equations

• M.AmpH d = PiLp 2 fun (x : Fin d × Fin d) => M.H

@[simp]

theorem CommutingRepetition.StdTracialAlgebra.AmpH.coord (M : StdTracialAlgebra) (d : ℕ) (w : M.AmpH d) (p : Fin d × Fin d) : w.ofLp p = w.ofLp p

noncomputable def CommutingRepetition.StdTracialAlgebra.ampτ (M : StdTracialAlgebra) (d : ℕ) : Matrix (Fin d) (Fin d) M.A →ₗ[ℂ] ℂ

The normalized amplified trace τ_d(X) = d⁻¹ ∑ᵢ τ(X i i).

Equations

• M.ampτ d = { toFun := fun (X : Matrix (Fin d) (Fin d) M.A) => (↑d)⁻¹ * ∑ i : Fin d, M.τ (X i i), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem CommutingRepetition.StdTracialAlgebra.ampτ_apply (M : StdTracialAlgebra) (d : ℕ) (X : Matrix (Fin d) (Fin d) M.A) : (M.ampτ d) X = (↑d)⁻¹ * ∑ i : Fin d, M.τ (X i i)

noncomputable def CommutingRepetition.StdTracialAlgebra.ampι (M : StdTracialAlgebra) (d : ℕ) : Matrix (Fin d) (Fin d) M.A →ₗ[ℂ] M.AmpH d

The amplified GNS embedding, scaled by d^{-1/2} so that the ampτ-inner-product identity holds with the unweighted ℓ²-inner product.

Equations

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

@[simp]

theorem CommutingRepetition.StdTracialAlgebra.ampι_apply (M : StdTracialAlgebra) (d : ℕ) (X : Matrix (Fin d) (Fin d) M.A) (p : Fin d × Fin d) : ((M.ampι d) X).ofLp p = ↑(√↑d)⁻¹ • M.ι (X p.1 p.2)

noncomputable def CommutingRepetition.StdTracialAlgebra.ampLCLM (M : StdTracialAlgebra) (d : ℕ) (X : Matrix (Fin d) (Fin d) M.A) : M.AmpH d →L[ℂ] M.AmpH d

Left multiplication by a matrix, acting on the row index of the amplified GNS space through M.L.

Equations

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

@[simp]

theorem CommutingRepetition.StdTracialAlgebra.ampLCLM_apply (M : StdTracialAlgebra) (d : ℕ) (X : Matrix (Fin d) (Fin d) M.A) (v : M.AmpH d) (p : Fin d × Fin d) : ((M.ampLCLM d X) v).ofLp p = ∑ j : Fin d, (M.L (X p.1 j)) (v.ofLp (j, p.2))

noncomputable def CommutingRepetition.StdTracialAlgebra.ampRCLM (M : StdTracialAlgebra) (d : ℕ) (P : (Matrix (Fin d) (Fin d) M.A)ᵐᵒᵖ) : M.AmpH d →L[ℂ] M.AmpH d

Right multiplication by a matrix, acting on the column index of the amplified GNS space through M.R.

Equations

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

@[simp]

theorem CommutingRepetition.StdTracialAlgebra.ampRCLM_apply (M : StdTracialAlgebra) (d : ℕ) (P : (Matrix (Fin d) (Fin d) M.A)ᵐᵒᵖ) (v : M.AmpH d) (p : Fin d × Fin d) : ((M.ampRCLM d P) v).ofLp p = ∑ j : Fin d, (M.R (MulOpposite.op (MulOpposite.unop P j p.2))) (v.ofLp (p.1, j))

theorem CommutingRepetition.StdTracialAlgebra.ampLCLM_one (M : StdTracialAlgebra) (d : ℕ) : M.ampLCLM d 1 = 1

theorem CommutingRepetition.StdTracialAlgebra.ampLCLM_mul (M : StdTracialAlgebra) (d : ℕ) (X Y : Matrix (Fin d) (Fin d) M.A) : M.ampLCLM d (X * Y) = M.ampLCLM d X ∘SL M.ampLCLM d Y

theorem CommutingRepetition.StdTracialAlgebra.ampLCLM_add (M : StdTracialAlgebra) (d : ℕ) (X Y : Matrix (Fin d) (Fin d) M.A) : M.ampLCLM d (X + Y) = M.ampLCLM d X + M.ampLCLM d Y

theorem CommutingRepetition.StdTracialAlgebra.ampLCLM_smul (M : StdTracialAlgebra) (d : ℕ) (c : ℂ) (X : Matrix (Fin d) (Fin d) M.A) : M.ampLCLM d (c • X) = c • M.ampLCLM d X

theorem CommutingRepetition.StdTracialAlgebra.ampLCLM_star (M : StdTracialAlgebra) (d : ℕ) (X : Matrix (Fin d) (Fin d) M.A) : M.ampLCLM d (star X) = star (M.ampLCLM d X)

theorem CommutingRepetition.StdTracialAlgebra.ampRCLM_one (M : StdTracialAlgebra) (d : ℕ) : M.ampRCLM d 1 = 1

theorem CommutingRepetition.StdTracialAlgebra.ampRCLM_mul (M : StdTracialAlgebra) (d : ℕ) (P Q : (Matrix (Fin d) (Fin d) M.A)ᵐᵒᵖ) : M.ampRCLM d (P * Q) = M.ampRCLM d P ∘SL M.ampRCLM d Q

theorem CommutingRepetition.StdTracialAlgebra.ampRCLM_add (M : StdTracialAlgebra) (d : ℕ) (P Q : (Matrix (Fin d) (Fin d) M.A)ᵐᵒᵖ) : M.ampRCLM d (P + Q) = M.ampRCLM d P + M.ampRCLM d Q

theorem CommutingRepetition.StdTracialAlgebra.ampRCLM_smul (M : StdTracialAlgebra) (d : ℕ) (c : ℂ) (P : (Matrix (Fin d) (Fin d) M.A)ᵐᵒᵖ) : M.ampRCLM d (c • P) = c • M.ampRCLM d P

theorem CommutingRepetition.StdTracialAlgebra.ampRCLM_star (M : StdTracialAlgebra) (d : ℕ) (P : (Matrix (Fin d) (Fin d) M.A)ᵐᵒᵖ) : M.ampRCLM d (star P) = star (M.ampRCLM d P)

noncomputable def CommutingRepetition.StdTracialAlgebra.ampLhom (M : StdTracialAlgebra) (d : ℕ) : Matrix (Fin d) (Fin d) M.A →⋆ₐ[ℂ] M.AmpH d →L[ℂ] M.AmpH d

The amplified left representation as a ⋆-algebra homomorphism.

Equations

• M.ampLhom d = { toFun := M.ampLCLM d, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯, map_star' := ⋯ }

noncomputable def CommutingRepetition.StdTracialAlgebra.ampRhom (M : StdTracialAlgebra) (d : ℕ) : (Matrix (Fin d) (Fin d) M.A)ᵐᵒᵖ →⋆ₐ[ℂ] M.AmpH d →L[ℂ] M.AmpH d

The amplified right representation as a ⋆-algebra homomorphism on the opposite algebra.

Equations

• M.ampRhom d = { toFun := M.ampRCLM d, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯, map_star' := ⋯ }

theorem CommutingRepetition.StdTracialAlgebra.ampι_dense (M : StdTracialAlgebra) (d : ℕ) : DenseRange ⇑(M.ampι d)

theorem CommutingRepetition.StdTracialAlgebra.ampι_inner (M : StdTracialAlgebra) (d : ℕ) (X Y : Matrix (Fin d) (Fin d) M.A) : inner ℂ ((M.ampι d) X) ((M.ampι d) Y) = (M.ampτ d) (star X * Y)

noncomputable def CommutingRepetition.StdTracialAlgebra.amplify (M : StdTracialAlgebra) (d : ℕ) [NeZero d] : StdTracialAlgebra

The matrix amplification M_d(M) as a standard tracial algebra (Stage B, WP-B3).

Equations

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