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 units: $$ 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{Matrix}_n(\mathbb C))^\times . $$
The file is organized in three layers.
- Matrix-unit packaging:
involutiveMatrixUnit,observableMatrixUnit, andnegOneMatrixUnitturn involutive matrices into units, so observable matrices and $-I$ can be used as group-valued generator images. - Generic presented-group construction:
solutionGroupRepresentationOfRelatorProofapplies the universal property of the presented group, whilesolutionGroupRelatorProofOfEquationProofandsolutionGroupRepresentationOfEquationProofreduce the all-relators proof to same-equation commutation and the equation relators. - 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, $$ andsolutionGroupRepresentationOfEPRLossuses these row identities to build the final solution-group representation.
Matrix units #
The target group of a representation is (Matrix n n ℂ)ˣ, so observable
matrices must first be packaged as units. Since an observable is involutive,
its inverse is itself. The distinguished solution-group generator J is
represented by the unit -I.
A square matrix whose square is 1 as a unit.
Equations
- SolutionGroup.involutiveMatrixUnit M hM = { val := M, inv := M, val_inv := hM, inv_val := hM }
Instances For
An observable matrix as a unit, using its involutivity.
Equations
Instances For
The scalar matrix -I as a unit.
Equations
Instances For
The underlying matrix of involutiveMatrixUnit M hM is $M$:
$$ \operatorname{val}(\operatorname{involutiveMatrixUnit}(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 observableMatrixUnit M hM is $M$:
$$ \operatorname{val}(\operatorname{observableMatrixUnit}(M)) = M. $$
This simp lemma keeps generator-image computations at the matrix level after an
observable has been packaged as a unit.
The underlying matrix of the distinguished unit for $J$ is $-I$: $$ \operatorname{val}(\operatorname{negOneMatrixUnit}) = -I. $$ This is used whenever a group-level expression involving $J$ is compared with a matrix row identity.
An involutive matrix unit squares to the identity unit: $$ \operatorname{involutiveMatrixUnit}(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 unit squares to $1$: $$ \operatorname{observableMatrixUnit}(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.
There are three levels:
solutionGroupRepresentationOfRelatorProofis the raw universal-property constructor: if every relator maps to1, the generator map descends to a homomorphism out ofSolutionGroup S.solutionGroupRelatorProofOfEquationProofproves the all-relators hypothesis from structured assumptions: generator involutions, centrality ofJ, same-equation commutation, and the equation relators.solutionGroupRepresentationOfEquationProofpackages those two steps. It automatically handles theJ-commutation and unit-lifting details, leaving only matrix commutation and equation-relator proofs to the caller.
The intended image of the solution-group generators in matrix units.
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.observableMatrixUnit (obs j) ⋯
- SolutionGroup.solutionGroupGeneratorImage obs obs_is_observable SolutionGen.J = SolutionGroup.negOneMatrixUnit
Instances For
On a variable generator, the intended generator image is the corresponding
observable unit:
$$ \rho_0(x_j) = \operatorname{obs}_j. $$
This rewrite lemma is used to simplify the final representation on
SolutionGroup.var.
On the distinguished generator, the intended generator image is $-I$:
$$ \rho_0(J) = -I. $$
This rewrite lemma is used to simplify the final representation on
SolutionGroup.J and in equation-relator calculations.
The raw universal-property constructor for solution-group representations.
The input hrel says that every defining relator of SolutionGroup S maps to
1 under the free-group lift of solutionGroupGeneratorImage. With that
proof in hand, PresentedGroup.toGroup descends the generator assignment to a
group homomorphism
SolutionGroup S →* (Matrix n n ℂ)ˣ
This definition does not prove any relators itself; it only consumes the full relator proof.
Equations
- SolutionGroup.solutionGroupRepresentationOfRelatorProof obs obs_is_observable hrel = PresentedGroup.toGroup hrel
Instances For
Build the full relator proof from the natural structured assumptions:
$$ r \in R_S \Longrightarrow \operatorname{lift}(\rho_0)(r) = 1. $$
The solution-group presentation has five families of relators: $x_j^2 = 1$,
$J^2 = 1$, $x_jJ = Jx_j$, same-equation commutation $x_jx_k = x_kx_j$, and
the equation relators. This lemma proves the first two from observability and
$J \mapsto -I$, consumes hJcomm and hsame for the commutation relators, and
uses hequation for the row equations. It is the structured all-relators proof
needed before applying the presented-group universal property.
Commuting matrices give commuting observable matrix units:
$$ 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 once the equation relators are known.
This is the main generic constructor used by later sections. It packages the two lower-level steps:
hsame + hequation
↓ solutionGroupRelatorProofOfEquationProof
all relators map to 1
↓ solutionGroupRepresentationOfRelatorProof
SolutionGroup S →* (Matrix n n ℂ)ˣ
The call to solutionGroupRelatorProofOfEquationProof also inserts two routine
facts: -I commutes with every matrix unit, and matrix-level commutation of
observables lifts to commutation of the corresponding units.
Equations
- SolutionGroup.solutionGroupRepresentationOfEquationProof obs obs_is_observable hsame hequation = SolutionGroup.solutionGroupRepresentationOfRelatorProof obs obs_is_observable ⋯
Instances For
The representation built from a relator proof sends var j to the observable unit:
$$ \rho(x_j) = \operatorname{obs}_j. $$
This is the public simp rule that records that the presented-group quotient did
not change the intended generator image.
The representation built from a relator proof sends $J$ to $-I$: $$ \rho(J) = -I. $$ This is the companion generator-evaluation rule for the distinguished central involution.
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_toLinearSystem_of_row
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 product to Finset.noncommProd:
$$ \prod_{j \in V_i}^{\mathrm{sorted}} f_j = \prod_{j \in V_i}^{\mathrm{noncomm}} f_j. $$
This is the monoid-level support-product lemma. The sorted list fixes the same
canonical order used by equationWord, while noncommProd is convenient for
strategy row products. Pairwise commutation makes the two presentations agree.
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.
In game.toLinearSystem, sameEquation is exactly common row membership:
$$ \operatorname{sameEquation}(j,k) \Longleftrightarrow \exists i,\; j \in V_i \land k \in V_i. $$
This converts the generic presentation's commutation hypothesis into the
row-wise commutation data carried by an LCS observable strategy.
The linear-system support of equation $i$ is the game row support $V_i$:
$$ \operatorname{eqSupport}(\operatorname{game.toLinearSystem}, i) = V_i. $$
This rewrite aligns the generic equationWord construction with the LCS row
support used in observable products.
Evaluate the free-group lift of a list of variable generators as matrices: $$ \operatorname{val}\!\left(\operatorname{lift}(\rho_0) \prod_\ell x_{\ell}\right) = \prod_\ell \operatorname{obs}_{\ell}. $$ This list-level calculation is the basic evaluator for equation words before the support list is specialized to a row.
Evaluating an equation word gives the corresponding row observable product: $$ \operatorname{val}\bigl(\operatorname{lift}(\rho_0)(w_i)\bigr) = \operatorname{rowObservableProduct}_i. $$ This identifies the group word appearing in the equation relator with the matrix product whose value is extracted from the EPR/local-loss argument.
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.
Convert row-wise commutation into sameEquation commutation for
game.toLinearSystem:
$$ j,k \in V_i \Longrightarrow \operatorname{obs}_j\operatorname{obs}_k = \operatorname{obs}_k\operatorname{obs}_j. $$
This supplies the generic constructor with the commutation hypothesis required
for every pair of variables that appears together in some equation.
Game-specialized representation constructor:
$$ \operatorname{SolutionGroup}(\operatorname{game.toLinearSystem}) \to (\operatorname{Matrix}_n(\mathbb C))^\times . $$
This is solutionGroupRepresentationOfEquationProof with
S = game.toLinearSystem. The only extra work is translating the row-wise
commutation hypothesis into the sameEquation form expected by the generic
constructor.
Equations
- One or more equations did not get rendered due to their size.
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{Matrix}_n(\mathbb C))^\times, \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
- One or more equations did not get rendered due to their size.
Instances For
The EPR/local-loss representation sends var j to the observable unit:
$$ \rho(x_j) = \operatorname{obs}_j. $$
This confirms that the end-to-end constructor has the intended value on
solution-group variable generators.
The EPR/local-loss representation sends $J$ to $-I$: $$ \rho(J) = -I. $$ This confirms that the distinguished solution-group generator is represented by the scalar central involution in the final representation.