A one-sided ancilla, and the fixed-state dilation in a bipartite model

Introspection's adaptive inductions replace a measurement of the first player by a projective one acting on the old space and a fresh ancilla, prepared in one fixed state for every question (MIPRE.Introspection.extVecA in the matrix analysis). In a bipartite model (Phase 4 of planning/mipco-track.md):

• The one-sided extension BipartiteModel.expandA M t₀: the first player's register T, in the basis state t₀; the first player's algebra becomes the T × T matrices over 𝒜, the second player's is unchanged, acting as 1 ⊗ b. The state is M.ψ ⊗ e_{t₀} (OperatorMatrix.emb), so a quadratic form, a Born probability or a squared state norm on the extension is the one of the (t₀, t₀) entry, or of the t₀-th column (qform_expandA, bornProb_expandA, stateSqNorm_expandA).
• The inert embedding BipartiteModel.inertA M t₀, a local isometry M → M.expandA t₀ carrying the state to the state, with the first player's operator a becoming a ⊗ 1.
• Local isometries extend along registers (LocalIsometry.expand), so the inert embedding of the ancilla is one of the register models too.

The fixed-state dilation itself is MIPRE.exists_pvm_dilation (MIPRE/Foundations/KrausDilation.lean), in the first player's algebra.

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

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

Equations

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

@[simp]

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

noncomputable def MIPRE.BipartiteModel.expandA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_4} [Fintype T] [DecidableEq T] (M : BipartiteModel 𝒞 𝒜 ℬ) (t₀ : T) : BipartiteModel (Matrix T T 𝒞) (Matrix T T 𝒜) ℬ

The one-sided ancilla extension: a register T for the first player only, in the basis state t₀. The space is H ⊗ ℂ^T, the state ψ ⊗ e_{t₀}, the first player's operators the T × T matrices over 𝒜, and the second player's b acts as 1 ⊗ b.

Equations

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

theorem MIPRE.BipartiteModel.expandA_πA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_4} [Fintype T] [DecidableEq T] (M : BipartiteModel 𝒞 𝒜 ℬ) (t₀ : T) (X : Matrix T T 𝒜) : (M.expandA t₀).πA X = X.map ⇑M.πA

theorem MIPRE.BipartiteModel.expandA_πB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_4} [Fintype T] [DecidableEq T] (M : BipartiteModel 𝒞 𝒜 ℬ) (t₀ : T) (b : ℬ) : (M.expandA t₀).πB b = Matrix.diagonal fun (x : T) => M.πB b

theorem MIPRE.BipartiteModel.norm_expandA_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_4} [Fintype T] [DecidableEq T] (M : BipartiteModel 𝒞 𝒜 ℬ) (t₀ : T) : ‖(M.expandA t₀).ψ‖ = ‖M.ψ‖

The norm of the extended state is the norm of the state.

theorem MIPRE.BipartiteModel.toCLM_emb_apply {T : Type u_4} [Fintype T] [DecidableEq T] (t₀ : T) {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : Matrix T T (H →L[ℂ] H)) (ξ : H) (t : T) : ((OperatorMatrix.toCLM N) ((OperatorMatrix.emb t₀) ξ)).ofLp t = (N t t₀) ξ

An operator matrix on an embedded vector: its t₀-th column.

theorem MIPRE.BipartiteModel.qform_expandA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_4} [Fintype T] [DecidableEq T] (M : BipartiteModel 𝒞 𝒜 ℬ) (t₀ : T) (Z : Matrix T T 𝒞) : (M.expandA t₀).qform Z = M.qform (Z t₀ t₀)

The quadratic form of the extension is that of the (t₀, t₀) entry.

theorem MIPRE.BipartiteModel.snorm_sq_expandA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_4} [Fintype T] [DecidableEq T] (M : BipartiteModel 𝒞 𝒜 ℬ) (t₀ : T) (Z : Matrix T T 𝒞) : (M.expandA t₀).snorm Z ^ 2 = ∑ t : T, M.snorm (Z t t₀) ^ 2

The squared state norm of the extension is that of the t₀-th column.

theorem MIPRE.BipartiteModel.bornProb_expandA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_4} [Fintype T] [DecidableEq T] (M : BipartiteModel 𝒞 𝒜 ℬ) (t₀ : T) (X : Matrix T T 𝒜) (b : ℬ) : (M.expandA t₀).bornProb X b = M.bornProb (X t₀ t₀) b

A Born probability on the extension is that of the (t₀, t₀) entry.

theorem MIPRE.BipartiteModel.stateSqNorm_expandA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_4} [Fintype T] [DecidableEq T] (M : BipartiteModel 𝒞 𝒜 ℬ) (t₀ : T) (X : Matrix T T 𝒜) : (M.expandA t₀).stateSqNorm X = ∑ t : T, M.stateSqNorm (X t t₀)

The first player's squared state norm on the extension: that of the t₀-th column.

Components

noncomputable def MIPRE.BipartiteModel.amplA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_4} [Fintype T] [DecidableEq T] (M : BipartiteModel 𝒞 𝒜 ℬ) (t₀ : T) : (M.expandA t₀).H ≃ₗᵢ[ℂ] OperatorMatrix.Ampl T M.H

The Hilbert space of a one-sided extension is the ℓ² sum.

Equations

• M.amplA t₀ = LinearIsometryEquiv.refl ℂ (MIPRE.OperatorMatrix.Ampl T M.H)

theorem MIPRE.BipartiteModel.expandA_ext {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_4} [Fintype T] [DecidableEq T] (M : BipartiteModel 𝒞 𝒜 ℬ) (t₀ : T) {v w : (M.expandA t₀).H} (h : ∀ (t : T), ((M.amplA t₀) v).ofLp t = ((M.amplA t₀) w).ofLp t) : v = w

Two vectors of a one-sided extension are equal if their components are.

theorem MIPRE.BipartiteModel.expandA_π_πA_apply {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_4} [Fintype T] [DecidableEq T] (M : BipartiteModel 𝒞 𝒜 ℬ) (t₀ : T) (X : Matrix T T 𝒜) (v : (M.expandA t₀).H) (t : T) : ((M.amplA t₀) (((M.expandA t₀).π ((M.expandA t₀).πA X)) v)).ofLp t = ∑ s : T, (M.π (M.πA (X t s))) (((M.amplA t₀) v).ofLp s)

theorem MIPRE.BipartiteModel.expandA_π_πB_apply {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_4} [Fintype T] [DecidableEq T] (M : BipartiteModel 𝒞 𝒜 ℬ) (t₀ : T) (b : ℬ) (v : (M.expandA t₀).H) (t : T) : ((M.amplA t₀) (((M.expandA t₀).π ((M.expandA t₀).πB b)) v)).ofLp t = (M.π (M.πB b)) (((M.amplA t₀) v).ofLp t)

theorem MIPRE.BipartiteModel.expandA_ψ_apply {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_4} [Fintype T] [DecidableEq T] (M : BipartiteModel 𝒞 𝒜 ℬ) (t₀ t : T) : ((M.amplA t₀) (M.expandA t₀).ψ).ofLp t = if t = t₀ then M.ψ else 0

The inert embedding

noncomputable def MIPRE.BipartiteModel.inertA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_4} [Fintype T] [DecidableEq T] (M : BipartiteModel 𝒞 𝒜 ℬ) (t₀ : T) : M.LocalIsometry (M.expandA t₀)

The inert embedding of a model into its one-sided extension: the state goes to ψ ⊗ e_{t₀}, the first player's operator a to a ⊗ 1, the second player's are unchanged.

Equations

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

theorem MIPRE.BipartiteModel.inertA_W_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_4} [Fintype T] [DecidableEq T] (M : BipartiteModel 𝒞 𝒜 ℬ) (t₀ : T) : (M.inertA t₀).W M.ψ = (M.expandA t₀).ψ

@[simp]

theorem MIPRE.BipartiteModel.inertA_ΦA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_4} [Fintype T] [DecidableEq T] (M : BipartiteModel 𝒞 𝒜 ℬ) (t₀ : T) (a : 𝒜) : (M.inertA t₀).ΦA a = Matrix.diagonal fun (x : T) => a

@[simp]

theorem MIPRE.BipartiteModel.inertA_ΦB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_4} [Fintype T] [DecidableEq T] (M : BipartiteModel 𝒞 𝒜 ℬ) (t₀ : T) (b : ℬ) : (M.inertA t₀).ΦB b = b

Local isometries extend along registers

def MIPRE.BipartiteModel.mapMatrixHom {α : Type u_8} [Fintype α] {R : Type u_10} {S : Type u_11} [Ring R] [StarRing R] [Algebra ℂ R] [Ring S] [StarRing S] [Algebra ℂ S] (f : R →⋆ₙₐ[ℂ] S) : Matrix α α R →⋆ₙₐ[ℂ] Matrix α α S

The entrywise image of a matrix under a non-unital ⋆-homomorphism, as one.

Equations

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

@[simp]

theorem MIPRE.BipartiteModel.mapMatrixHom_apply {α : Type u_8} [Fintype α] {R : Type u_10} {S : Type u_11} [Ring R] [StarRing R] [Algebra ℂ R] [Ring S] [StarRing S] [Algebra ℂ S] (f : R →⋆ₙₐ[ℂ] S) (X : Matrix α α R) : (mapMatrixHom f) X = X.map ⇑f

def MIPRE.BipartiteModel.amplMap {ι : Type u_10} {H : Type u_11} {H' : Type u_12} [Fintype ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] (W : H →ₗᵢ[ℂ] H') : OperatorMatrix.Ampl ι H →ₗᵢ[ℂ] OperatorMatrix.Ampl ι H'

A linear isometry applied in each component of an ℓ² sum.

Equations

• MIPRE.BipartiteModel.amplMap W = { toFun := fun (v : MIPRE.OperatorMatrix.Ampl ι H) => WithLp.toLp 2 fun (i : ι) => W (v.ofLp i), map_add' := ⋯, map_smul' := ⋯, norm_map' := ⋯ }

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

The isometry of the extensions by the same register, componentwise.

Equations

• Φ.expandW e = (M'.ampl e).symm.toLinearIsometry.comp ((MIPRE.BipartiteModel.amplMap Φ.W).comp (M.ampl e).toLinearIsometry)

theorem MIPRE.BipartiteModel.LocalIsometry.ampl_expandW {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {𝒞' : Type u_5} {𝒜' : Type u_6} {ℬ' : Type u_7} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {α : Type u_8} {β : Type u_9} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (Φ : M.LocalIsometry M') (e : α × β → ℂ) (v : (M.expand e).H) (p : α × β) : ((M'.ampl e) ((Φ.expandW e) v)).ofLp p = Φ.W (((M.ampl e) v).ofLp p)

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

A local isometry extends along a register: the extensions of the two models by the same registers in the same state, with the players' block matrices mapped entrywise.

Equations

• Φ.expand e = { W := Φ.expandW e, ΦA := MIPRE.BipartiteModel.mapMatrixHom Φ.ΦA, ΦB := MIPRE.BipartiteModel.mapMatrixHom Φ.ΦB, intertwineA := ⋯, intertwineB := ⋯ }

@[simp]

theorem MIPRE.BipartiteModel.LocalIsometry.expand_ΦA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {𝒞' : Type u_5} {𝒜' : Type u_6} {ℬ' : Type u_7} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {α : Type u_8} {β : Type u_9} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (Φ : M.LocalIsometry M') (e : α × β → ℂ) (X : Matrix α α 𝒜) : (Φ.expand e).ΦA X = X.map ⇑Φ.ΦA

@[simp]

theorem MIPRE.BipartiteModel.LocalIsometry.expand_ΦB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {𝒞' : Type u_5} {𝒜' : Type u_6} {ℬ' : Type u_7} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {α : Type u_8} {β : Type u_9} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (Φ : M.LocalIsometry M') (e : α × β → ℂ) (Y : Matrix β β ℬ) : (Φ.expand e).ΦB Y = Y.map ⇑Φ.ΦB

theorem MIPRE.BipartiteModel.LocalIsometry.expand_W_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {𝒞' : Type u_5} {𝒜' : Type u_6} {ℬ' : Type u_7} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {α : Type u_8} {β : Type u_9} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] {Φ : M.LocalIsometry M'} (h : Φ.W M.ψ = M'.ψ) (e : α × β → ℂ) : (Φ.expand e).W (M.expand e).ψ = (M'.expand e).ψ

The extension carries the state to the state when the local isometry does.

Local isometries extend along a one-sided ancilla

noncomputable def MIPRE.BipartiteModel.LocalIsometry.expandAW {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_4} [Fintype T] [DecidableEq T] {M : BipartiteModel 𝒞 𝒜 ℬ} {𝒞' : Type u_5} {𝒜' : Type u_6} {ℬ' : Type u_7} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') (t₀ : T) : (M.expandA t₀).H →ₗᵢ[ℂ] (M'.expandA t₀).H

The isometry of the one-sided extensions, componentwise.

Equations

• Φ.expandAW t₀ = (M'.amplA t₀).symm.toLinearIsometry.comp ((MIPRE.BipartiteModel.amplMap Φ.W).comp (M.amplA t₀).toLinearIsometry)

theorem MIPRE.BipartiteModel.LocalIsometry.amplA_expandAW {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_4} [Fintype T] [DecidableEq T] {M : BipartiteModel 𝒞 𝒜 ℬ} {𝒞' : Type u_5} {𝒜' : Type u_6} {ℬ' : Type u_7} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') (t₀ : T) (v : (M.expandA t₀).H) (t : T) : ((M'.amplA t₀) ((Φ.expandAW t₀) v)).ofLp t = Φ.W (((M.amplA t₀) v).ofLp t)

noncomputable def MIPRE.BipartiteModel.LocalIsometry.expandA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_4} [Fintype T] [DecidableEq T] {M : BipartiteModel 𝒞 𝒜 ℬ} {𝒞' : Type u_5} {𝒜' : Type u_6} {ℬ' : Type u_7} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') (t₀ : T) : (M.expandA t₀).LocalIsometry (M'.expandA t₀)

A local isometry extends along a one-sided ancilla: the first player's block matrices are mapped entrywise, the second player's operators as before.

Equations

• Φ.expandA t₀ = { W := Φ.expandAW t₀, ΦA := MIPRE.BipartiteModel.mapMatrixHom Φ.ΦA, ΦB := Φ.ΦB, intertwineA := ⋯, intertwineB := ⋯ }

@[simp]

theorem MIPRE.BipartiteModel.LocalIsometry.expandA_ΦA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_4} [Fintype T] [DecidableEq T] {M : BipartiteModel 𝒞 𝒜 ℬ} {𝒞' : Type u_5} {𝒜' : Type u_6} {ℬ' : Type u_7} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') (t₀ : T) (X : Matrix T T 𝒜) : (Φ.expandA t₀).ΦA X = X.map ⇑Φ.ΦA

@[simp]

theorem MIPRE.BipartiteModel.LocalIsometry.expandA_ΦB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_4} [Fintype T] [DecidableEq T] {M : BipartiteModel 𝒞 𝒜 ℬ} {𝒞' : Type u_5} {𝒜' : Type u_6} {ℬ' : Type u_7} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') (t₀ : T) (b : ℬ) : (Φ.expandA t₀).ΦB b = Φ.ΦB b

theorem MIPRE.BipartiteModel.LocalIsometry.expandA_W_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_4} [Fintype T] [DecidableEq T] {M : BipartiteModel 𝒞 𝒜 ℬ} {𝒞' : Type u_5} {𝒜' : Type u_6} {ℬ' : Type u_7} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {Φ : M.LocalIsometry M'} (h : Φ.W M.ψ = M'.ψ) (t₀ : T) : (Φ.expandA t₀).W (M.expandA t₀).ψ = (M'.expandA t₀).ψ

The extension carries the state to the state when the local isometry does.

Exchanging an ancilla with a register

def MIPRE.BipartiteModel.layerSwap {T : Type u_4} [Fintype T] {α : Type u_5} [Fintype α] {R : Type u_7} [Ring R] [StarRing R] [Algebra ℂ R] : Matrix T T (Matrix α α R) →⋆ₙₐ[ℂ] Matrix α α (Matrix T T R)

The exchange of the two layers of a block matrix of block matrices, as a ⋆-homomorphism: X t t' a a' becomes the entry (a, a') (t, t').

Equations

• MIPRE.BipartiteModel.layerSwap = MIPRE.uncompHom.comp ((MIPRE.submatrixHom (Equiv.prodComm α T)).comp MIPRE.compHom)

@[simp]

theorem MIPRE.BipartiteModel.layerSwap_apply {T : Type u_4} [Fintype T] {α : Type u_5} [Fintype α] {R : Type u_7} [Ring R] [StarRing R] [Algebra ℂ R] (X : Matrix T T (Matrix α α R)) (a a' : α) (t t' : T) : layerSwap X a a' t t' = X t t' a a'

theorem MIPRE.BipartiteModel.layerSwap_one {T : Type u_4} [Fintype T] [DecidableEq T] {α : Type u_5} [Fintype α] [DecidableEq α] {R : Type u_7} [Ring R] [StarRing R] [Algebra ℂ R] : layerSwap 1 = 1

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

The isometry exchanging the ancilla and the register coordinates.

Equations

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

theorem MIPRE.BipartiteModel.ampl_exchangeIsometry {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_4} [Fintype T] [DecidableEq T] {M : BipartiteModel 𝒞 𝒜 ℬ} (t₀ : T) {α : Type u_5} {β : Type u_6} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) (v : ((M.expand e).expandA t₀).H) (p : α × β) (t : T) : ((M.amplA t₀) ((((M.expandA t₀).ampl e) ((exchangeIsometry t₀ e) v)).ofLp p)).ofLp t = ((M.ampl e) ((((M.expand e).amplA t₀) v).ofLp t)).ofLp p

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

The exchange of a one-sided ancilla with a register: the one-sided extension of an extension into the extension of the one-sided extension, the first player's block matrices of block matrices exchanged layer for layer (layerSwap), the second player's unchanged.

Equations

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

theorem MIPRE.BipartiteModel.exchange_W_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_4} [Fintype T] [DecidableEq T] {M : BipartiteModel 𝒞 𝒜 ℬ} (t₀ : T) {α : Type u_5} {β : Type u_6} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) : (exchange t₀ e).W ((M.expand e).expandA t₀).ψ = ((M.expandA t₀).expand e).ψ

@[simp]

theorem MIPRE.BipartiteModel.exchange_ΦA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_4} [Fintype T] [DecidableEq T] {M : BipartiteModel 𝒞 𝒜 ℬ} (t₀ : T) {α : Type u_5} {β : Type u_6} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) (X : Matrix T T (Matrix α α 𝒜)) : (exchange t₀ e).ΦA X = layerSwap X

@[simp]

theorem MIPRE.BipartiteModel.exchange_ΦB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_4} [Fintype T] [DecidableEq T] {M : BipartiteModel 𝒞 𝒜 ℬ} (t₀ : T) {α : Type u_5} {β : Type u_6} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) (Y : Matrix β β ℬ) : (exchange t₀ e).ΦB Y = Y