Matrices of scalars on a register, and the contraction against a vector

A finite register ι adjoined to a Hilbert space H is the ℓ² sum OperatorMatrix.Ampl ι H (H ⊗ ℂ^ι, the register the outer index). A matrix R of scalars on the register acts on it as R ⊗ 1_H: regAct R, a unital ⋆-algebra homomorphism from Matrix ι ι ℂ, so that sums, products and adjoints of register matrices are computed on the register alone. Two computations are all the analyses need of it.

• On a product vector e ⊗ ξ (WithLp.toLp 2 fun i => e i • ξ) it acts on the register's factor alone: regAct R (e ⊗ ξ) = (R e) ⊗ ξ (regAct_toLp_smul).
• The rank-one matrix |e⟩⟨f| contracts: it sends θ to e ⊗ (∑_j f_j θ_j) (regAct_vecMulVec). At the maximally entangled vector of a pair of registers this is the EPR contraction of the Pauli basis test's swap isometry: the range of |EPR⟩⟨EPR| ⊗ 1 is the set of products EPR ⊗ aux, and the contraction is the aux.

And one link with the ancilla extension of a bipartite model (MIPRE/Foundations/AncillaModel.lean): in M.expand e, whose space is Ampl (α × β) M.H, a matrix of scalars P on the first player's register times one Q on the second's acts as the register matrix P ⊗ Q (BipartiteModel.expand_π_smulKron_one_mul), whatever the model. So a quadratic form of such a product on any vector of the extension is a quadratic form of regAct.

noncomputable def MIPRE.OperatorMatrix.regActHom {ι : Type u_1} [Fintype ι] [DecidableEq ι] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : Matrix ι ι ℂ →⋆ₐ[ℂ] Ampl ι H →L[ℂ] Ampl ι H

The matrices of scalars acting on the register of ℂ^ι ⊗ H, R ↦ R ⊗ 1_H, as a unital ⋆-algebra homomorphism: the entrywise inclusion of the scalars, followed by the action of operator matrices.

Equations

• MIPRE.OperatorMatrix.regActHom = MIPRE.OperatorMatrix.toCLMStarAlgHom.comp (MIPRE.mapMatrixStarAlgHom (StarAlgHom.ofId ℂ (H →L[ℂ] H)))

noncomputable def MIPRE.OperatorMatrix.regAct {ι : Type u_1} [Fintype ι] [DecidableEq ι] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (R : Matrix ι ι ℂ) : Ampl ι H →L[ℂ] Ampl ι H

A matrix of scalars acting on the register of ℂ^ι ⊗ H: R ⊗ 1_H.

Equations

• MIPRE.OperatorMatrix.regAct R = MIPRE.OperatorMatrix.regActHom R

theorem MIPRE.OperatorMatrix.regActHom_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (R : Matrix ι ι ℂ) : regActHom R = regAct R

theorem MIPRE.OperatorMatrix.regAct_eq_toCLM {ι : Type u_1} [Fintype ι] [DecidableEq ι] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (R : Matrix ι ι ℂ) : regAct R = toCLM (R.map fun (r : ℂ) => r • 1)

regAct R is the operator matrix with the entries R i j • 1.

theorem MIPRE.OperatorMatrix.regAct_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (R S : Matrix ι ι ℂ) : regAct (R * S) = regAct R * regAct S

theorem MIPRE.OperatorMatrix.regAct_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : regAct 1 = 1

theorem MIPRE.OperatorMatrix.regAct_conjTranspose {ι : Type u_1} [Fintype ι] [DecidableEq ι] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (R : Matrix ι ι ℂ) : regAct R.conjTranspose = star (regAct R)

theorem MIPRE.OperatorMatrix.regAct_add {ι : Type u_1} [Fintype ι] [DecidableEq ι] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (R S : Matrix ι ι ℂ) : regAct (R + S) = regAct R + regAct S

theorem MIPRE.OperatorMatrix.regAct_smul {ι : Type u_1} [Fintype ι] [DecidableEq ι] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (c : ℂ) (R : Matrix ι ι ℂ) : regAct (c • R) = c • regAct R

theorem MIPRE.OperatorMatrix.regAct_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {κ : Type u_3} (s : Finset κ) (R : κ → Matrix ι ι ℂ) : regAct (∑ k ∈ s, R k) = ∑ k ∈ s, regAct (R k)

theorem MIPRE.OperatorMatrix.isStarProjection_regAct {ι : Type u_1} [Fintype ι] [DecidableEq ι] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P : Matrix ι ι ℂ} (hsa : P.conjTranspose = P) (hid : P * P = P) : IsStarProjection (regAct P)

The register action of a self-adjoint idempotent is an orthogonal projection.

theorem MIPRE.OperatorMatrix.regAct_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (R : Matrix ι ι ℂ) (θ : Ampl ι H) (i : ι) : ((regAct R) θ).ofLp i = ∑ j : ι, R i j • θ.ofLp j

The components of regAct R θ: (R θ)_i = ∑_j R_{ij} θ_j.

theorem MIPRE.OperatorMatrix.regAct_toLp_smul {ι : Type u_1} [Fintype ι] [DecidableEq ι] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (R : Matrix ι ι ℂ) (e : ι → ℂ) (ξ : H) : (regAct R) (WithLp.toLp 2 fun (i : ι) => e i • ξ) = WithLp.toLp 2 fun (i : ι) => R.mulVec e i • ξ

On a product vector a register matrix acts on the register's factor alone: (R ⊗ 1)(e ⊗ ξ) = (R e) ⊗ ξ.

theorem MIPRE.OperatorMatrix.regAct_vecMulVec {ι : Type u_1} [Fintype ι] [DecidableEq ι] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (e f : ι → ℂ) (θ : Ampl ι H) : (regAct (Matrix.vecMulVec e f)) θ = WithLp.toLp 2 fun (i : ι) => e i • ∑ j : ι, f j • θ.ofLp j

The contraction against a vector: the rank-one register matrix |e⟩⟨f| sends θ to the product vector e ⊗ ∑_j f_j θ_j.

theorem MIPRE.OperatorMatrix.norm_toLp_smul {ι : Type u_1} [Fintype ι] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (e : ι → ℂ) (ξ : H) : ‖WithLp.toLp 2 fun (i : ι) => e i • ξ‖ = ‖evec e‖ * ‖ξ‖

The norm of a product vector is the product of the norms.

theorem MIPRE.BipartiteModel.expand_π_πA_smulKron_one {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) (P : Matrix α α ℂ) : (M.expand e).π ((M.expand e).πA (smulKron 1 P)) = OperatorMatrix.regAct (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P 1)

A matrix of scalars on the first player's register of an extension acts as the register matrix P ⊗ 1.

theorem MIPRE.BipartiteModel.expand_π_πB_smulKron_one {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) (Q : Matrix β β ℂ) : (M.expand e).π ((M.expand e).πB (smulKron 1 Q)) = OperatorMatrix.regAct (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 Q)

A matrix of scalars on the second player's register of an extension acts as the register matrix 1 ⊗ Q.

theorem MIPRE.BipartiteModel.expand_π_smulKron_one_mul {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) (P : Matrix α α ℂ) (Q : Matrix β β ℂ) : (M.expand e).π ((M.expand e).πA (smulKron 1 P) * (M.expand e).πB (smulKron 1 Q)) = OperatorMatrix.regAct (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P Q)

A product of matrices of scalars on the two players' registers of an extension acts as the register matrix P ⊗ Q.