@[reducible, inline]

abbrev CommutingRepetition.Block.BH (M : StdTracialAlgebra) (κ : Type) : Type u

The block Hilbert space H^κ.

Equations

• CommutingRepetition.Block.BH M κ = PiLp 2 fun (x : κ) => M.H

Coordinate embeddings and projections

noncomputable def CommutingRepetition.Block.embed (M : StdTracialAlgebra) (κ : Type) [DecidableEq κ] (r : κ) : M.H →L[ℂ] BH M κ

Coordinate embedding v ↦ (0, …, v, …, 0).

Equations

• CommutingRepetition.Block.embed M κ r = ↑(PiLp.continuousLinearEquiv 2 ℂ fun (x : κ) => M.H).symm ∘SL ContinuousLinearMap.pi fun (r' : κ) => if r' = r then ContinuousLinearMap.id ℂ M.H else 0

noncomputable def CommutingRepetition.Block.proj (M : StdTracialAlgebra) (κ : Type) (r : κ) : BH M κ →L[ℂ] M.H

Coordinate projection.

Equations

• CommutingRepetition.Block.proj M κ r = PiLp.proj 2 (fun (x : κ) => M.H) r

theorem CommutingRepetition.Block.embed_apply (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] (r r' : κ) (v : M.H) : ((embed M κ r) v).ofLp r' = if r' = r then v else 0

theorem CommutingRepetition.Block.proj_apply (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] (r : κ) (w : BH M κ) : (proj M κ r) w = w.ofLp r

theorem CommutingRepetition.Block.proj_embed (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] (r r' : κ) (v : M.H) : (proj M κ r) ((embed M κ r') v) = if r = r' then v else 0

theorem CommutingRepetition.Block.proj_comp_embed_same (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] (r : κ) : proj M κ r ∘SL embed M κ r = ContinuousLinearMap.id ℂ M.H

theorem CommutingRepetition.Block.proj_comp_embed_ne (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] {r r' : κ} (h : r ≠ r') : proj M κ r ∘SL embed M κ r' = 0

theorem CommutingRepetition.Block.inner_embed_left (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] (r : κ) (v : M.H) (w : BH M κ) : inner ℂ ((embed M κ r) v) w = inner ℂ v (w.ofLp r)

theorem CommutingRepetition.Block.adjoint_embed (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] (r : κ) : ContinuousLinearMap.adjoint (embed M κ r) = proj M κ r

theorem CommutingRepetition.Block.adjoint_proj (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] (r : κ) : ContinuousLinearMap.adjoint (proj M κ r) = embed M κ r

theorem CommutingRepetition.Block.sumA (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] {ι : Type u_1} (s : Finset ι) (f : ι → BH M κ) (r : κ) : (∑ i ∈ s, f i).ofLp r = ∑ i ∈ s, (f i).ofLp r

theorem CommutingRepetition.Block.sumCLM {ι : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℂ E] [NormedSpace ℂ F] (s : Finset ι) (f : ι → E →L[ℂ] F) (v : E) : (∑ i ∈ s, f i) v = ∑ i ∈ s, (f i) v

theorem CommutingRepetition.Block.sum_embed_proj_apply (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] (w : BH M κ) : ∑ r : κ, (embed M κ r) ((proj M κ r) w) = w

Entries

noncomputable def CommutingRepetition.Block.entry (M : StdTracialAlgebra) (κ : Type) [DecidableEq κ] (T : BH M κ →L[ℂ] BH M κ) (r r' : κ) : M.H →L[ℂ] M.H

The (r, r') entry of a block operator.

Equations

• CommutingRepetition.Block.entry M κ T r r' = CommutingRepetition.Block.proj M κ r ∘SL T ∘SL CommutingRepetition.Block.embed M κ r'

theorem CommutingRepetition.Block.entry_apply (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] (T : BH M κ →L[ℂ] BH M κ) (r r' : κ) (v : M.H) : (entry M κ T r r') v = (proj M κ r) (T ((embed M κ r') v))

theorem CommutingRepetition.Block.entry_add (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] (T T' : BH M κ →L[ℂ] BH M κ) (r r' : κ) : entry M κ (T + T') r r' = entry M κ T r r' + entry M κ T' r r'

theorem CommutingRepetition.Block.entry_sub (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] (T T' : BH M κ →L[ℂ] BH M κ) (r r' : κ) : entry M κ (T - T') r r' = entry M κ T r r' - entry M κ T' r r'

theorem CommutingRepetition.Block.entry_smul (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] (c : ℂ) (T : BH M κ →L[ℂ] BH M κ) (r r' : κ) : entry M κ (c • T) r r' = c • entry M κ T r r'

theorem CommutingRepetition.Block.entry_zero (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] (r r' : κ) : entry M κ 0 r r' = 0

theorem CommutingRepetition.Block.entry_one (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] (r r' : κ) : entry M κ 1 r r' = if r = r' then 1 else 0

theorem CommutingRepetition.Block.entry_mul (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] (T T' : BH M κ →L[ℂ] BH M κ) (r r' : κ) : entry M κ (T * T') r r' = ∑ k : κ, entry M κ T r k * entry M κ T' k r'

theorem CommutingRepetition.Block.entry_star (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] (T : BH M κ →L[ℂ] BH M κ) (r r' : κ) : entry M κ (star T) r r' = star (entry M κ T r' r)

theorem CommutingRepetition.Block.continuous_entry (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] (r r' : κ) : Continuous fun (T : BH M κ →L[ℂ] BH M κ) => entry M κ T r r'

theorem CommutingRepetition.Block.block_decomp (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] (T : BH M κ →L[ℂ] BH M κ) : T = ∑ r : κ, ∑ r' : κ, embed M κ r ∘SL entry M κ T r r' ∘SL proj M κ r'

Block decomposition T = ∑ r r', embed r ∘ entry T r r' ∘ proj r'.

The block algebra

noncomputable def CommutingRepetition.Block.blockAlg (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] : StarSubalgebra ℂ (BH M κ →L[ℂ] BH M κ)

Block operators with all entries in the concrete von Neumann algebra.

Equations

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

theorem CommutingRepetition.Block.mem_blockAlg_iff (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] {T : BH M κ →L[ℂ] BH M κ} : T ∈ blockAlg M κ ↔ ∀ (r r' : κ), entry M κ T r r' ∈ M.vnAlg

theorem CommutingRepetition.Block.isClosed_blockAlg (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] : IsClosed ↑(blockAlg M κ)

The lift into the amplification

@[reducible, inline]

abbrev CommutingRepetition.Block.dim (κ : Type) [Fintype κ] : ℕ

The amplification dimension.

Equations

• CommutingRepetition.Block.dim κ = Fintype.card κ

instance CommutingRepetition.Block.instNeZeroNatDim (κ : Type) [Fintype κ] [Nonempty κ] : NeZero (dim κ)

@[reducible, inline]

noncomputable abbrev CommutingRepetition.Block.N (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [Nonempty κ] : StdTracialAlgebra

The target algebra M_d(vnAlg M) as a standard tracial algebra.

Equations

• CommutingRepetition.Block.N M κ = M.vnModel.amplify (CommutingRepetition.Block.dim κ)

@[reducible, inline]

noncomputable abbrev CommutingRepetition.Block.eκ (κ : Type) [Fintype κ] : κ ≃ Fin (dim κ)

The index equivalence.

Equations

• CommutingRepetition.Block.eκ κ = Fintype.equivFin κ

noncomputable def CommutingRepetition.Block.liftFun (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] (T : ↥(blockAlg M κ)) : Matrix (Fin (dim κ)) (Fin (dim κ)) M.vnModel.A

The entry matrix of a block-algebra element, reindexed to Fin d.

Equations

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

theorem CommutingRepetition.Block.liftFun_apply (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (T : ↥(blockAlg M κ)) (p q : Fin (dim κ)) : ↑(liftFun M κ T p q) = entry M κ (↑T) ((eκ κ).symm p) ((eκ κ).symm q)

theorem CommutingRepetition.Block.liftFun_one (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] : liftFun M κ 1 = 1

theorem CommutingRepetition.Block.liftFun_mul (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (T T' : ↥(blockAlg M κ)) : liftFun M κ (T * T') = liftFun M κ T * liftFun M κ T'

theorem CommutingRepetition.Block.liftFun_add (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (T T' : ↥(blockAlg M κ)) : liftFun M κ (T + T') = liftFun M κ T + liftFun M κ T'

theorem CommutingRepetition.Block.liftFun_zero (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] : liftFun M κ 0 = 0

theorem CommutingRepetition.Block.liftFun_smul (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (c : ℂ) (T : ↥(blockAlg M κ)) : liftFun M κ (c • T) = c • liftFun M κ T

theorem CommutingRepetition.Block.liftFun_star (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (T : ↥(blockAlg M κ)) : liftFun M κ (star T) = star (liftFun M κ T)

noncomputable def CommutingRepetition.Block.lift (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] : ↥(blockAlg M κ) →⋆ₐ[ℂ] (N M κ).A

The lift blockAlg M κ →⋆ₐ[ℂ] M_d(vnAlg M).

Equations

• CommutingRepetition.Block.lift M κ = { toFun := CommutingRepetition.Block.liftFun M κ, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯, map_star' := ⋯ }

theorem CommutingRepetition.Block.lift_apply (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (T : ↥(blockAlg M κ)) (p q : Fin (dim κ)) : ↑((lift M κ) T p q) = entry M κ (↑T) ((eκ κ).symm p) ((eκ κ).symm q)

theorem CommutingRepetition.Block.τ_lift (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (T : ↥(blockAlg M κ)) : (N M κ).τ ((lift M κ) T) = (↑(dim κ))⁻¹ * ∑ r : κ, M.traceState (entry M κ (↑T) r r)

The amplified trace of a lifted block operator: d⁻¹ ∑ᵣ φ(entry T r r).

The corner copy of vnAlg M

theorem CommutingRepetition.Block.entry_corner (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (s : κ) (T : M.H →L[ℂ] M.H) (r r' : κ) : entry M κ (embed M κ s ∘SL T ∘SL proj M κ s) r r' = if r = s ∧ r' = s then T else 0

theorem CommutingRepetition.Block.corner_mem (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (s : κ) (T : ↥M.vnAlg) : embed M κ s ∘SL ↑T ∘SL proj M κ s ∈ blockAlg M κ

noncomputable def CommutingRepetition.Block.E (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (s : κ) (T : ↥M.vnAlg) : ↥(blockAlg M κ)

The corner copy E s T = embed s ∘ T ∘ proj s.

Equations

• CommutingRepetition.Block.E M κ s T = ⟨CommutingRepetition.Block.embed M κ s ∘SL ↑T ∘SL CommutingRepetition.Block.proj M κ s, ⋯⟩

theorem CommutingRepetition.Block.E_val (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (s : κ) (T : ↥M.vnAlg) : ↑(E M κ s T) = embed M κ s ∘SL ↑T ∘SL proj M κ s

theorem CommutingRepetition.Block.E_mul (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (s : κ) (T T' : ↥M.vnAlg) : E M κ s (T * T') = E M κ s T * E M κ s T'

theorem CommutingRepetition.Block.E_star (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (s : κ) (T : ↥M.vnAlg) : E M κ s (star T) = star (E M κ s T)

theorem CommutingRepetition.Block.E_add (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (s : κ) (T T' : ↥M.vnAlg) : E M κ s (T + T') = E M κ s T + E M κ s T'

theorem CommutingRepetition.Block.E_sub (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (s : κ) (T T' : ↥M.vnAlg) : E M κ s (T - T') = E M κ s T - E M κ s T'

theorem CommutingRepetition.Block.E_smul (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (s : κ) (c : ℂ) (T : ↥M.vnAlg) : E M κ s (c • T) = c • E M κ s T

theorem CommutingRepetition.Block.E_zero (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (s : κ) : E M κ s 0 = 0

noncomputable def CommutingRepetition.Block.Eadd (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (s : κ) : ↥M.vnAlg →+ ↥(blockAlg M κ)

The corner copy as an additive monoid homomorphism.

Equations

• CommutingRepetition.Block.Eadd M κ s = { toFun := CommutingRepetition.Block.E M κ s, map_zero' := ⋯, map_add' := ⋯ }

theorem CommutingRepetition.Block.E_sum (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (s : κ) {ι : Type u_1} (t : Finset ι) (f : ι → ↥M.vnAlg) : E M κ s (∑ x ∈ t, f x) = ∑ x ∈ t, E M κ s (f x)

theorem CommutingRepetition.Block.τ_lift_E (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (s : κ) (T : ↥M.vnAlg) : (N M κ).τ ((lift M κ) (E M κ s T)) = (↑(dim κ))⁻¹ * M.traceState ↑T

τ_N (lift (E s T)) = d⁻¹ φ(T).

Placement, matrix units and the block-diagonal right action

noncomputable def CommutingRepetition.Block.place (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] (r r' : κ) : (M.H →L[ℂ] M.H) →L[ℂ] BH M κ →L[ℂ] BH M κ

X ↦ embed r ∘ X ∘ proj r' as a continuous linear map.

Equations

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

theorem CommutingRepetition.Block.place_apply (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (r r' : κ) (X : M.H →L[ℂ] M.H) : (place M κ r r') X = embed M κ r ∘SL X ∘SL proj M κ r'

theorem CommutingRepetition.Block.place_apply_vec (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (r r' : κ) (X : M.H →L[ℂ] M.H) (w : BH M κ) : ((place M κ r r') X) w = (embed M κ r) (X (w.ofLp r'))

theorem CommutingRepetition.Block.entry_place (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (r r' : κ) (X : M.H →L[ℂ] M.H) (q q' : κ) : entry M κ ((place M κ r r') X) q q' = if q = r ∧ q' = r' then X else 0

theorem CommutingRepetition.Block.place_mem (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (r r' : κ) {T : M.H →L[ℂ] M.H} (hT : T ∈ M.vnAlg) : (place M κ r r') T ∈ blockAlg M κ

theorem CommutingRepetition.Block.entry_sum (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] {ι : Type u_1} (s : Finset ι) (T : ι → BH M κ →L[ℂ] BH M κ) (r r' : κ) : entry M κ (∑ i ∈ s, T i) r r' = ∑ i ∈ s, entry M κ (T i) r r'

theorem CommutingRepetition.Block.ext_entry (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] {T T' : BH M κ →L[ℂ] BH M κ} (h : ∀ (r r' : κ), entry M κ T r r' = entry M κ T' r r') : T = T'

Two block operators with the same entries are equal.

theorem CommutingRepetition.Block.place_mul_place (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (r r' q q' : κ) (X Y : M.H →L[ℂ] M.H) : (place M κ r r') X * (place M κ q q') Y = if r' = q then (place M κ r q') (X * Y) else 0

theorem CommutingRepetition.Block.star_place (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (r r' : κ) (X : M.H →L[ℂ] M.H) : star ((place M κ r r') X) = (place M κ r' r) (star X)

theorem CommutingRepetition.Block.place_one_mul_mul_place_one (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (s r r' s' : κ) (W : BH M κ →L[ℂ] BH M κ) : (place M κ s r) 1 * W * (place M κ r' s') 1 = (place M κ s s') (entry M κ W r r')

noncomputable def CommutingRepetition.Block.Rt (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] (b : M.A) : BH M κ →L[ℂ] BH M κ

The block-diagonal right action diag (R b).

Equations

• CommutingRepetition.Block.Rt M κ b = ∑ r : κ, (CommutingRepetition.Block.place M κ r r) (M.Rop b)

theorem CommutingRepetition.Block.entry_Rt (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (b : M.A) (r r' : κ) : entry M κ (Rt M κ b) r r' = if r = r' then M.Rop b else 0

theorem CommutingRepetition.Block.entry_mul_Rt (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (T : BH M κ →L[ℂ] BH M κ) (b : M.A) (r r' : κ) : entry M κ (T * Rt M κ b) r r' = entry M κ T r r' * M.Rop b

theorem CommutingRepetition.Block.entry_Rt_mul (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (T : BH M κ →L[ℂ] BH M κ) (b : M.A) (r r' : κ) : entry M κ (Rt M κ b * T) r r' = M.Rop b * entry M κ T r r'

theorem CommutingRepetition.Block.star_Rt (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] (b : M.A) : star (Rt M κ b) = Rt M κ (star b)

theorem CommutingRepetition.Block.mem_blockAlg_iff_comm (M : StdTracialAlgebra) (κ : Type) [Fintype κ] [DecidableEq κ] [Nonempty κ] {T : BH M κ →L[ℂ] BH M κ} : T ∈ blockAlg M κ ↔ ∀ (b : M.A), Rt M κ b * T = T * Rt M κ b

Membership in the block algebra is commutation with the block-diagonal right action.