Representations of Solution Groups #
This module constructs matrix representations of an LCS solution group from observable matrices satisfying the analytic identities extracted by the EPR/local-loss pipeline.
The representation sends the solution-group generators to unitary matrices: $$ x_j \mapsto \operatorname{obs}_j,\qquad J \mapsto -I. $$ The main point is to prove that this assignment respects every relator in the solution-group presentation, so that it descends to a homomorphism $$ \operatorname{SolutionGroup}(\operatorname{game.toLinearSystem}) \to \operatorname{U}(n) . $$
The file is organized in three layers.
- Unitary packaging:
involutiveMatrixUnitary,observableMatrixUnitary, andnegOneMatrixUnitaryturn observables and $-I$ into unitary matrices, so they can be used as group-valued generator images. - Generic presented-group construction:
solutionGroupRepresentationpackages the observable generator image, same-equation commutation, and equation relators into a representation of the presented solution group. - Game and EPR construction:
rowObservableProduct_eq_sign_of_local_lossconverts local-loss annihilation on the EPR vector into the row identity $$ \prod_{j \in V_i}\operatorname{obs}_j = (-1)^{b_i}I, $$solutionGroupRepresentationOfRowsturns row identities into a game-specialized representation, andsolutionGroupRepresentationOfEPRLosssupplies those row identities from the EPR/local-loss argument.
Unitary Matrices #
The target group of a representation is unitary (Matrix n n ℂ), so observable
matrices must first be packaged as unitary elements. Since an observable is
self-adjoint and involutive, it is unitary. The distinguished solution-group
generator J is represented by the unitary matrix -I.
A self-adjoint involution as a unitary matrix.
Equations
- SolutionGroup.involutiveMatrixUnitary M hM hMstar = ⟨M, ⋯⟩
Instances For
An observable matrix as a unitary matrix.
Equations
Instances For
The scalar matrix -I as a unitary matrix.
Equations
Instances For
The underlying matrix of involutiveMatrixUnitary M hM hMstar is $M$:
$$ \operatorname{val}(\operatorname{involutiveMatrixUnitary}(M)) = M. $$
This simp lemma lets unit-valued generator images reduce back to their matrix
values during relator and row-product calculations.
The underlying matrix of observableMatrixUnitary M hM is $M$:
$$ \operatorname{val}(\operatorname{observableMatrixUnitary}(M)) = M. $$
This simp lemma keeps generator-image computations at the matrix level after an
observable has been packaged as a unitary matrix.
A packaged observable squares to the identity in the unitary group: $$ \operatorname{involutiveMatrixUnitary}(M)^2 = 1. $$ This discharges the $x_j^2 = 1$ and $J^2 = 1$ style relators after matrices are turned into units.
An observable matrix unitary squares to $1$: $$ \operatorname{observableMatrixUnitary}(M)^2 = 1. $$ This is the representation-side proof of the variable involution relators $x_j^2 = 1$.
The unit representing $J$ squares to $1$: $$ (-I)^2 = I. $$ This is the representation-side proof of the distinguished involution relator $J^2 = 1$.
Alice lift commutes with finite noncommutative products:
$$ \operatorname{AliceLift}\!\left(\prod_{x \in s} f_x\right) = \prod_{x \in s}\operatorname{AliceLift}(f_x). $$
The product is written with Finset.noncommProd, so pairwise commutation fixes
the order ambiguity. This is useful when the EPR/local-loss row product
Alice_Row_Prod must be identified with the Alice lift of the concrete row
observable product.
Generic presented-group construction #
This section is independent of a concrete LCSGame. It starts with a
LinearSystem S and a proposed image of the solution-group generators.
The public constructor in this section is solutionGroupRepresentation. It
handles the involution and centrality relators internally, so the caller only
needs to supply matrix commutation for variables in a common equation and the
equation-relator proofs themselves.
The intended image of the solution-group generators in unitary matrices.
This is the generator-level assignment that all later constructors try to
descend through the quotient defining SolutionGroup S:
var j ↦ obs j
J ↦ -I
Equations
- SolutionGroup.solutionGroupGeneratorImage obs obs_is_observable (SolutionGen.var j) = SolutionGroup.observableMatrixUnitary (obs j) ⋯
- SolutionGroup.solutionGroupGeneratorImage obs obs_is_observable SolutionGen.J = SolutionGroup.negOneMatrixUnitary
Instances For
Commuting matrices give commuting packaged unitary observables:
$$ MN = NM \Longrightarrow \widehat M\,\widehat N = \widehat N\,\widehat M. $$
This lifts same-equation commutation from matrices to units, which is the form
required by the relators in SolutionGroup S.
The distinguished image of $J$, namely $-I$, commutes with every matrix unit: $$ U(-I) = (-I)U. $$ This proves the centrality relators involving $J$ in the target unit group.
Construct a representation of SolutionGroup S from observable generator
images, same-equation commutation, and the equation-relator proofs.
Equations
- SolutionGroup.solutionGroupRepresentation obs obs_is_observable hsame hequation = PresentedGroup.toGroup ⋯
Instances For
Game-level and EPR-level constructors #
The previous section works for an arbitrary LinearSystem. This section
specializes it to game.toLinearSystem and supplies equation-relator proofs
from the local identities produced by the EPR/local-loss pipeline.
The key bridge is:
rowObservableProduct obs i = (-1) ^ (game.b i).val • I
↓ lift_equationRelator_of_rowIdentity
equationRelator game.toLinearSystem i maps to 1
The top-level constructor solutionGroupRepresentationOfEPRLoss obtains that
row identity from local_matrix_identities_of_local_loss_annihilate_epr.
The canonical ordered product over the support of row i.
The product is taken over the sorted support list. This fixes an order that
matches equationWord, which is useful when translating between free-group
words and matrix products.
Equations
Instances For
The local product of observables in equation i.
This is the matrix-side version of the equation word for row i, using the
same sorted support order as equationWord.
Equations
Instances For
Relate the sorted row observable product to the noncommProd used by
Alice_Row_Prod:
$$ \operatorname{rowObservableProduct}_i = \prod_{j \in V_i}^{\mathrm{noncomm}}\operatorname{obs}_j. $$
rowObservableProduct uses a sorted list to match equationWord, while
Alice_Row_Prod uses Finset.noncommProd over the attached row support. This
bridge is useful when importing the row identity extracted from the EPR/SOS
pipeline.
Turn a row matrix identity into the corresponding equation-relator proof: if $$ \operatorname{rowObservableProduct}_i = (-1)^{b_i}I, $$ then the equation relator maps to $1$: $$ \operatorname{lift}(\rho_0)(\operatorname{equationRelator}_i) = 1. $$ This is the main algebraic bridge from row equations to the relator hypothesis needed by the presented-group universal property.
Build the game-level representation from the row identities. This is the natural intermediate constructor between the generic presented-group layer and the EPR/local-loss extraction.
Equations
- SolutionGroup.solutionGroupRepresentationOfRows game obs obs_is_observable sameEquation_comm hrow = SolutionGroup.solutionGroupRepresentation obs obs_is_observable ⋯ ⋯
Instances For
Extract the row equation from the EPR/local-loss hypothesis: $$ \operatorname{rowObservableProduct}_i = (-1)^{b_i}I. $$ For each row $i$, the local loss for any support element contains the row SOS term. Since the row is assumed nonempty, one such support element is enough to recover the row identity. This isolates the analytic EPR/SOS step from the presented-group construction.
End-to-end representation constructor from the EPR/local-loss hypothesis: $$ \operatorname{SolutionGroup}(\operatorname{game.toLinearSystem}) \to \operatorname{U}(n), \qquad x_j \mapsto \operatorname{obs}_j,\quad J \mapsto -I. $$ This is the main constructor in the file. It extracts each row identity from local-loss annihilation on $\Omega$, turns the row identity into an equation relator proof, and then invokes the generic solution-group representation constructor.
Equations
- SolutionGroup.solutionGroupRepresentationOfEPRLoss game strat hNonempty hLoss = SolutionGroup.solutionGroupRepresentationOfRows game strat.obs ⋯ ⋯ ⋯