Embeddings of bipartite models

A local isometry (BipartiteModel.LocalIsometry) that carries the state to the state and keeps both players' units is an embedding of bipartite models (BipartiteModel.Embedding): the model form of "adjoin ancilla registers in fixed vectors", and of the reduced isometry of the soundness analysis of the Pauli basis test. New in Phase 5 of planning/mipco-track.md, where that analysis is stated in a bipartite model; there the matrix statements that a quantity is unchanged when registers in fixed vectors are adjoined, regrouped or read across the cut become transfers along an embedding.

• An embedding carries every quantity computed from the state and the players' operators: Born probabilities (Embedding.bornProb), the players' state norms (Embedding.stateSqNorm, Embedding.swap_stateSqNorm), cross norms (Embedding.xSqNorm), and, being unital, the value and the inconsistency of families of measurements pushed forward (Embedding.povmValue_pushforward, Embedding.inconsistency_pushforward). A sum of products of the two players' operators keeps its state norm and quadratic form along any local isometry carrying the state to the state (LocalIsometry.snorm_sum_mul_of_W_ψ, LocalIsometry.qform_sum_mul_of_W_ψ).
• Embeddings compose (Embedding.comp), exchange with the players (Embedding.swap), and every isomorphism is one (Iso.toEmbedding). The local isometries between extensions of MIPRE/Foundations/AncillaIsometry.lean are embeddings once their state conditions hold (inertEmb, assocEmb, relabelEmb, swapExpandEmb), and so is the change of cut of MIPRE/Foundations/ModelReading.lean (recutEmb).
• Two local isometries with no state condition: the same maps into the target with its state replaced (LocalIsometry.toWithState), and the conjugation of a model by a unitary of each player (LocalIsometry.ofUnitary), a local isometry because the two players' operators commute.
• Relabelling the outcomes of both families along one bijection keeps their inconsistency (BipartiteModel.inconsistency_map_equiv), and pushing a POVM forward along a composite is pushing it forward twice (POVMIn.pushforward_comp).

Pushing a POVM forward along a composite

theorem MIPRE.POVMIn.pushforward_comp {R : Type u_1} {S : Type u_2} {T : Type u_3} [Ring R] [StarRing R] [Algebra ℂ R] [PartialOrder R] [StarOrderedRing R] [Ring S] [StarRing S] [Algebra ℂ S] [PartialOrder S] [StarOrderedRing S] [Ring T] [StarRing T] [Algebra ℂ T] [PartialOrder T] [StarOrderedRing T] {X : Type u_4} [Fintype X] (g : S →⋆ₙₐ[ℂ] T) (hg : g 1 = 1) (f : R →⋆ₙₐ[ℂ] S) (hf : f 1 = 1) (P : POVMIn X R) : pushforward (g.comp f) ⋯ P = pushforward g hg (pushforward f hf P)

Pushing a POVM forward along a composite is pushing it forward twice.

Relabelling the outcomes of two families along one bijection

theorem MIPRE.BipartiteModel.inconsistency_map_equiv {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {Λ : Type u_10} {Λ' : Type u_11} {X : Type u_12} [Fintype Λ] [DecidableEq Λ] [Fintype Λ'] [DecidableEq Λ'] [Fintype X] (e : Λ ≃ Λ') (μ : X → ℝ) (P : X → POVMIn Λ 𝒜) (Q : X → POVMIn Λ ℬ) : (M.inconsistency μ (fun (x : X) => POVMIn.map (⇑e) (P x)) fun (x : X) => POVMIn.map (⇑e) (Q x)) = M.inconsistency μ P Q

Relabelling the outcomes of both families along one bijection keeps their inconsistency.

theorem MIPRE.BipartiteModel.star_πA_mul_πB_mul_self {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) {U : 𝒜} {V : ℬ} (hU : star U * U = 1) (hV : star V * V = 1) : star (N.πA U * N.πB V) * (N.πA U * N.πB V) = 1

The product of a unitary of each player is represented by an isometry: (U V)* (U V) = 1 needs only U* U = 1 and V* V = 1.

Three facts about local isometries

def MIPRE.BipartiteModel.LocalIsometry.toWithState {𝒞 : 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') (φ : M'.H) : M.LocalIsometry (M'.withState φ)

A local isometry into a model with its state replaced: the same isometry and homomorphisms, the target's state playing no part in a local isometry.

Equations

• Φ.toWithState φ = { W := Φ.W, ΦA := Φ.ΦA, ΦB := Φ.ΦB, intertwineA := ⋯, intertwineB := ⋯ }

@[simp]

theorem MIPRE.BipartiteModel.LocalIsometry.toWithState_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.LocalIsometry M') (φ : M'.H) (v : M.H) : (Φ.toWithState φ).W v = Φ.W v

@[simp]

theorem MIPRE.BipartiteModel.LocalIsometry.toWithState_Φ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.LocalIsometry M') (φ : M'.H) (a : 𝒜) : (Φ.toWithState φ).ΦA a = Φ.ΦA a

@[simp]

theorem MIPRE.BipartiteModel.LocalIsometry.toWithState_Φ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.LocalIsometry M') (φ : M'.H) (b : ℬ) : (Φ.toWithState φ).ΦB b = Φ.ΦB b

theorem MIPRE.BipartiteModel.LocalIsometry.intertwine_sum {𝒞 : 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') {κ : Type u_10} (s : Finset κ) (X : κ → 𝒜) (Y : κ → ℬ) (v : M.H) : (M'.π (∑ i ∈ s, M'.πA (Φ.ΦA (X i)) * M'.πB (Φ.ΦB (Y i)))) (Φ.W v) = Φ.W ((M.π (∑ i ∈ s, M.πA (X i) * M.πB (Y i))) v)

The isometry intertwines a sum of products of the two players' operators with the sum of the products of their images.

theorem MIPRE.BipartiteModel.LocalIsometry.snorm_sum_mul_of_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.LocalIsometry M') (h : Φ.W M.ψ = M'.ψ) {κ : Type u_10} (s : Finset κ) (X : κ → 𝒜) (Y : κ → ℬ) : M'.snorm (∑ i ∈ s, M'.πA (Φ.ΦA (X i)) * M'.πB (Φ.ΦB (Y i))) = M.snorm (∑ i ∈ s, M.πA (X i) * M.πB (Y i))

A sum of products of the two players' operators keeps its state norm along a local isometry carrying the state to the state.

theorem MIPRE.BipartiteModel.LocalIsometry.qform_sum_mul_of_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.LocalIsometry M') (h : Φ.W M.ψ = M'.ψ) {κ : Type u_10} (s : Finset κ) (X : κ → 𝒜) (Y : κ → ℬ) : M'.qform (∑ i ∈ s, M'.πA (Φ.ΦA (X i)) * M'.πB (Φ.ΦB (Y i))) = M.qform (∑ i ∈ s, M.πA (X i) * M.πB (Y i))

A sum of products of the two players' operators keeps its quadratic form along a local isometry carrying the state to the state.

Conjugation by a unitary of each player

def MIPRE.BipartiteModel.LocalIsometry.ofUnitary {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) (U : 𝒜) (V : ℬ) (hU : star U * U = 1) (hU' : U * star U = 1) (hV : star V * V = 1) (hV' : V * star V = 1) : N.LocalIsometry N

Conjugation by a unitary of each player: the isometry is the product πA U πB V of the two unitaries, and each player's operators are conjugated by the player's unitary, X ↦ U X U* and Y ↦ V Y V*. It is an isometry by U* U = 1 and V* V = 1, and it intertwines because the two players' operators commute; U U* = 1 and V V* = 1 make the two homomorphisms unital (ofUnitary_ΦA_one, ofUnitary_ΦB_one). The state is carried to the state only when πA U πB V fixes it, which is not asked.

Equations

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

@[simp]

theorem MIPRE.BipartiteModel.LocalIsometry.ofUnitary_W {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) (U : 𝒜) (V : ℬ) (hU : star U * U = 1) (hU' : U * star U = 1) (hV : star V * V = 1) (hV' : V * star V = 1) (v : N.H) : (ofUnitary N U V hU hU' hV hV').W v = (N.π (N.πA U * N.πB V)) v

@[simp]

theorem MIPRE.BipartiteModel.LocalIsometry.ofUnitary_ΦA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) (U : 𝒜) (V : ℬ) (hU : star U * U = 1) (hU' : U * star U = 1) (hV : star V * V = 1) (hV' : V * star V = 1) (X : 𝒜) : (ofUnitary N U V hU hU' hV hV').ΦA X = U * X * star U

@[simp]

theorem MIPRE.BipartiteModel.LocalIsometry.ofUnitary_ΦB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) (U : 𝒜) (V : ℬ) (hU : star U * U = 1) (hU' : U * star U = 1) (hV : star V * V = 1) (hV' : V * star V = 1) (Y : ℬ) : (ofUnitary N U V hU hU' hV hV').ΦB Y = V * Y * star V

theorem MIPRE.BipartiteModel.LocalIsometry.ofUnitary_ΦA_one {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) (U : 𝒜) (V : ℬ) (hU : star U * U = 1) (hU' : U * star U = 1) (hV : star V * V = 1) (hV' : V * star V = 1) : (ofUnitary N U V hU hU' hV hV').ΦA 1 = 1

The conjugation of the first player's operators is unital.

theorem MIPRE.BipartiteModel.LocalIsometry.ofUnitary_ΦB_one {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) (U : 𝒜) (V : ℬ) (hU : star U * U = 1) (hU' : U * star U = 1) (hV : star V * V = 1) (hV' : V * star V = 1) : (ofUnitary N U V hU hU' hV hV').ΦB 1 = 1

The conjugation of the second player's operators is unital.

Embeddings

structure MIPRE.BipartiteModel.Embedding {𝒞 : 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 𝒞' 𝒜' ℬ') extends M.LocalIsometry M' : Type (max (max (max (max (max u u') u_2) u_3) u_5) u_6)

An embedding of bipartite models: a local isometry carrying the state to the state and preserving both players' units. It is the model form of an extension by ancilla registers in fixed vectors, and of the reduced isometry of the soundness analysis of the Pauli basis test; everything a model computes from its state and its players' operators is carried along it unchanged.

• W : M.H →ₗᵢ[ℂ] M'.H
• ΦA : 𝒜 →⋆ₙₐ[ℂ] 𝒜'
• ΦB : ℬ →⋆ₙₐ[ℂ] ℬ'
• intertwineA (a : 𝒜) (v : M.H) : (M'.π (M'.πA (self.ΦA a))) (self.W v) = self.W ((M.π (M.πA a)) v)
• intertwineB (b : ℬ) (v : M.H) : (M'.π (M'.πB (self.ΦB b))) (self.W v) = self.W ((M.π (M.πB b)) v)
• W_ψ : self.W M.ψ = M'.ψ

  The isometry carries the state to the state.

• ΦA_one : self.ΦA 1 = 1

  The first player's unit goes to the unit.

• ΦB_one : self.ΦB 1 = 1

  The second player's unit goes to the unit.

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

The identity embedding.

Equations

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

def MIPRE.BipartiteModel.Embedding.comp {𝒞 : 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'.Embedding M'') (ι : M.Embedding M') : M.Embedding M''

Embeddings compose, the second argument applied first (as LocalIsometry.comp).

Equations

• ι'.comp ι = { toLocalIsometry := ι'.comp ι.toLocalIsometry, W_ψ := ⋯, ΦA_one := ⋯, ΦB_one := ⋯ }

def MIPRE.BipartiteModel.Embedding.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.Embedding M') : M.swap.Embedding M'.swap

The embedding with the players exchanged.

Equations

• ι.swap = { toLocalIsometry := ι.swap, W_ψ := ⋯, ΦA_one := ⋯, ΦB_one := ⋯ }

@[simp]

theorem MIPRE.BipartiteModel.Embedding.id_W {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (v : M.H) : (id M).W v = v

@[simp]

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

@[simp]

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

theorem MIPRE.BipartiteModel.Embedding.comp_toLocalIsometry {𝒞 : 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'.Embedding M'') (ι : M.Embedding M') : (ι'.comp ι).toLocalIsometry = ι'.comp ι.toLocalIsometry

@[simp]

theorem MIPRE.BipartiteModel.Embedding.comp_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'.Embedding M'') (ι : M.Embedding M') (v : M.H) : (ι'.comp ι).W v = ι'.W (ι.W v)

@[simp]

theorem MIPRE.BipartiteModel.Embedding.comp_Φ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'.Embedding M'') (ι : M.Embedding M') (a : 𝒜) : (ι'.comp ι).ΦA a = ι'.ΦA (ι.ΦA a)

@[simp]

theorem MIPRE.BipartiteModel.Embedding.comp_Φ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'.Embedding M'') (ι : M.Embedding M') (b : ℬ) : (ι'.comp ι).ΦB b = ι'.ΦB (ι.ΦB b)

theorem MIPRE.BipartiteModel.Embedding.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.Embedding M') : ι.swap.toLocalIsometry = ι.swap

@[simp]

theorem MIPRE.BipartiteModel.Embedding.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.Embedding M') : ι.swap.W = ι.W

@[simp]

theorem MIPRE.BipartiteModel.Embedding.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.Embedding M') : ι.swap.ΦA = ι.ΦB

@[simp]

theorem MIPRE.BipartiteModel.Embedding.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.Embedding M') : ι.swap.ΦB = ι.ΦA

@[simp]

theorem MIPRE.BipartiteModel.Embedding.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.Embedding M') : ι.swap.swap = ι

What an embedding carries over

theorem MIPRE.BipartiteModel.Embedding.bornProb {𝒞 : 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.Embedding M') (a : 𝒜) (b : ℬ) : M'.bornProb (ι.ΦA a) (ι.ΦB b) = M.bornProb a b

Born probabilities are carried over.

theorem MIPRE.BipartiteModel.Embedding.stateSqNorm {𝒞 : 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.Embedding M') (a : 𝒜) : M'.stateSqNorm (ι.ΦA a) = M.stateSqNorm a

The first player's state norms are carried over.

theorem MIPRE.BipartiteModel.Embedding.swap_stateSqNorm {𝒞 : 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.Embedding M') (b : ℬ) : M'.swap.stateSqNorm (ι.ΦB b) = M.swap.stateSqNorm b

The second player's state norms are carried over.

theorem MIPRE.BipartiteModel.Embedding.xSqNorm {𝒞 : 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.Embedding M') (a : 𝒜) (b : ℬ) : M'.xSqNorm (ι.ΦA a) (ι.ΦB b) = M.xSqNorm a b

The cross norms are carried over.

theorem MIPRE.BipartiteModel.Embedding.norm_ψ {𝒞 : 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.Embedding M') : ‖M'.ψ‖ = ‖M.ψ‖

The state has the norm of the state.

theorem MIPRE.BipartiteModel.Embedding.inconsistency_pushforward {𝒞 : 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 ℬ] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] [PartialOrder ℬ'] [StarOrderedRing ℬ'] (ι : M.Embedding M') {Λ : Type u_10} {X : Type u_11} [Fintype Λ] [DecidableEq Λ] [Fintype X] (μ : X → ℝ) (P : X → POVMIn Λ 𝒜) (Q : X → POVMIn Λ ℬ) : (M'.inconsistency μ (fun (x : X) => POVMIn.pushforward ι.ΦA ⋯ (P x)) fun (x : X) => POVMIn.pushforward ι.ΦB ⋯ (Q x)) = M.inconsistency μ P Q

Two families of measurements pushed forward along an embedding have their inconsistency.

theorem MIPRE.BipartiteModel.Embedding.povmValue_pushforward {𝒞 : 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 ℬ] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] [PartialOrder ℬ'] [StarOrderedRing ℬ'] (ι : M.Embedding 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 ℬ) : (M'.povmValue G (fun (x : X) => POVMIn.pushforward ι.ΦA ⋯ (PA x)) fun (y : Y) => POVMIn.pushforward ι.ΦB ⋯ (PB y)) = M.povmValue G PA PB

A family of measurements pushed forward along an embedding has its value.

def MIPRE.BipartiteModel.Iso.toEmbedding {𝒞 : 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.Embedding M'

Every isomorphism of models is an embedding.

Equations

• Φ.toEmbedding = { toLocalIsometry := Φ.toLocalIsometry, W_ψ := ⋯, ΦA_one := ⋯, ΦB_one := ⋯ }

theorem MIPRE.BipartiteModel.Iso.toEmbedding_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') : Φ.toEmbedding.toLocalIsometry = Φ.toLocalIsometry

@[simp]

theorem MIPRE.BipartiteModel.Iso.toEmbedding_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) : Φ.toEmbedding.W v = Φ.W v

@[simp]

theorem MIPRE.BipartiteModel.Iso.toEmbedding_Φ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 : 𝒜) : Φ.toEmbedding.ΦA a = Φ.ΦA a

@[simp]

theorem MIPRE.BipartiteModel.Iso.toEmbedding_Φ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 : ℬ) : Φ.toEmbedding.ΦB b = Φ.ΦB b

The embeddings between extensions

noncomputable def MIPRE.BipartiteModel.inertEmb {𝒞 : 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 : α × β → ℂ) (he : ‖evec e‖ = 1) : M.Embedding (M.expand e)

An inert ancilla in a unit vector, as an embedding (BipartiteModel.inert).

Equations

• M.inertEmb e he = { toLocalIsometry := M.inert e he, W_ψ := ⋯, ΦA_one := ⋯, ΦB_one := ⋯ }

theorem MIPRE.BipartiteModel.inertEmb_toLocalIsometry {𝒞 : 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 : α × β → ℂ) (he : ‖evec e‖ = 1) : (M.inertEmb e he).toLocalIsometry = M.inert e he

@[simp]

theorem MIPRE.BipartiteModel.inertEmb_Φ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 : α × β → ℂ) (he : ‖evec e‖ = 1) (a : 𝒜) : (M.inertEmb e he).ΦA a = Matrix.diagonal fun (x : α) => a

@[simp]

theorem MIPRE.BipartiteModel.inertEmb_Φ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 : α × β → ℂ) (he : ‖evec e‖ = 1) (b : ℬ) : (M.inertEmb e he).ΦB b = Matrix.diagonal fun (x : β) => b

noncomputable def MIPRE.BipartiteModel.assocEmb {𝒞 : 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').Embedding (M.expand e'')

Associativity of extensions, as an embedding (BipartiteModel.assoc), in a vector e'' that is the product of the two.

Equations

• M.assocEmb e e' e'' he = { toLocalIsometry := M.assoc e e' e'', W_ψ := ⋯, ΦA_one := ⋯, ΦB_one := ⋯ }

theorem MIPRE.BipartiteModel.assocEmb_toLocalIsometry {𝒞 : 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.assocEmb e e' e'' he).toLocalIsometry = M.assoc e e' e''

@[simp]

theorem MIPRE.BipartiteModel.assocEmb_Φ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.assocEmb e e' e'' he).ΦA a = compHom a

@[simp]

theorem MIPRE.BipartiteModel.assocEmb_Φ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.assocEmb e e' e'' he).ΦB b = compHom b

noncomputable def MIPRE.BipartiteModel.relabelEmb {𝒞 : 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).Embedding (M.expand e')

A relabelling of the registers, as an embedding (BipartiteModel.relabel), to the relabelled vector.

Equations

• M.relabelEmb e e' f g he = { toLocalIsometry := M.relabel e e' f g, W_ψ := ⋯, ΦA_one := ⋯, ΦB_one := ⋯ }

theorem MIPRE.BipartiteModel.relabelEmb_toLocalIsometry {𝒞 : 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.relabelEmb e e' f g he).toLocalIsometry = M.relabel e e' f g

@[simp]

theorem MIPRE.BipartiteModel.relabelEmb_Φ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.relabelEmb e e' f g he).ΦA a = a.submatrix ⇑f ⇑f

@[simp]

theorem MIPRE.BipartiteModel.relabelEmb_Φ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.relabelEmb e e' f g he).ΦB b = b.submatrix ⇑g ⇑g

noncomputable def MIPRE.BipartiteModel.swapExpandEmb {𝒞 : 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 : α × β → ℂ) (e' : β × α → ℂ) (he : ∀ (p : β × α), e' p = e p.swap) : (M.expand e).swap.Embedding (M.swap.expand e')

The exchange of the players in an extension, as an embedding (BipartiteModel.swapExpand), to the exchanged vector.

Equations

• M.swapExpandEmb e e' he = { toLocalIsometry := M.swapExpand e e', W_ψ := ⋯, ΦA_one := ⋯, ΦB_one := ⋯ }

theorem MIPRE.BipartiteModel.swapExpandEmb_toLocalIsometry {𝒞 : 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 : α × β → ℂ) (e' : β × α → ℂ) (he : ∀ (p : β × α), e' p = e p.swap) : (M.swapExpandEmb e e' he).toLocalIsometry = M.swapExpand e e'

@[simp]

theorem MIPRE.BipartiteModel.swapExpandEmb_Φ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 : α × β → ℂ) (e' : β × α → ℂ) (he : ∀ (p : β × α), e' p = e p.swap) (b : Matrix β β ℬ) : (M.swapExpandEmb e e' he).ΦA b = b

@[simp]

theorem MIPRE.BipartiteModel.swapExpandEmb_Φ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 : α × β → ℂ) (e' : β × α → ℂ) (he : ∀ (p : β × α), e' p = e p.swap) (a : Matrix α α 𝒜) : (M.swapExpandEmb e e' he).ΦB a = a

noncomputable def MIPRE.BipartiteModel.recutEmb {𝒞 : 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 : α × β → ℂ) (σ : α × β ≃ α' × β') : (M.expand (e ∘ ⇑σ.symm)).Embedding (M.recut e σ)

The change of cut, as an embedding (BipartiteModel.recutIsom): the extension along the regrouped registers into the reading of the original extension.

Equations

• M.recutEmb e σ = { toLocalIsometry := M.recutIsom e σ, W_ψ := ⋯, ΦA_one := ⋯, ΦB_one := ⋯ }

theorem MIPRE.BipartiteModel.recutEmb_toLocalIsometry {𝒞 : 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 : α × β → ℂ) (σ : α × β ≃ α' × β') : (M.recutEmb e σ).toLocalIsometry = M.recutIsom e σ

@[simp]

theorem MIPRE.BipartiteModel.recutEmb_Φ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 : α × β → ℂ) (σ : α × β ≃ α' × β') (X : Matrix α' α' 𝒜) : (M.recutEmb e σ).ΦA X = X

@[simp]

theorem MIPRE.BipartiteModel.recutEmb_Φ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 : α × β → ℂ) (σ : α × β ≃ α' × β') (Y : Matrix β' β' ℬ) : (M.recutEmb e σ).ΦB Y = Y