Projections of relabeled tensor-product strategies

These equations expose the unchanged registers and state without unfolding the game carried by a strategy. Measurement equations expose only the relabeling.

@[simp]

theorem MIPRE.TensorProductStrategy.relabel_dA {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {X' : Type u_5} {Y' : Type u_6} {A' : Type u_7} {B' : Type u_8} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype X'] [Fintype Y'] [Fintype A'] [Fintype B'] {G : Game X Y A B} (S : TensorProductStrategy G) (G' : Game X' Y' A' B') (eX : X' → X) (eY : Y' → Y) (eA : A' ≃ A) (eB : B' ≃ B) : (S.relabel G' eX eY eA eB).dA = S.dA

Relabeling preserves Alice's register dimension.

@[simp]

theorem MIPRE.TensorProductStrategy.relabel_dB {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {X' : Type u_5} {Y' : Type u_6} {A' : Type u_7} {B' : Type u_8} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype X'] [Fintype Y'] [Fintype A'] [Fintype B'] {G : Game X Y A B} (S : TensorProductStrategy G) (G' : Game X' Y' A' B') (eX : X' → X) (eY : Y' → Y) (eA : A' ≃ A) (eB : B' ≃ B) : (S.relabel G' eX eY eA eB).dB = S.dB

Relabeling preserves Bob's register dimension.

@[simp]

theorem MIPRE.TensorProductStrategy.relabel_ψ {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {X' : Type u_5} {Y' : Type u_6} {A' : Type u_7} {B' : Type u_8} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype X'] [Fintype Y'] [Fintype A'] [Fintype B'] {G : Game X Y A B} (S : TensorProductStrategy G) (G' : Game X' Y' A' B') (eX : X' → X) (eY : Y' → Y) (eA : A' ≃ A) (eB : B' ≃ B) : (S.relabel G' eX eY eA eB).ψ = S.ψ

Relabeling preserves the literal shared state.

@[simp]

theorem MIPRE.TensorProductStrategy.relabel_PA_M {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {X' : Type u_5} {Y' : Type u_6} {A' : Type u_7} {B' : Type u_8} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype X'] [Fintype Y'] [Fintype A'] [Fintype B'] {G : Game X Y A B} (S : TensorProductStrategy G) (G' : Game X' Y' A' B') (eX : X' → X) (eY : Y' → Y) (eA : A' ≃ A) (eB : B' ≃ B) (x : X') (a : A') : (S.relabel G' eX eY eA eB).PA.M x a = S.PA.M (eX x) (eA a)

Alice's relabeled effects are the original effects at relabeled questions and answers.

@[simp]

theorem MIPRE.TensorProductStrategy.relabel_PB_M {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {X' : Type u_5} {Y' : Type u_6} {A' : Type u_7} {B' : Type u_8} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype X'] [Fintype Y'] [Fintype A'] [Fintype B'] {G : Game X Y A B} (S : TensorProductStrategy G) (G' : Game X' Y' A' B') (eX : X' → X) (eY : Y' → Y) (eA : A' ≃ A) (eB : B' ≃ B) (y : Y') (b : B') : (S.relabel G' eX eY eA eB).PB.M y b = S.PB.M (eY y) (eB b)

Bob's relabeled effects are the original effects at relabeled questions and answers.