The commutant of a matrix amplification #
The low-individual-degree hypothesis of Phase 5 of planning/mipco-track.md,
LIDT.Simul.SoundCo, is soundness in the model S.toModel of every commuting-operator strategy
S; the Pauli basis analysis needs it in the ancilla extensions S.toModel.expand e
(MIPRE/Foundations/AncillaModel.lean). This file shows that an extension by a unit vector of a
commuting-operator model is a commuting-operator model, up to isomorphism
(BipartiteModel.Iso, MIPRE/Foundations/ModelIso.lean), so that the hypothesis applies to it as
it stands (LIDT.Simul.SoundCo.expand, on the Background side).
The strategy is S.expandStrategy e he, on the space H ⊗ ℂ^{α × β} of the extension and in its
state. Only the second player's operators determine the model's algebras, and they are chosen so
that their commutant is exactly the first player's algebra of the extension: the operators
1_α ⊗ 1_β ⊗ F^y_b of S, the projections 1_α ⊗ |b⟩⟨b| ⊗ 1 onto the basis vectors of the
register β, and the projection 1_α ⊗ |u⟩⟨u| ⊗ 1 onto its uniform superposition u, each
measured as a two-outcome measurement. The first player asks one question and always gives the
same answer.
An operator T on H ⊗ ℂ^ι is the operator of the matrix of its compressions,
T = toCLM (entries T) (OperatorMatrix.toCLM_entries), so commuting with an operator matrix is
matrix algebra (OperatorMatrix.commute_toCLM_iff). Then:
- the commutant of the second register's matrix units is the first register's matrices
(
eq_liftLeft_of_commute), and symmetrically (eq_liftRight_of_commute): an(α × β)-matrix commuting with1_α ⊗ E_{bb'}for allb, b'isX ⊗ 1_β. The matrix units are in the algebra generated by the projections the second player measures, sinceE_{bb'} = |β| E_{bb} |u⟩⟨u| E_{b'b'}(commute_liftRight_single_of_commute); - commuting with an amplified operator
f ⊗ 1is commuting entrywise withf(commute_diagonal_const_iff). Together, an operator commuting withf ⊗ 1forf ∈ sand with the register's matrix units isX ⊗ 1with the entries ofXin the commutant ofs(OperatorMatrix.exists_eq_toCLM_liftLeft, andOperatorMatrix.exists_eq_toCLM_liftRightfor the other register).
So the first player's algebra of the strategy is the image of M_α(𝒜), for 𝒜 = S.aliceAlg
(CommutingOperatorStrategy.expandAliceEquiv). That image contains M_α(ℂ) ⊗ 1 and 𝒜 ⊗ 1, so
the same two facts, for the first register, make its commutant the image of M_β(𝒜'), and
𝒜' = S.bobAlg by definition (CommutingOperatorStrategy.expandBobEquiv). Both equivalences are
the representations of the extension, so the identity of the space is an isomorphism of bipartite
models S.toModel.expand e ≅ (S.expandStrategy e he).toModel
(CommutingOperatorStrategy.expandIso).
expandStrategy is not reducible, so that the instances stated for every commuting-operator
strategy, the order of its algebras among them, are found for it; the proofs read it through its
reducible twin expandStrategyAux, whose space is seen to be H ⊗ ℂ^{α × β} with that space's
own instances.
The entries of an operator on an amplification #
The entries of an operator on the amplification: the entry (i, j) is the compression
ξ ↦ (T (ξ ⊗ e_j))_i of T from the j-th copy of H to the i-th.
Equations
- MIPRE.OperatorMatrix.entries T = Matrix.of fun (i j : ι) => PiLp.proj 2 (fun (x : ι) => H) i ∘SL T ∘SL MIPRE.OperatorMatrix.emb j
Instances For
A vector of the amplification is the sum of its coordinates, embedded.
An operator is the operator of its entries.
The entries of the operator of a matrix are the matrix.
An operator commutes with the operator of a matrix exactly when its entries do.
Matrices commuting with a register #
A matrix commutes with a constant diagonal matrix exactly when its entries commute with the constant.
A constant diagonal matrix of the first register acts on the pair as the constant diagonal.
A constant diagonal matrix of the second register acts on the pair as the constant diagonal.
The two registers' matrices commute when their entries do.
The commutant of the second register's matrix units is the first register's matrices: a
matrix commuting with every 1_α ⊗ E_{bb'} is X ⊗ 1_β, with X its block at any b₀.
The commutant of the first register's matrix units is the second register's matrices: a
matrix commuting with every E_{aa'} ⊗ 1_β is 1_α ⊗ Y, with Y its block at any a₀.
The projections of a register that generate its matrices #
The projection |u⟩⟨u| onto the uniform superposition u = |β|^{-1/2} ∑_b |b⟩ of a
register: every entry is 1 / |β|.
Equations
- MIPRE.uniformProj β = Matrix.of fun (x x_1 : β) => (↑(Fintype.card β))⁻¹
Instances For
A matrix unit from the diagonal projections and the uniform one:
E_{bb'} = |β| E_{bb} |u⟩⟨u| E_{b'b'}.
Commuting with the diagonal and the uniform projections of the second register is commuting with its matrix units.
The commutant of an amplification, as operators #
The two registers' operators commute when their entries do.
An operator commuting with the second register and with an amplified set is a matrix of the
first register over the commutant of the set: if T on H ⊗ ℂ^{α × β} commutes with f ⊗ 1
for every f ∈ s and with 1 ⊗ 1_α ⊗ E_{bb'} for all b, b', then T = X ⊗ 1_β with every
entry of X commuting with s.
An operator commuting with the first register and with an amplified set is a matrix of the
second register over the commutant of the set: the mirror of exists_eq_toCLM_liftLeft.
The first register's matrices act injectively, when the second register is not empty.
The second register's matrices act injectively, when the first register is not empty.
The strategy of an ancilla extension #
The projections of the register β that the second player of an extension measures: none
the projection onto the uniform superposition, some b the projection onto the basis vector
b.
Equations
Instances For
The second player's operators of the ancilla strategy, as matrices over B(H) on the
register β (the first register acting trivially): to a question y of S, the amplified
S.F y b; to a question g about the register, the two-outcome measurement of
expandRegProj g.
Equations
- S.expandBobMat (Sum.inl y) (Sum.inl b) = (Matrix.scalar β) (S.F y b)
- S.expandBobMat (Sum.inr g) (Sum.inr t) = (MIPRE.mapMatrixStarAlgHom (StarAlgHom.ofId ℂ (S.H →L[ℂ] S.H))) (MIPRE.twoOutcome (MIPRE.CommutingOperatorStrategy.expandRegProj g) t)
- S.expandBobMat (Sum.inl val) (Sum.inr val_1) = 0
- S.expandBobMat (Sum.inr val) (Sum.inl val_1) = 0
Instances For
The entries of the second player's operators commute with the first player's algebra.
expandStrategy, reducibly: the proofs below read its space as H ⊗ ℂ^{α × β} with that
space's own instances, which is what lets its operators be compared with operator matrices.
expandStrategy itself is not reducible, so that instances stated for every commuting-operator
strategy (the order of its algebras, for example) are found for it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The commuting-operator strategy of an ancilla extension of S by registers α, β in
the unit state e: the space H ⊗ ℂ^{α × β} and the state ψ ⊗ e of S.toModel.expand e; the
first player asks one question and always gives the same answer, with the operator 1; the second
player answers a question y of S with the operators 1_α ⊗ 1_β ⊗ F^y_b, and a question
g : Option β about the register with the two-outcome measurement of expandRegProj g.
Equations
- S.expandStrategy e he = S.expandStrategyAux e he
Instances For
The first player's matrices of an extension, as operators on H ⊗ ℂ^{α × β}: X ⊗ 1_β.
Equations
Instances For
The second player's matrices of an extension, as operators on H ⊗ ℂ^{α × β}: 1_α ⊗ Y.
Equations
Instances For
expandAliceRep is the first player's representation of the extension.
expandBobRep is the second player's representation of the extension.
The first player's operators of the extension are in the first player's algebra of the strategy: they commute with the second player's operators.
The first player's algebra of the strategy is the first player's algebra of the
extension: every operator commuting with the second player's operators is X ⊗ 1_β for a matrix
X over the commutant of S's second player.
The first player's representation of the extension, into the first player's algebra of the strategy. (The representation is first read on the strategy's space, where the algebra lives, so that the restriction of its codomain is between subalgebras of one type.)
Equations
- S.expandAliceHom e he = S.expandAliceRep.codRestrict (S.expandStrategy e he).aliceAlg ⋯
Instances For
The first player's algebra of the strategy is the matrix algebra M_α(𝒜) over the first
player's algebra 𝒜 of S, by the representation of the extension.
Equations
- S.expandAliceEquiv e he = StarAlgEquiv.ofBijective (S.expandAliceHom e he) ⋯
Instances For
The second player's operators of the extension are in the second player's algebra of the strategy: they commute with its first player's algebra, which is the first player's algebra of the extension.
The second player's algebra of the strategy is the second player's algebra of the
extension: every operator commuting with the first player's algebra of the strategy is 1_α ⊗ Y
for a matrix Y over the commutant of S.aliceAlg, which is S.bobAlg.
The second player's representation of the extension, into the second player's algebra of the strategy.
Equations
- S.expandBobHom e he = S.expandBobRep.codRestrict (S.expandStrategy e he).bobAlg ⋯
Instances For
The second player's algebra of the strategy is the matrix algebra M_β(ℬ) over the second
player's algebra ℬ of S, by the representation of the extension.
Equations
- S.expandBobEquiv e he = StarAlgEquiv.ofBijective (S.expandBobHom e he) ⋯
Instances For
The first player's algebra of the strategy, as a set: the operators X ⊗ 1_β for the
matrices X over S.aliceAlg.
The second player's algebra of the strategy, as a set: the operators 1_α ⊗ Y for the
matrices Y over S.bobAlg.
The extension of a commuting-operator model is a commuting-operator model #
The ancilla extension of a commuting-operator model is the model of a commuting-operator
strategy, S.toModel.expand e ≅ (S.expandStrategy e he).toModel: the identity of the space
H ⊗ ℂ^{α × β}, which carries the state to itself, with the equivalences expandAliceEquiv and
expandBobEquiv of the players' algebras.
Equations
- One or more equations did not get rendered due to their size.