Local isometries between ancilla extensions

The introspection analysis moves a strategy between extensions of one bipartite model by finite registers (BipartiteModel.expand): it splits a register into two, relabels one, adjoins one on which the strategy does nothing, reads a register on the other player's side, and adjoins the answer register of a Naimark dilation. In the tensor-product model each of these is a permutation of computational basis labels of ℂ^{register} ⊗ ℂ^{d} (MIPRE.Introspection.registerOp, registerParty, registerExtend). In a bipartite model each is a local isometry (BipartiteModel.LocalIsometry) carrying the state of one extension exactly to the state of the other, so that it carries every Born probability and state norm over (LocalIsometry.bornProb_of_W_ψ, LocalIsometry.stateSqNorm_of_W_ψ). Four of them generate the rest:

• an inert ancilla (BipartiteModel.inert): M into M.expand e for a unit vector e, the players' operators acting as X ⊗ 1;
• a relabelling of the registers (BipartiteModel.relabel);
• associativity (BipartiteModel.assoc): an extension of an extension is an extension by the product registers, the players' block matrices of block matrices becoming block matrices (Matrix.comp);
• the exchange of the players (BipartiteModel.swapExpand): the extension of the exchanged model is the exchanged extension.

The entrywise action of an extension's operators (expand_π_πA_apply, expand_π_πB_apply) is what every intertwining identity here reduces to.

Isometries of ℓ² sums

noncomputable def MIPRE.OperatorMatrix.amplReindex {ι : Type u_1} {κ : Type u_2} {H : Type u_3} [Fintype ι] [Fintype κ] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (e : κ ≃ ι) : Ampl ι H →ₗᵢ[ℂ] Ampl κ H

The isometry of ℓ² sums induced by a bijection of the index sets: (v ↦ v ∘ e).

Equations

• MIPRE.OperatorMatrix.amplReindex e = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ H e.symm).toLinearIsometry

@[simp]

theorem MIPRE.OperatorMatrix.amplReindex_apply {ι : Type u_1} {κ : Type u_2} {H : Type u_3} [Fintype ι] [Fintype κ] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (e : κ ≃ ι) (v : Ampl ι H) (k : κ) : ((amplReindex e) v).ofLp k = v.ofLp (e k)

def MIPRE.OperatorMatrix.amplUncurry {ι : Type u_1} {κ : Type u_2} {H : Type u_3} [Fintype ι] [Fintype κ] [NormedAddCommGroup H] [InnerProductSpace ℂ H] : Ampl ι (Ampl κ H) →ₗᵢ[ℂ] Ampl (ι × κ) H

The ℓ² sum of ℓ² sums, as one ℓ² sum over the pairs of indices.

Equations

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

@[simp]

theorem MIPRE.OperatorMatrix.amplUncurry_apply {ι : Type u_1} {κ : Type u_2} {H : Type u_3} [Fintype ι] [Fintype κ] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (v : Ampl ι (Ampl κ H)) (q : ι × κ) : (amplUncurry v).ofLp q = (v.ofLp q.1).ofLp q.2

def MIPRE.OperatorMatrix.amplCurry {ι : Type u_1} {κ : Type u_2} {H : Type u_3} [Fintype ι] [Fintype κ] [NormedAddCommGroup H] [InnerProductSpace ℂ H] : Ampl (ι × κ) H →ₗᵢ[ℂ] Ampl ι (Ampl κ H)

One ℓ² sum over the pairs of indices, as the ℓ² sum of ℓ² sums.

Equations

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

@[simp]

theorem MIPRE.OperatorMatrix.amplCurry_apply {ι : Type u_1} {κ : Type u_2} {H : Type u_3} [Fintype ι] [Fintype κ] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (v : Ampl (ι × κ) H) (i : ι) (k : κ) : ((amplCurry v).ofLp i).ofLp k = v.ofLp (i, k)

Matrices over a star ring as ⋆-homomorphisms

def MIPRE.diagHom {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {α : Type u_2} [Fintype α] [DecidableEq α] : R →⋆ₙₐ[ℂ] Matrix α α R

The constant diagonal X ↦ X ⊗ 1, as a ⋆-homomorphism.

Equations

• MIPRE.diagHom = { toFun := fun (X : R) => Matrix.diagonal fun (x : α) => X, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }

@[simp]

theorem MIPRE.diagHom_apply {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {α : Type u_2} [Fintype α] [DecidableEq α] (X : R) : diagHom X = Matrix.diagonal fun (x : α) => X

theorem MIPRE.diagHom_one {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {α : Type u_2} [Fintype α] [DecidableEq α] : diagHom 1 = 1

def MIPRE.submatrixHom {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {α : Type u_2} {α' : Type u_3} [Fintype α] [Fintype α'] (f : α' ≃ α) : Matrix α α R →⋆ₙₐ[ℂ] Matrix α' α' R

Relabelling the rows and columns of a square matrix along a bijection, as a ⋆-homomorphism.

Equations

• MIPRE.submatrixHom f = { toFun := fun (X : Matrix α α R) => X.submatrix ⇑f ⇑f, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }

@[simp]

theorem MIPRE.submatrixHom_apply {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {α : Type u_2} {α' : Type u_3} [Fintype α] [Fintype α'] (f : α' ≃ α) (X : Matrix α α R) : (submatrixHom f) X = X.submatrix ⇑f ⇑f

theorem MIPRE.submatrixHom_one {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {α : Type u_2} {α' : Type u_3} [Fintype α] [DecidableEq α] [Fintype α'] [DecidableEq α'] (f : α' ≃ α) : (submatrixHom f) 1 = 1

def MIPRE.compHom {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {α : Type u_2} {α' : Type u_3} [Fintype α] [Fintype α'] : Matrix α' α' (Matrix α α R) →⋆ₙₐ[ℂ] Matrix (α' × α) (α' × α) R

Block matrices of block matrices as block matrices over the pairs (Matrix.comp), as a ⋆-homomorphism.

Equations

• MIPRE.compHom = { toFun := fun (X : Matrix α' α' (Matrix α α R)) => (Matrix.comp α' α' α α R) X, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }

@[simp]

theorem MIPRE.compHom_apply {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {α : Type u_2} {α' : Type u_3} [Fintype α] [Fintype α'] (X : Matrix α' α' (Matrix α α R)) (p q : α' × α) : compHom X p q = X p.1 q.1 p.2 q.2

theorem MIPRE.compHom_one {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {α : Type u_2} {α' : Type u_3} [Fintype α] [DecidableEq α] [Fintype α'] [DecidableEq α'] : compHom 1 = 1

def MIPRE.uncompHom {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {α : Type u_2} {α' : Type u_3} [Fintype α] [Fintype α'] : Matrix (α' × α) (α' × α) R →⋆ₙₐ[ℂ] Matrix α' α' (Matrix α α R)

Block matrices over pairs as block matrices of block matrices, the inverse of compHom.

Equations

• MIPRE.uncompHom = { toFun := fun (X : Matrix (α' × α) (α' × α) R) => (Matrix.comp α' α' α α R).symm X, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }

@[simp]

theorem MIPRE.uncompHom_apply {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {α : Type u_2} {α' : Type u_3} [Fintype α] [Fintype α'] (X : Matrix (α' × α) (α' × α) R) (i j : α') (k l : α) : uncompHom X i j k l = X (i, k) (j, l)

@[simp]

theorem MIPRE.compHom_uncompHom {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {α : Type u_2} {α' : Type u_3} [Fintype α] [Fintype α'] (X : Matrix (α' × α) (α' × α) R) : compHom (uncompHom X) = X

@[simp]

theorem MIPRE.uncompHom_compHom {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {α : Type u_2} {α' : Type u_3} [Fintype α] [Fintype α'] (X : Matrix α' α' (Matrix α α R)) : uncompHom (compHom X) = X

theorem MIPRE.uncompHom_one {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {α : Type u_2} {α' : Type u_3} [Fintype α] [DecidableEq α] [Fintype α'] [DecidableEq α'] : uncompHom 1 = 1

The action of an extension, entry by entry

A vector of an extension is a vector of the ℓ² sum Ampl (α × β) M.H, definitionally but not syntactically; BipartiteModel.ampl is that identification, as an isometry, so that the components of a vector of an extension can be read and rewritten.

noncomputable def MIPRE.BipartiteModel.ampl {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) : (M.expand e).H ≃ₗᵢ[ℂ] OperatorMatrix.Ampl (α × β) M.H

The Hilbert space of an extension is the ℓ² sum.

Equations

• M.ampl e = LinearIsometryEquiv.refl ℂ (MIPRE.OperatorMatrix.Ampl (α × β) M.H)

theorem MIPRE.BipartiteModel.expand_ext {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) {v w : (M.expand e).H} (h : ∀ (p : α × β), ((M.ampl e) v).ofLp p = ((M.ampl e) w).ofLp p) : v = w

Two vectors of an extension are equal if their components are.

theorem MIPRE.BipartiteModel.expand_π_πA_apply {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) (X : Matrix α α 𝒜) (v : (M.expand e).H) (p : α × β) : ((M.ampl e) (((M.expand e).π ((M.expand e).πA X)) v)).ofLp p = ∑ a : α, (M.π (M.πA (X p.1 a))) (((M.ampl e) v).ofLp (a, p.2))

The first player's operators of an extension act on the first register.

theorem MIPRE.BipartiteModel.expand_π_πB_apply {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) (Y : Matrix β β ℬ) (v : (M.expand e).H) (p : α × β) : ((M.ampl e) (((M.expand e).π ((M.expand e).πB Y)) v)).ofLp p = ∑ b : β, (M.π (M.πB (Y p.2 b))) (((M.ampl e) v).ofLp (p.1, b))

The second player's operators of an extension act on the second register.

theorem MIPRE.BipartiteModel.expand_ψ_apply {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) (p : α × β) : ((M.ampl e) (M.expand e).ψ).ofLp p = e p • M.ψ

An inert ancilla

def MIPRE.BipartiteModel.tensorLeft {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} (e : α × β → ℂ) : M.H →ₗ[ℂ] OperatorMatrix.Ampl (α × β) M.H

The vector e ⊗ v of the ℓ² sum.

Equations

• M.tensorLeft e = { toFun := fun (v : M.H) => WithLp.toLp 2 fun (p : α × β) => e p • v, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem MIPRE.BipartiteModel.tensorLeft_apply {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} (e : α × β → ℂ) (v : M.H) (p : α × β) : ((M.tensorLeft e) v).ofLp p = e p • v

theorem MIPRE.BipartiteModel.norm_tensorLeft {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] (e : α × β → ℂ) (v : M.H) : ‖(M.tensorLeft e) v‖ = ‖evec e‖ * ‖v‖

noncomputable def MIPRE.BipartiteModel.ancillaIsometry {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) (he : ‖evec e‖ = 1) : M.H →ₗᵢ[ℂ] (M.expand e).H

v ↦ e ⊗ v, an isometry into the extension for a unit vector e.

Equations

• M.ancillaIsometry e he = (M.ampl e).symm.toLinearIsometry.comp (let __LinearMap := M.tensorLeft e; { toLinearMap := __LinearMap, norm_map' := ⋯ })

@[simp]

theorem MIPRE.BipartiteModel.ampl_ancillaIsometry {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) (he : ‖evec e‖ = 1) (v : M.H) : (M.ampl e) ((M.ancillaIsometry e he) v) = (M.tensorLeft e) v

noncomputable def MIPRE.BipartiteModel.inert {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) (he : ‖evec e‖ = 1) : M.LocalIsometry (M.expand e)

An inert ancilla in the unit vector e: M into its extension, the players' operators acting as X ⊗ 1. It carries the state of M to the state of the extension.

Equations

• M.inert e he = { W := M.ancillaIsometry e he, ΦA := MIPRE.diagHom, ΦB := MIPRE.diagHom, intertwineA := ⋯, intertwineB := ⋯ }

theorem MIPRE.BipartiteModel.inert_W_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) (he : ‖evec e‖ = 1) : (M.inert e he).W M.ψ = (M.expand e).ψ

@[simp]

theorem MIPRE.BipartiteModel.inert_ΦA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) (he : ‖evec e‖ = 1) (a : 𝒜) : (M.inert e he).ΦA a = Matrix.diagonal fun (x : α) => a

@[simp]

theorem MIPRE.BipartiteModel.inert_ΦB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) (he : ‖evec e‖ = 1) (b : ℬ) : (M.inert e he).ΦB b = Matrix.diagonal fun (x : β) => b

Relabelling the registers

noncomputable def MIPRE.BipartiteModel.relabelIsometry {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} {α' : Type u_6} {β' : Type u_7} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [Fintype α'] [DecidableEq α'] [Fintype β'] [DecidableEq β'] (e : α × β → ℂ) (e' : α' × β' → ℂ) (f : α' ≃ α) (g : β' ≃ β) : (M.expand e).H →ₗᵢ[ℂ] (M.expand e').H

The isometry of the extensions relabelling the registers along f and g.

Equations

• M.relabelIsometry e e' f g = (M.ampl e').symm.toLinearIsometry.comp ((MIPRE.OperatorMatrix.amplReindex (f.prodCongr g)).comp (M.ampl e).toLinearIsometry)

@[simp]

theorem MIPRE.BipartiteModel.ampl_relabelIsometry {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} {α' : Type u_6} {β' : Type u_7} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [Fintype α'] [DecidableEq α'] [Fintype β'] [DecidableEq β'] (e : α × β → ℂ) (e' : α' × β' → ℂ) (f : α' ≃ α) (g : β' ≃ β) (v : (M.expand e).H) (p : α' × β') : ((M.ampl e') ((M.relabelIsometry e e' f g) v)).ofLp p = ((M.ampl e) v).ofLp (f p.1, g p.2)

noncomputable def MIPRE.BipartiteModel.relabel {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} {α' : Type u_6} {β' : Type u_7} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [Fintype α'] [DecidableEq α'] [Fintype β'] [DecidableEq β'] (e : α × β → ℂ) (e' : α' × β' → ℂ) (f : α' ≃ α) (g : β' ≃ β) : (M.expand e).LocalIsometry (M.expand e')

A relabelling of the registers, along bijections f and g, from the extension in e to the extension in the relabelled vector e'.

Equations

• M.relabel e e' f g = { W := M.relabelIsometry e e' f g, ΦA := MIPRE.submatrixHom f, ΦB := MIPRE.submatrixHom g, intertwineA := ⋯, intertwineB := ⋯ }

theorem MIPRE.BipartiteModel.relabel_W_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} {α' : Type u_6} {β' : Type u_7} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [Fintype α'] [DecidableEq α'] [Fintype β'] [DecidableEq β'] (e : α × β → ℂ) (e' : α' × β' → ℂ) (f : α' ≃ α) (g : β' ≃ β) (he : ∀ (p : α' × β'), e' p = e (f p.1, g p.2)) : (M.relabel e e' f g).W (M.expand e).ψ = (M.expand e').ψ

@[simp]

theorem MIPRE.BipartiteModel.relabel_ΦA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} {α' : Type u_6} {β' : Type u_7} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [Fintype α'] [DecidableEq α'] [Fintype β'] [DecidableEq β'] (e : α × β → ℂ) (e' : α' × β' → ℂ) (f : α' ≃ α) (g : β' ≃ β) (a : Matrix α α 𝒜) : (M.relabel e e' f g).ΦA a = a.submatrix ⇑f ⇑f

@[simp]

theorem MIPRE.BipartiteModel.relabel_ΦB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} {α' : Type u_6} {β' : Type u_7} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [Fintype α'] [DecidableEq α'] [Fintype β'] [DecidableEq β'] (e : α × β → ℂ) (e' : α' × β' → ℂ) (f : α' ≃ α) (g : β' ≃ β) (b : Matrix β β ℬ) : (M.relabel e e' f g).ΦB b = b.submatrix ⇑g ⇑g

Associativity

noncomputable def MIPRE.BipartiteModel.assocIsometry {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} {α' : Type u_6} {β' : Type u_7} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [Fintype α'] [DecidableEq α'] [Fintype β'] [DecidableEq β'] (e : α × β → ℂ) (e' : α' × β' → ℂ) (e'' : (α' × α) × β' × β → ℂ) : ((M.expand e).expand e').H →ₗᵢ[ℂ] (M.expand e'').H

The isometry of an extension of an extension onto the extension by the product registers.

Equations

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

@[simp]

theorem MIPRE.BipartiteModel.ampl_assocIsometry {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} {α' : Type u_6} {β' : Type u_7} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [Fintype α'] [DecidableEq α'] [Fintype β'] [DecidableEq β'] (e : α × β → ℂ) (e' : α' × β' → ℂ) (e'' : (α' × α) × β' × β → ℂ) (v : ((M.expand e).expand e').H) (q : (α' × α) × β' × β) : ((M.ampl e'') ((M.assocIsometry e e' e'') v)).ofLp q = ((M.ampl e) ((((M.expand e).ampl e') v).ofLp (q.1.1, q.2.1))).ofLp (q.1.2, q.2.2)

noncomputable def MIPRE.BipartiteModel.assoc {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} {α' : Type u_6} {β' : Type u_7} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [Fintype α'] [DecidableEq α'] [Fintype β'] [DecidableEq β'] (e : α × β → ℂ) (e' : α' × β' → ℂ) (e'' : (α' × α) × β' × β → ℂ) : ((M.expand e).expand e').LocalIsometry (M.expand e'')

Associativity: the extension in e' of the extension in e into the extension by the product registers, in any vector e'' that is the product of the two.

Equations

• M.assoc e e' e'' = { W := M.assocIsometry e e' e'', ΦA := MIPRE.compHom, ΦB := MIPRE.compHom, intertwineA := ⋯, intertwineB := ⋯ }

theorem MIPRE.BipartiteModel.assoc_W_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} {α' : Type u_6} {β' : Type u_7} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [Fintype α'] [DecidableEq α'] [Fintype β'] [DecidableEq β'] (e : α × β → ℂ) (e' : α' × β' → ℂ) (e'' : (α' × α) × β' × β → ℂ) (he : ∀ (q : (α' × α) × β' × β), e'' q = e' (q.1.1, q.2.1) * e (q.1.2, q.2.2)) : (M.assoc e e' e'').W ((M.expand e).expand e').ψ = (M.expand e'').ψ

@[simp]

theorem MIPRE.BipartiteModel.assoc_ΦA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} {α' : Type u_6} {β' : Type u_7} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [Fintype α'] [DecidableEq α'] [Fintype β'] [DecidableEq β'] (e : α × β → ℂ) (e' : α' × β' → ℂ) (e'' : (α' × α) × β' × β → ℂ) (a : Matrix α' α' (Matrix α α 𝒜)) : (M.assoc e e' e'').ΦA a = compHom a

@[simp]

theorem MIPRE.BipartiteModel.assoc_ΦB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} {α' : Type u_6} {β' : Type u_7} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [Fintype α'] [DecidableEq α'] [Fintype β'] [DecidableEq β'] (e : α × β → ℂ) (e' : α' × β' → ℂ) (e'' : (α' × α) × β' × β → ℂ) (b : Matrix β' β' (Matrix β β ℬ)) : (M.assoc e e' e'').ΦB b = compHom b

Exchanging the players

noncomputable def MIPRE.BipartiteModel.swapIsometry {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) (e' : β × α → ℂ) : (M.expand e).swap.H →ₗᵢ[ℂ] (M.swap.expand e').H

The isometry of the exchanged extension onto the extension of the exchanged model.

Equations

• M.swapIsometry e e' = (M.swap.ampl e').symm.toLinearIsometry.comp ((MIPRE.OperatorMatrix.amplReindex (Equiv.prodComm β α)).comp (M.ampl e).toLinearIsometry)

@[simp]

theorem MIPRE.BipartiteModel.ampl_swapIsometry {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) (e' : β × α → ℂ) (v : (M.expand e).swap.H) (p : β × α) : ((M.swap.ampl e') ((M.swapIsometry e e') v)).ofLp p = ((M.ampl e) v).ofLp p.swap

noncomputable def MIPRE.BipartiteModel.swapExpand {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) (e' : β × α → ℂ) : (M.expand e).swap.LocalIsometry (M.swap.expand e')

The exchange of the players: the exchanged extension into the extension of the exchanged model, in the exchanged vector.

Equations

• M.swapExpand e e' = { W := M.swapIsometry e e', ΦA := NonUnitalStarAlgHom.id ℂ (Matrix β β ℬ), ΦB := NonUnitalStarAlgHom.id ℂ (Matrix α α 𝒜), intertwineA := ⋯, intertwineB := ⋯ }

theorem MIPRE.BipartiteModel.swapExpand_W_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) (e' : β × α → ℂ) (he : ∀ (p : β × α), e' p = e p.swap) : (M.swapExpand e e').W (M.expand e).swap.ψ = (M.swap.expand e').ψ