Isomorphisms of bipartite models

A local isometry (BipartiteModel.LocalIsometry) moves a strategy from one model into another, and carries its value over on the transported state. When the isometry is onto, the two homomorphisms are bijective and the state goes to the state, nothing is lost in either direction: the two models are isomorphic (BipartiteModel.Iso), and a property of models stated through Born probabilities --- the soundness of a test, the domination of the strategies by a value --- passes from either to the other. The constructions of MIPRE/Foundations/AncillaIsometry.lean and MIPRE/Foundations/TensorExpand.lean are isomorphisms in this sense, once their state hypotheses hold:

• an extension by one-point registers in the state 1 is the model itself (BipartiteModel.expandUnit);
• associativity of extensions (BipartiteModel.assocIso), relabelling of the registers (BipartiteModel.relabelIso), and the exchange of the players in an extension (BipartiteModel.swapExpandIso);
• an isomorphism of models extends to their extensions by the same registers (BipartiteModel.Iso.expandCongr);
• the extension of a tensor-product model is the tensor-product model of the expanded vector (BipartiteModel.tensorExpandIso), and a tensor-product model is unchanged by relabelling the two factors (BipartiteModel.tensorReindexIso), so that a statement about the tensor-product models of states on Fin a × Fin b holds on any finite factors.

Each of these is a local isometry of those files with inverses (Iso.ofLocalIsometry), and every isomorphism is a local isometry (Iso.toLocalIsometry), so the lemmas about local isometries carrying the state to the state apply. What an isomorphism carries over, exactly: Born probabilities (Iso.bornProb_eq), the players' state norms (Iso.stateSqNorm_eq), the value of a family of measurements and of a projective strategy pushed forward (Iso.povmValue_push, Iso.value_pushStrat, and so the domination of a model by a value, Iso.dominates), and the inconsistency of two families (Iso.inconsistency_eq). The exchange of the players is an operation on projective strategies too (ProjStrat.swap), which keeps the value of a game that is symmetric in the players, and on inconsistencies (BipartiteModel.inconsistency_swap).

A one-point ℓ² sum, exchanged registers, and three ⋆-algebra isomorphisms of matrices

def MIPRE.OperatorMatrix.amplSubsingleton {ι : Type u_1} {H : Type u_2} [Fintype ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [Subsingleton ι] (i₀ : ι) : Ampl ι H ≃ₗᵢ[ℂ] H

The ℓ² sum over a one-point index {i₀} is the space itself.

Equations

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

@[simp]

theorem MIPRE.OperatorMatrix.amplSubsingleton_apply {ι : Type u_1} {H : Type u_2} [Fintype ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [Subsingleton ι] (i₀ : ι) (v : Ampl ι H) : (amplSubsingleton i₀) v = v.ofLp i₀

theorem MIPRE.norm_evec_comp_swap {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (e : α × β → ℂ) : ‖evec (e ∘ Prod.swap)‖ = ‖evec e‖

Exchanging the two registers of a vector keeps its norm.

def MIPRE.matrixUnitStarAlgEquiv (R : Type u_1) [Ring R] [StarRing R] [Algebra ℂ R] : Matrix Unit Unit R ≃⋆ₐ[ℂ] R

One-by-one matrices over a ⋆-algebra are the algebra.

Equations

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

@[simp]

theorem MIPRE.matrixUnitStarAlgEquiv_apply {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (X : Matrix Unit Unit R) : (matrixUnitStarAlgEquiv R) X = X () ()

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

Relabelling the rows and columns of square matrices along a bijection, as a ⋆-algebra isomorphism.

Equations

• MIPRE.submatrixStarAlgEquiv f = StarAlgEquiv.ofNonUnitalStarAlgHom (MIPRE.submatrixHom f) (MIPRE.submatrixHom f.symm) ⋯ ⋯

@[simp]

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

@[simp]

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

def MIPRE.mapMatrixStarAlgEquiv {R : Type u_1} {S : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [Ring S] [StarRing S] [Algebra ℂ S] {α : Type u_3} [Fintype α] [DecidableEq α] (f : R ≃⋆ₐ[ℂ] S) : Matrix α α R ≃⋆ₐ[ℂ] Matrix α α S

A ⋆-algebra isomorphism, applied entrywise to square matrices.

Equations

• MIPRE.mapMatrixStarAlgEquiv f = StarAlgEquiv.ofAlgEquiv f.toAlgEquiv.mapMatrix ⋯

@[simp]

theorem MIPRE.mapMatrixStarAlgEquiv_apply {R : Type u_1} {S : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [Ring S] [StarRing S] [Algebra ℂ S] {α : Type u_3} [Fintype α] [DecidableEq α] (f : R ≃⋆ₐ[ℂ] S) (X : Matrix α α R) : (mapMatrixStarAlgEquiv f) X = X.map ⇑f

@[simp]

theorem MIPRE.mapMatrixStarAlgEquiv_symm_apply {R : Type u_1} {S : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [Ring S] [StarRing S] [Algebra ℂ S] {α : Type u_3} [Fintype α] [DecidableEq α] (f : R ≃⋆ₐ[ℂ] S) (X : Matrix α α S) : (mapMatrixStarAlgEquiv f).symm X = X.map ⇑f.symm

Isomorphisms

structure MIPRE.BipartiteModel.Iso {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] (M : BipartiteModel 𝒞 𝒜 ℬ) (M' : BipartiteModel 𝒞' 𝒜' ℬ') : Type (max (max (max (max (max u u') u_2) u_3) u_5) u_6)

An isomorphism of bipartite models: a unitary of the Hilbert spaces carrying the state of M to the state of M', and a ⋆-algebra isomorphism for each player, the two representations intertwined by the unitary. Everything a model computes from its state and its players' operators --- Born probabilities, state norms, values, inconsistencies --- is carried across unchanged.

• W : M.H ≃ₗᵢ[ℂ] M'.H

  The unitary of the Hilbert spaces.

• ΦA : 𝒜 ≃⋆ₐ[ℂ] 𝒜'

  The first player's algebras.

• ΦB : ℬ ≃⋆ₐ[ℂ] ℬ'

  The second player's algebras.

• intertwineA (a : 𝒜) (v : M.H) : (M'.π (M'.πA (self.ΦA a))) (self.W v) = self.W ((M.π (M.πA a)) v)

  The unitary intertwines the first player's operators with their images.

• intertwineB (b : ℬ) (v : M.H) : (M'.π (M'.πB (self.ΦB b))) (self.W v) = self.W ((M.π (M.πB b)) v)

  The unitary intertwines the second player's operators with their images.

• W_ψ : self.W M.ψ = M'.ψ

  The unitary carries the state to the state.

def MIPRE.BipartiteModel.Iso.refl {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) : M.Iso M

The identity isomorphism.

Equations

• MIPRE.BipartiteModel.Iso.refl M = { W := LinearIsometryEquiv.refl ℂ M.H, ΦA := StarAlgEquiv.refl ℂ 𝒜, ΦB := StarAlgEquiv.refl ℂ ℬ, intertwineA := ⋯, intertwineB := ⋯, W_ψ := ⋯ }

def MIPRE.BipartiteModel.Iso.symm {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.Iso M') : M'.Iso M

The inverse isomorphism.

Equations

• Φ.symm = { W := Φ.W.symm, ΦA := Φ.ΦA.symm, ΦB := Φ.ΦB.symm, intertwineA := ⋯, intertwineB := ⋯, W_ψ := ⋯ }

def MIPRE.BipartiteModel.Iso.trans {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} {𝒞'' : Type u_7} {𝒜'' : Type u_8} {ℬ'' : Type u_9} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] [Ring 𝒞''] [StarRing 𝒞''] [Algebra ℂ 𝒞''] [Ring 𝒜''] [StarRing 𝒜''] [Algebra ℂ 𝒜''] [Ring ℬ''] [StarRing ℬ''] [Algebra ℂ ℬ''] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {M'' : BipartiteModel 𝒞'' 𝒜'' ℬ''} (Φ : M.Iso M') (Φ' : M'.Iso M'') : M.Iso M''

Isomorphisms compose, the first applied first.

Equations

• Φ.trans Φ' = { W := Φ.W.trans Φ'.W, ΦA := Φ.ΦA.trans Φ'.ΦA, ΦB := Φ.ΦB.trans Φ'.ΦB, intertwineA := ⋯, intertwineB := ⋯, W_ψ := ⋯ }

def MIPRE.BipartiteModel.Iso.swap {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.Iso M') : M.swap.Iso M'.swap

The isomorphism with the players exchanged.

Equations

• Φ.swap = { W := Φ.W, ΦA := Φ.ΦB, ΦB := Φ.ΦA, intertwineA := ⋯, intertwineB := ⋯, W_ψ := ⋯ }

@[simp]

theorem MIPRE.BipartiteModel.Iso.refl_ΦA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (a : 𝒜) : (refl M).ΦA a = a

@[simp]

theorem MIPRE.BipartiteModel.Iso.refl_ΦB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (b : ℬ) : (refl M).ΦB b = b

@[simp]

theorem MIPRE.BipartiteModel.Iso.symm_W {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.Iso M') : Φ.symm.W = Φ.W.symm

@[simp]

theorem MIPRE.BipartiteModel.Iso.symm_ΦA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.Iso M') : Φ.symm.ΦA = Φ.ΦA.symm

@[simp]

theorem MIPRE.BipartiteModel.Iso.symm_ΦB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.Iso M') : Φ.symm.ΦB = Φ.ΦB.symm

@[simp]

theorem MIPRE.BipartiteModel.Iso.trans_W {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} {𝒞'' : Type u_7} {𝒜'' : Type u_8} {ℬ'' : Type u_9} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] [Ring 𝒞''] [StarRing 𝒞''] [Algebra ℂ 𝒞''] [Ring 𝒜''] [StarRing 𝒜''] [Algebra ℂ 𝒜''] [Ring ℬ''] [StarRing ℬ''] [Algebra ℂ ℬ''] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {M'' : BipartiteModel 𝒞'' 𝒜'' ℬ''} (Φ : M.Iso M') (Φ' : M'.Iso M'') (v : M.H) : (Φ.trans Φ').W v = Φ'.W (Φ.W v)

@[simp]

theorem MIPRE.BipartiteModel.Iso.trans_ΦA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} {𝒞'' : Type u_7} {𝒜'' : Type u_8} {ℬ'' : Type u_9} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] [Ring 𝒞''] [StarRing 𝒞''] [Algebra ℂ 𝒞''] [Ring 𝒜''] [StarRing 𝒜''] [Algebra ℂ 𝒜''] [Ring ℬ''] [StarRing ℬ''] [Algebra ℂ ℬ''] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {M'' : BipartiteModel 𝒞'' 𝒜'' ℬ''} (Φ : M.Iso M') (Φ' : M'.Iso M'') (a : 𝒜) : (Φ.trans Φ').ΦA a = Φ'.ΦA (Φ.ΦA a)

@[simp]

theorem MIPRE.BipartiteModel.Iso.trans_ΦB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} {𝒞'' : Type u_7} {𝒜'' : Type u_8} {ℬ'' : Type u_9} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] [Ring 𝒞''] [StarRing 𝒞''] [Algebra ℂ 𝒞''] [Ring 𝒜''] [StarRing 𝒜''] [Algebra ℂ 𝒜''] [Ring ℬ''] [StarRing ℬ''] [Algebra ℂ ℬ''] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {M'' : BipartiteModel 𝒞'' 𝒜'' ℬ''} (Φ : M.Iso M') (Φ' : M'.Iso M'') (b : ℬ) : (Φ.trans Φ').ΦB b = Φ'.ΦB (Φ.ΦB b)

@[simp]

theorem MIPRE.BipartiteModel.Iso.swap_W {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.Iso M') : Φ.swap.W = Φ.W

@[simp]

theorem MIPRE.BipartiteModel.Iso.swap_ΦA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.Iso M') : Φ.swap.ΦA = Φ.ΦB

@[simp]

theorem MIPRE.BipartiteModel.Iso.swap_ΦB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.Iso M') : Φ.swap.ΦB = Φ.ΦA

@[simp]

theorem MIPRE.BipartiteModel.Iso.symm_symm {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.Iso M') : Φ.symm.symm = Φ

@[simp]

theorem MIPRE.BipartiteModel.Iso.swap_swap {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.Iso M') : Φ.swap.swap = Φ

def MIPRE.BipartiteModel.Iso.toLocalIsometry {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.Iso M') : M.LocalIsometry M'

An isomorphism is a local isometry, its homomorphisms unital and its isometry carrying the state to the state (toLocalIsometry_W_ψ).

Equations

• Φ.toLocalIsometry = { W := Φ.W.toLinearIsometry, ΦA := Φ.ΦA.toNonUnitalStarAlgHom, ΦB := Φ.ΦB.toNonUnitalStarAlgHom, intertwineA := ⋯, intertwineB := ⋯ }

@[simp]

theorem MIPRE.BipartiteModel.Iso.toLocalIsometry_W {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.Iso M') (v : M.H) : Φ.toLocalIsometry.W v = Φ.W v

@[simp]

theorem MIPRE.BipartiteModel.Iso.toLocalIsometry_ΦA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.Iso M') (a : 𝒜) : Φ.toLocalIsometry.ΦA a = Φ.ΦA a

@[simp]

theorem MIPRE.BipartiteModel.Iso.toLocalIsometry_ΦB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.Iso M') (b : ℬ) : Φ.toLocalIsometry.ΦB b = Φ.ΦB b

theorem MIPRE.BipartiteModel.Iso.toLocalIsometry_W_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.Iso M') : Φ.toLocalIsometry.W M.ψ = M'.ψ

theorem MIPRE.BipartiteModel.Iso.toLocalIsometry_ΦA_one {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.Iso M') : Φ.toLocalIsometry.ΦA 1 = 1

theorem MIPRE.BipartiteModel.Iso.toLocalIsometry_ΦB_one {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.Iso M') : Φ.toLocalIsometry.ΦB 1 = 1

@[simp]

theorem MIPRE.BipartiteModel.Iso.swap_toLocalIsometry {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.Iso M') : Φ.swap.toLocalIsometry = Φ.toLocalIsometry.swap

def MIPRE.BipartiteModel.Iso.ofLocalIsometry {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') (hψ : Φ.W M.ψ = M'.ψ) (W' : M'.H → M.H) (hW : ∀ (v : M'.H), Φ.W (W' v) = v) (ΨA : 𝒜' → 𝒜) (hA₁ : ∀ (a : 𝒜), ΨA (Φ.ΦA a) = a) (hA₂ : ∀ (a : 𝒜'), Φ.ΦA (ΨA a) = a) (ΨB : ℬ' → ℬ) (hB₁ : ∀ (b : ℬ), ΨB (Φ.ΦB b) = b) (hB₂ : ∀ (b : ℬ'), Φ.ΦB (ΨB b) = b) : M.Iso M'

A local isometry with inverses is an isomorphism: an isometry with a right inverse, and homomorphisms with two-sided inverses, carrying the state to the state.

Equations

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

What an isomorphism carries over

theorem MIPRE.BipartiteModel.Iso.bornProb_eq {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.Iso M') (a : 𝒜) (b : ℬ) : M'.bornProb (Φ.ΦA a) (Φ.ΦB b) = M.bornProb a b

Born probabilities are carried over.

theorem MIPRE.BipartiteModel.Iso.stateSqNorm_eq {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.Iso M') (a : 𝒜) : M'.stateSqNorm (Φ.ΦA a) = M.stateSqNorm a

The first player's state norms are carried over.

theorem MIPRE.BipartiteModel.Iso.swap_stateSqNorm_eq {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.Iso M') (b : ℬ) : M'.swap.stateSqNorm (Φ.ΦB b) = M.swap.stateSqNorm b

The second player's state norms are carried over.

theorem MIPRE.BipartiteModel.Iso.xSqNorm_eq {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.Iso M') (a : 𝒜) (b : ℬ) : M'.xSqNorm (Φ.ΦA a) (Φ.ΦB b) = M.xSqNorm a b

The cross norms are carried over.

theorem MIPRE.BipartiteModel.Iso.norm_ψ_eq {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.Iso M') : ‖M'.ψ‖ = ‖M.ψ‖

The state has the norm of the state.

Measurements and strategies moved along an isomorphism

def MIPRE.BipartiteModel.Iso.pushA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] (Φ : M.Iso M') {X : Type u_10} [Fintype X] (P : POVMIn X 𝒜) : POVMIn X 𝒜'

A POVM of the first player, moved along the isomorphism.

Equations

• Φ.pushA P = MIPRE.POVMIn.pushforward Φ.toLocalIsometry.ΦA ⋯ P

@[simp]

theorem MIPRE.BipartiteModel.Iso.pushA_op {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] (Φ : M.Iso M') {X : Type u_10} [Fintype X] (P : POVMIn X 𝒜) (x : X) : (Φ.pushA P).op x = Φ.ΦA (P.op x)

theorem MIPRE.BipartiteModel.Iso.isPVMIn_pushA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] (Φ : M.Iso M') {X : Type u_10} [Fintype X] {P : POVMIn X 𝒜} (hP : IsPVMIn P.op) : IsPVMIn (Φ.pushA P).op

theorem MIPRE.BipartiteModel.Iso.symm_pushA_pushA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] (Φ : M.Iso M') {X : Type u_10} [Fintype X] (P : POVMIn X 𝒜) : Φ.symm.pushA (Φ.pushA P) = P

theorem MIPRE.BipartiteModel.Iso.pushA_symm_pushA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] (Φ : M.Iso M') {X : Type u_10} [Fintype X] (P : POVMIn X 𝒜') : Φ.pushA (Φ.symm.pushA P) = P

def MIPRE.BipartiteModel.Iso.pushB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} [PartialOrder ℬ] [StarOrderedRing ℬ] [PartialOrder ℬ'] [StarOrderedRing ℬ'] (Φ : M.Iso M') {X : Type u_10} [Fintype X] (Q : POVMIn X ℬ) : POVMIn X ℬ'

A POVM of the second player, moved along the isomorphism.

Equations

• Φ.pushB Q = MIPRE.POVMIn.pushforward Φ.toLocalIsometry.ΦB ⋯ Q

@[simp]

theorem MIPRE.BipartiteModel.Iso.pushB_op {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} [PartialOrder ℬ] [StarOrderedRing ℬ] [PartialOrder ℬ'] [StarOrderedRing ℬ'] (Φ : M.Iso M') {X : Type u_10} [Fintype X] (Q : POVMIn X ℬ) (x : X) : (Φ.pushB Q).op x = Φ.ΦB (Q.op x)

theorem MIPRE.BipartiteModel.Iso.isPVMIn_pushB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} [PartialOrder ℬ] [StarOrderedRing ℬ] [PartialOrder ℬ'] [StarOrderedRing ℬ'] (Φ : M.Iso M') {X : Type u_10} [Fintype X] {Q : POVMIn X ℬ} (hQ : IsPVMIn Q.op) : IsPVMIn (Φ.pushB Q).op

theorem MIPRE.BipartiteModel.Iso.symm_pushB_pushB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} [PartialOrder ℬ] [StarOrderedRing ℬ] [PartialOrder ℬ'] [StarOrderedRing ℬ'] (Φ : M.Iso M') {X : Type u_10} [Fintype X] (Q : POVMIn X ℬ) : Φ.symm.pushB (Φ.pushB Q) = Q

theorem MIPRE.BipartiteModel.Iso.pushB_symm_pushB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} [PartialOrder ℬ] [StarOrderedRing ℬ] [PartialOrder ℬ'] [StarOrderedRing ℬ'] (Φ : M.Iso M') {X : Type u_10} [Fintype X] (Q : POVMIn X ℬ') : Φ.pushB (Φ.symm.pushB Q) = Q

theorem MIPRE.BipartiteModel.Iso.povmValue_eq {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} [PartialOrder 𝒜] [PartialOrder ℬ] [PartialOrder 𝒜'] [PartialOrder ℬ'] (Φ : M.Iso M') {X : Type u_10} {Y : Type u_11} {A : Type u_12} {B : Type u_13} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {PA : X → POVMIn A 𝒜} {PB : Y → POVMIn B ℬ} {PA' : X → POVMIn A 𝒜'} {PB' : Y → POVMIn B ℬ'} (hA : ∀ (x : X) (a : A), (PA' x).op a = Φ.ΦA ((PA x).op a)) (hB : ∀ (y : Y) (b : B), (PB' y).op b = Φ.ΦB ((PB y).op b)) : M'.povmValue G PA' PB' = M.povmValue G PA PB

Two families of measurements whose operators correspond have the same value.

theorem MIPRE.BipartiteModel.Iso.povmValue_push {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} [PartialOrder 𝒜] [PartialOrder ℬ] [PartialOrder 𝒜'] [PartialOrder ℬ'] (Φ : M.Iso M') {X : Type u_10} {Y : Type u_11} {A : Type u_12} {B : Type u_13} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [StarOrderedRing 𝒜] [StarOrderedRing ℬ] [StarOrderedRing 𝒜'] [StarOrderedRing ℬ'] (G : Game X Y A B) (PA : X → POVMIn A 𝒜) (PB : Y → POVMIn B ℬ) : (M'.povmValue G (fun (x : X) => Φ.pushA (PA x)) fun (y : Y) => Φ.pushB (PB y)) = M.povmValue G PA PB

A family of measurements moved along the isomorphism has its value.

def MIPRE.BipartiteModel.Iso.pushStrat {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} [PartialOrder 𝒜] [PartialOrder ℬ] [PartialOrder 𝒜'] [PartialOrder ℬ'] (Φ : M.Iso M') {X : Type u_10} {Y : Type u_11} {A : Type u_12} {B : Type u_13} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [StarOrderedRing 𝒜] [StarOrderedRing ℬ] [StarOrderedRing 𝒜'] [StarOrderedRing ℬ'] {G : Game X Y A B} (S : M.ProjStrat G) : M'.ProjStrat G

A projective strategy moved along the isomorphism: each measurement pushed forward.

Equations

• Φ.pushStrat S = { PA := fun (x : X) => Φ.pushA (S.PA x), PB := fun (y : Y) => Φ.pushB (S.PB y), projA := ⋯, projB := ⋯, ψ_unit := ⋯ }

@[simp]

theorem MIPRE.BipartiteModel.Iso.pushStrat_PA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} [PartialOrder 𝒜] [PartialOrder ℬ] [PartialOrder 𝒜'] [PartialOrder ℬ'] (Φ : M.Iso M') {X : Type u_10} {Y : Type u_11} {A : Type u_12} {B : Type u_13} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [StarOrderedRing 𝒜] [StarOrderedRing ℬ] [StarOrderedRing 𝒜'] [StarOrderedRing ℬ'] {G : Game X Y A B} (S : M.ProjStrat G) (x : X) : (Φ.pushStrat S).PA x = Φ.pushA (S.PA x)

@[simp]

theorem MIPRE.BipartiteModel.Iso.pushStrat_PB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} [PartialOrder 𝒜] [PartialOrder ℬ] [PartialOrder 𝒜'] [PartialOrder ℬ'] (Φ : M.Iso M') {X : Type u_10} {Y : Type u_11} {A : Type u_12} {B : Type u_13} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [StarOrderedRing 𝒜] [StarOrderedRing ℬ] [StarOrderedRing 𝒜'] [StarOrderedRing ℬ'] {G : Game X Y A B} (S : M.ProjStrat G) (y : Y) : (Φ.pushStrat S).PB y = Φ.pushB (S.PB y)

theorem MIPRE.BipartiteModel.Iso.value_pushStrat {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} [PartialOrder 𝒜] [PartialOrder ℬ] [PartialOrder 𝒜'] [PartialOrder ℬ'] (Φ : M.Iso M') {X : Type u_10} {Y : Type u_11} {A : Type u_12} {B : Type u_13} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [StarOrderedRing 𝒜] [StarOrderedRing ℬ] [StarOrderedRing 𝒜'] [StarOrderedRing ℬ'] {G : Game X Y A B} (S : M.ProjStrat G) : (Φ.pushStrat S).value = S.value

A projective strategy moved along the isomorphism has its value.

theorem MIPRE.BipartiteModel.Iso.dominates {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} [PartialOrder 𝒜] [PartialOrder ℬ] [PartialOrder 𝒜'] [PartialOrder ℬ'] [StarOrderedRing 𝒜] [StarOrderedRing ℬ] [StarOrderedRing 𝒜'] [StarOrderedRing ℬ'] (Φ : M.Iso M') {ω : ValueModel} (h : ω.Dominates M') : ω.Dominates M

A value model dominating a model dominates every model isomorphic to it: a projective strategy moves along the isomorphism with its value.

theorem MIPRE.BipartiteModel.Iso.inconsistency_eq {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} [PartialOrder 𝒜] [PartialOrder ℬ] [PartialOrder 𝒜'] [PartialOrder ℬ'] (Φ : M.Iso M') {Λ : Type u_10} {X : Type u_11} [Fintype Λ] [DecidableEq Λ] [Fintype X] (μ : X → ℝ) {P : X → POVMIn Λ 𝒜} {Q : X → POVMIn Λ ℬ} {P' : X → POVMIn Λ 𝒜'} {Q' : X → POVMIn Λ ℬ'} (hP : ∀ (x : X) (a : Λ), (P' x).op a = Φ.ΦA ((P x).op a)) (hQ : ∀ (x : X) (b : Λ), (Q' x).op b = Φ.ΦB ((Q x).op b)) : M'.inconsistency μ P' Q' = M.inconsistency μ P Q

Two pairs of families whose operators correspond have the same inconsistency.

theorem MIPRE.BipartiteModel.Iso.inconsistency_push {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} [PartialOrder 𝒜] [PartialOrder ℬ] [PartialOrder 𝒜'] [PartialOrder ℬ'] (Φ : M.Iso M') {Λ : Type u_10} {X : Type u_11} [Fintype Λ] [DecidableEq Λ] [Fintype X] [StarOrderedRing 𝒜] [StarOrderedRing ℬ] [StarOrderedRing 𝒜'] [StarOrderedRing ℬ'] (μ : X → ℝ) (P : X → POVMIn Λ 𝒜) (Q : X → POVMIn Λ ℬ) : (M'.inconsistency μ (fun (x : X) => Φ.pushA (P x)) fun (x : X) => Φ.pushB (Q x)) = M.inconsistency μ P Q

Two families moved along the isomorphism have their inconsistency.

Exchanging the players in a strategy and in an inconsistency

def MIPRE.BipartiteModel.ProjStrat.swap {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {X : Type u_10} {Y : Type u_11} {A : Type u_12} {B : Type u_13} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : M.ProjStrat G) (G' : Game Y X B A) : M.swap.ProjStrat G'

A projective strategy with the players exchanged, as a strategy of the swapped model for any game G' of the exchanged shape: the first player's measurements are the second's.

Equations

• S.swap G' = { PA := S.PB, PB := S.PA, projA := ⋯, projB := ⋯, ψ_unit := ⋯ }

@[simp]

theorem MIPRE.BipartiteModel.ProjStrat.swap_PA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {X : Type u_10} {Y : Type u_11} {A : Type u_12} {B : Type u_13} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : M.ProjStrat G) (G' : Game Y X B A) : (S.swap G').PA = S.PB

@[simp]

theorem MIPRE.BipartiteModel.ProjStrat.swap_PB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {X : Type u_10} {Y : Type u_11} {A : Type u_12} {B : Type u_13} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : M.ProjStrat G) (G' : Game Y X B A) : (S.swap G').PB = S.PA

theorem MIPRE.BipartiteModel.ProjStrat.value_swap {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {X : Type u_10} {Y : Type u_11} {A : Type u_12} {B : Type u_13} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : M.ProjStrat G) {G' : Game Y X B A} (hμ : ∀ (x : X) (y : Y), G'.μ y x = G.μ x y) (hD : ∀ (x : X) (y : Y) (a : A) (b : B), G'.D y x b a = G.D x y a b) : (S.swap G').value = S.value

The exchanged strategy has the value of the strategy, for a game G' that is G with the players exchanged: the question pair (y, x) weighed as (x, y), and the answers (b, a) accepted as (a, b). For a game symmetric in the players, G' is G itself.

theorem MIPRE.BipartiteModel.inconsistency_swap {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {Λ : Type u_10} {X : Type u_11} [Fintype Λ] [DecidableEq Λ] [Fintype X] (μ : X → ℝ) (P : X → POVMIn Λ 𝒜) (Q : X → POVMIn Λ ℬ) : M.swap.inconsistency μ Q P = M.inconsistency μ P Q

The inconsistency is symmetric in the players: with the players exchanged, the second player's family is measured first.

Isomorphisms between ancilla extensions

noncomputable def MIPRE.BipartiteModel.expandUnit {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) : (M.expand fun (x : Unit × Unit) => 1).Iso M

An extension by one-point registers in the state 1 is the model itself: the one-by-one matrices over each player's algebra are that algebra.

Equations

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

@[simp]

theorem MIPRE.BipartiteModel.expandUnit_ΦA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (X : Matrix Unit Unit 𝒜) : M.expandUnit.ΦA X = X () ()

@[simp]

theorem MIPRE.BipartiteModel.expandUnit_ΦB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (Y : Matrix Unit Unit ℬ) : M.expandUnit.ΦB Y = Y () ()

noncomputable def MIPRE.BipartiteModel.assocIso {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_10} {β : Type u_11} {α' : Type u_12} {β' : Type u_13} [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.expand e).expand e').Iso (M.expand e'')

Associativity, as an isomorphism: the extension in e' of the extension in e is the extension by the product registers, in the product vector e'' (BipartiteModel.assoc).

Equations

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

@[simp]

theorem MIPRE.BipartiteModel.assocIso_ΦA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_10} {β : Type u_11} {α' : Type u_12} {β' : Type u_13} [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)) (a : Matrix α' α' (Matrix α α 𝒜)) : (M.assocIso e e' e'' he).ΦA a = compHom a

@[simp]

theorem MIPRE.BipartiteModel.assocIso_ΦB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_10} {β : Type u_11} {α' : Type u_12} {β' : Type u_13} [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)) (b : Matrix β' β' (Matrix β β ℬ)) : (M.assocIso e e' e'' he).ΦB b = compHom b

noncomputable def MIPRE.BipartiteModel.swapExpandIso {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_10} {β : Type u_11} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) : (M.expand e).swap.Iso (M.swap.expand (e ∘ Prod.swap))

The exchange of the players, as an isomorphism: the exchanged extension in e is the extension of the exchanged model in the exchanged vector (BipartiteModel.swapExpand).

Equations

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

@[simp]

theorem MIPRE.BipartiteModel.swapExpandIso_ΦA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_10} {β : Type u_11} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) (b : Matrix β β ℬ) : (M.swapExpandIso e).ΦA b = b

@[simp]

theorem MIPRE.BipartiteModel.swapExpandIso_ΦB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_10} {β : Type u_11} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) (a : Matrix α α 𝒜) : (M.swapExpandIso e).ΦB a = a

noncomputable def MIPRE.BipartiteModel.relabelIso {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_10} {β : Type u_11} {α' : Type u_12} {β' : Type u_13} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [Fintype α'] [DecidableEq α'] [Fintype β'] [DecidableEq β'] (e : α × β → ℂ) (e' : α' × β' → ℂ) (f : α' ≃ α) (g : β' ≃ β) (he : ∀ (p : α' × β'), e' p = e (f p.1, g p.2)) : (M.expand e).Iso (M.expand e')

A relabelling of the registers, as an isomorphism, along bijections f and g, from the extension in e to the extension in the relabelled vector e' (BipartiteModel.relabel).

Equations

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

@[simp]

theorem MIPRE.BipartiteModel.relabelIso_ΦA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_10} {β : Type u_11} {α' : Type u_12} {β' : Type u_13} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [Fintype α'] [DecidableEq α'] [Fintype β'] [DecidableEq β'] (e : α × β → ℂ) (e' : α' × β' → ℂ) (f : α' ≃ α) (g : β' ≃ β) (he : ∀ (p : α' × β'), e' p = e (f p.1, g p.2)) (a : Matrix α α 𝒜) : (M.relabelIso e e' f g he).ΦA a = a.submatrix ⇑f ⇑f

@[simp]

theorem MIPRE.BipartiteModel.relabelIso_ΦB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_10} {β : Type u_11} {α' : Type u_12} {β' : Type u_13} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [Fintype α'] [DecidableEq α'] [Fintype β'] [DecidableEq β'] (e : α × β → ℂ) (e' : α' × β' → ℂ) (f : α' ≃ α) (g : β' ≃ β) (he : ∀ (p : α' × β'), e' p = e (f p.1, g p.2)) (b : Matrix β β ℬ) : (M.relabelIso e e' f g he).ΦB b = b.submatrix ⇑g ⇑g

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

The unitary of an isomorphism, acting on each component of an ℓ² sum.

Equations

• Φ.expandCongrW e = (M.ampl e).trans ((LinearIsometryEquiv.piLpCongrRight 2 fun (x : α × β) => Φ.W).trans (M'.ampl e).symm)

theorem MIPRE.BipartiteModel.Iso.ampl_expandCongrW {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {α : Type u_10} {β : Type u_11} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (Φ : M.Iso M') (e : α × β → ℂ) (v : (M.expand e).H) (p : α × β) : ((M'.ampl e) ((Φ.expandCongrW e) v)).ofLp p = Φ.W (((M.ampl e) v).ofLp p)

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

An isomorphism extends to the extensions by the same registers in the same state: the unitary acts on each component, and each player's isomorphism entrywise.

Equations

• Φ.expandCongr e = { W := Φ.expandCongrW e, ΦA := MIPRE.mapMatrixStarAlgEquiv Φ.ΦA, ΦB := MIPRE.mapMatrixStarAlgEquiv Φ.ΦB, intertwineA := ⋯, intertwineB := ⋯, W_ψ := ⋯ }

@[simp]

theorem MIPRE.BipartiteModel.Iso.expandCongr_ΦA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {α : Type u_10} {β : Type u_11} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (Φ : M.Iso M') (e : α × β → ℂ) (X : Matrix α α 𝒜) : (Φ.expandCongr e).ΦA X = X.map ⇑Φ.ΦA

@[simp]

theorem MIPRE.BipartiteModel.Iso.expandCongr_ΦB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {α : Type u_10} {β : Type u_11} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (Φ : M.Iso M') (e : α × β → ℂ) (Y : Matrix β β ℬ) : (Φ.expandCongr e).ΦB Y = Y.map ⇑Φ.ΦB

Isomorphisms of tensor-product models

noncomputable def MIPRE.BipartiteModel.tensorExpandIso {dA : Type u_10} {dB : Type u_11} {α : Type u_14} {β : Type u_15} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (ξ : dA × dB → ℂ) (e : α × β → ℂ) : ((tensor ξ).expand e).Iso (tensor (expVec e ξ))

The extension of a tensor-product model is the tensor-product model of the expanded vector, as an isomorphism (BipartiteModel.tensorExpand, inverted by tensorUnexpand).

Equations

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

@[simp]

theorem MIPRE.BipartiteModel.tensorExpandIso_ΦA {dA : Type u_10} {dB : Type u_11} {α : Type u_14} {β : Type u_15} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (ξ : dA × dB → ℂ) (e : α × β → ℂ) (X : Matrix α α (Matrix dA dA ℂ)) : (tensorExpandIso ξ e).ΦA X = compHom X

@[simp]

theorem MIPRE.BipartiteModel.tensorExpandIso_ΦB {dA : Type u_10} {dB : Type u_11} {α : Type u_14} {β : Type u_15} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (ξ : dA × dB → ℂ) (e : α × β → ℂ) (Y : Matrix β β (Matrix dB dB ℂ)) : (tensorExpandIso ξ e).ΦB Y = compHom Y

noncomputable def MIPRE.BipartiteModel.tensorReindexW {dA : Type u_10} {dB : Type u_11} {dA' : Type u_12} {dB' : Type u_13} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype dA'] [DecidableEq dA'] [Fintype dB'] [DecidableEq dB'] (f : dA ≃ dA') (g : dB ≃ dB') (ψ : dA × dB → ℂ) : (tensor ψ).H ≃ₗᵢ[ℂ] (tensor (ψ ∘ Prod.map ⇑f.symm ⇑g.symm)).H

The unitary of ℂ^{dA × dB} onto ℂ^{dA' × dB'} relabelling the two factors.

Equations

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

theorem MIPRE.BipartiteModel.tensorReindexW_apply {dA : Type u_10} {dB : Type u_11} {dA' : Type u_12} {dB' : Type u_13} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype dA'] [DecidableEq dA'] [Fintype dB'] [DecidableEq dB'] (f : dA ≃ dA') (g : dB ≃ dB') (ψ : dA × dB → ℂ) (v : (tensor ψ).H) (q : dA' × dB') : ((tensorReindexW f g ψ) v).ofLp q = v.ofLp (f.symm q.1, g.symm q.2)

noncomputable def MIPRE.BipartiteModel.tensorReindexIso {dA : Type u_10} {dB : Type u_11} {dA' : Type u_12} {dB' : Type u_13} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype dA'] [DecidableEq dA'] [Fintype dB'] [DecidableEq dB'] (f : dA ≃ dA') (g : dB ≃ dB') (ψ : dA × dB → ℂ) : (tensor ψ).Iso (tensor (ψ ∘ Prod.map ⇑f.symm ⇑g.symm))

A tensor-product model is unchanged by relabelling its two factors: along bijections f : dA ≃ dA' and g : dB ≃ dB', the model of ψ is the model of ψ relabelled, each player's matrices relabelled along their factor.

Equations

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

@[simp]

theorem MIPRE.BipartiteModel.tensorReindexIso_ΦA {dA : Type u_10} {dB : Type u_11} {dA' : Type u_12} {dB' : Type u_13} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype dA'] [DecidableEq dA'] [Fintype dB'] [DecidableEq dB'] (f : dA ≃ dA') (g : dB ≃ dB') (ψ : dA × dB → ℂ) (X : Matrix dA dA ℂ) : (tensorReindexIso f g ψ).ΦA X = X.submatrix ⇑f.symm ⇑f.symm

@[simp]

theorem MIPRE.BipartiteModel.tensorReindexIso_ΦB {dA : Type u_10} {dB : Type u_11} {dA' : Type u_12} {dB' : Type u_13} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype dA'] [DecidableEq dA'] [Fintype dB'] [DecidableEq dB'] (f : dA ≃ dA') (g : dB ≃ dB') (ψ : dA × dB → ℂ) (Y : Matrix dB dB ℂ) : (tensorReindexIso f g ψ).ΦB Y = Y.submatrix ⇑g.symm ⇑g.symm