The order of a finite pair's algebras is the operator order

In a finite pair (MIPRE/Foundations/FinitePair.lean) each player's algebra is ordered by its own order, and represented injectively on the model's space onto the commutant of the other player's operators. This file shows that the two orders agree (reports/c6b-paper-proofs.md, §4 Lemma 10 and §5 Lemma 13): for a star-ordered 𝒜, 0 ≤ a exactly when 0 ≤ π (πA a) in B(H) (IsFinitePair.nonneg_iff_A), and likewise for ℬ. So positive operator valued and projective measurements of the represented operators pull back to the players' algebras, and push forward.

• The commutants as C⋆-algebras. The commutant StarSubalgebra.centralizer ℂ s of a set of operators is norm closed (isClosed_centralizer), hence a C⋆-algebra (StarSubalgebra.cstarAlgebra), and star-ordered with the order of B(H) (starOrderedRing_centralizer, registered here as an instance).
• The players' algebras as commutants (IsFinitePair.equivA, IsFinitePair.equivB): in a finite pair, a ↦ π (πA a) is a ⋆-isomorphism of 𝒜 onto the commutant of the second player's operators: injective by injA, onto by commutantA.
• Order agreement (IsFinitePair.nonneg_iff_A, IsFinitePair.nonneg_iff_B): a ⋆-ring homomorphism between star-ordered rings is monotone, and the inverse of the isomorphism is one. The forward direction is π_πA_nonneg; the backward one is where the commutant matters, through the square root of a positive operator of the commutant, which lies in it.
• Transport of measurements (POVMIn.mapHom, isPVMIn_map_equiv_iff): a unital ⋆-ring homomorphism between star-ordered rings carries a POVM to a POVM, and a ⋆-isomorphism carries projective measurements both ways; in particular a POVM of a product has POVMs as coordinates (POVMIn.fst, POVMIn.snd).

Commutants of operators

instance MIPRE.isClosed_centralizer {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (s : Set (H →L[ℂ] H)) : IsClosed ↑(StarSubalgebra.centralizer ℂ s)

The commutant of a set of operators is norm closed.

instance MIPRE.instStarOrderedRingCentralizer {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (s : Set (H →L[ℂ] H)) : StarOrderedRing ↥(StarSubalgebra.centralizer ℂ s)

The commutant of a set of operators is star-ordered with the order of B(H) (starOrderedRing_centralizer).

Transport of measurements along ⋆-homomorphisms

def MIPRE.POVMIn.mapHom {X : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype X] [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] [Ring S] [StarRing S] [PartialOrder S] [StarOrderedRing S] {F : Type u_4} [FunLike F R S] [RingHomClass F R S] [NonUnitalStarRingHomClass F R S] (f : F) (P : POVMIn X R) : POVMIn X S

The image of a POVM under a unital ⋆-ring homomorphism between star-ordered rings, which is monotone: each operator is replaced by its image. (POVMIn.map coarse-grains the outcomes instead.)

Equations

• MIPRE.POVMIn.mapHom f P = { mats := fun (x : X) => ⟨f (P.op x), ⋯⟩, nonneg := ⋯, normalized := ⋯ }

@[simp]

theorem MIPRE.POVMIn.mapHom_op {X : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype X] [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] [Ring S] [StarRing S] [PartialOrder S] [StarOrderedRing S] {F : Type u_4} [FunLike F R S] [RingHomClass F R S] [NonUnitalStarRingHomClass F R S] (f : F) (P : POVMIn X R) (x : X) : (mapHom f P).op x = f (P.op x)

The operators of a transported POVM are the images of the operators.

@[simp]

theorem MIPRE.POVMIn.mapHom_symm_mapHom {X : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype X] [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] [Ring S] [StarRing S] [PartialOrder S] [StarOrderedRing S] [Algebra ℂ R] [Algebra ℂ S] (e : R ≃⋆ₐ[ℂ] S) (P : POVMIn X R) : mapHom e.symm (mapHom e P) = P

Transport along a ⋆-isomorphism and back is the identity.

@[simp]

theorem MIPRE.POVMIn.mapHom_mapHom_symm {X : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype X] [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] [Ring S] [StarRing S] [PartialOrder S] [StarOrderedRing S] [Algebra ℂ R] [Algebra ℂ S] (e : R ≃⋆ₐ[ℂ] S) (P : POVMIn X S) : mapHom e (mapHom e.symm P) = P

Transport along the inverse of a ⋆-isomorphism and back is the identity.

def MIPRE.POVMIn.fst {X : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype X] [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] [Ring S] [StarRing S] [PartialOrder S] [StarOrderedRing S] [Algebra ℂ R] [Algebra ℂ S] (P : POVMIn X (R × S)) : POVMIn X R

The first coordinates of a POVM of a product of star-ordered algebras, a POVM of the first factor.

Equations

• P.fst = MIPRE.POVMIn.mapHom (StarAlgHom.fst ℂ R S) P

def MIPRE.POVMIn.snd {X : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype X] [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] [Ring S] [StarRing S] [PartialOrder S] [StarOrderedRing S] [Algebra ℂ R] [Algebra ℂ S] (P : POVMIn X (R × S)) : POVMIn X S

The second coordinates of a POVM of a product of star-ordered algebras, a POVM of the second factor.

Equations

• P.snd = MIPRE.POVMIn.mapHom (StarAlgHom.snd ℂ R S) P

@[simp]

theorem MIPRE.POVMIn.fst_op {X : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype X] [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] [Ring S] [StarRing S] [PartialOrder S] [StarOrderedRing S] [Algebra ℂ R] [Algebra ℂ S] (P : POVMIn X (R × S)) (x : X) : P.fst.op x = (P.op x).1

The operators of the first coordinates are the first coordinates of the operators.

@[simp]

theorem MIPRE.POVMIn.snd_op {X : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype X] [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] [Ring S] [StarRing S] [PartialOrder S] [StarOrderedRing S] [Algebra ℂ R] [Algebra ℂ S] (P : POVMIn X (R × S)) (x : X) : P.snd.op x = (P.op x).2

The operators of the second coordinates are the second coordinates of the operators.

theorem MIPRE.isPVMIn_map_equiv_iff {X : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype X] [Ring R] [StarRing R] [Ring S] [StarRing S] [Algebra ℂ R] [Algebra ℂ S] (e : R ≃⋆ₐ[ℂ] S) {P : X → R} : (IsPVMIn fun (x : X) => e (P x)) ↔ IsPVMIn P

A ⋆-isomorphism carries projective measurements both ways.

The players' algebras of a finite pair

theorem MIPRE.BipartiteModel.opsA_subset_centralizer {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) : M.opsA ⊆ ↑(StarSubalgebra.centralizer ℂ M.opsB)

The first player's operators commute with the second player's and their adjoints.

theorem MIPRE.BipartiteModel.opsB_subset_centralizer {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) : M.opsB ⊆ ↑(StarSubalgebra.centralizer ℂ M.opsA)

The second player's operators commute with the first player's and their adjoints.

theorem MIPRE.BipartiteModel.IsFinitePair.coe_centralizer_opsB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) : ↑(StarSubalgebra.centralizer ℂ M.opsB) = M.opsA

In a finite pair, the commutant of the second player's operators is the first player's operators.

theorem MIPRE.BipartiteModel.IsFinitePair.coe_centralizer_opsA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) : ↑(StarSubalgebra.centralizer ℂ M.opsA) = M.opsB

In a finite pair, the commutant of the first player's operators is the second player's operators.

theorem MIPRE.BipartiteModel.IsFinitePair.mem_opsA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (x : ↥(StarSubalgebra.centralizer ℂ M.opsB)) : ↑x ∈ M.opsA

An element of the commutant of the second player's operators is one of the first player's.

theorem MIPRE.BipartiteModel.IsFinitePair.mem_opsB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (x : ↥(StarSubalgebra.centralizer ℂ M.opsA)) : ↑x ∈ M.opsB

An element of the commutant of the first player's operators is one of the second player's.

noncomputable def MIPRE.BipartiteModel.IsFinitePair.equivA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) : 𝒜 ≃⋆ₐ[ℂ] ↥(StarSubalgebra.centralizer ℂ M.opsB)

The first player's algebra of a finite pair is the commutant of the second player's operators, as a ⋆-isomorphism a ↦ π (πA a): injective by injA, onto by commutantA.

Equations

• hM.equivA = StarAlgEquiv.ofBijective ((M.π.comp M.πA).codRestrict (StarSubalgebra.centralizer ℂ M.opsB) ⋯) ⋯

noncomputable def MIPRE.BipartiteModel.IsFinitePair.equivB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) : ℬ ≃⋆ₐ[ℂ] ↥(StarSubalgebra.centralizer ℂ M.opsA)

The second player's algebra of a finite pair is the commutant of the first player's operators, as a ⋆-isomorphism b ↦ π (πB b).

Equations

• hM.equivB = ⋯.equivA

@[simp]

theorem MIPRE.BipartiteModel.IsFinitePair.coe_equivA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (a : 𝒜) : ↑(hM.equivA a) = M.π (M.πA a)

The operator of equivA a is π (πA a).

@[simp]

theorem MIPRE.BipartiteModel.IsFinitePair.coe_equivB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (b : ℬ) : ↑(hM.equivB b) = M.π (M.πB b)

The operator of equivB b is π (πB b).

theorem MIPRE.BipartiteModel.IsFinitePair.π_πA_equivA_symm {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (x : ↥(StarSubalgebra.centralizer ℂ M.opsB)) : M.π (M.πA (hM.equivA.symm x)) = ↑x

The operator of the inverse of equivA is the element of the commutant.

theorem MIPRE.BipartiteModel.IsFinitePair.π_πB_equivB_symm {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (x : ↥(StarSubalgebra.centralizer ℂ M.opsA)) : M.π (M.πB (hM.equivB.symm x)) = ↑x

The operator of the inverse of equivB is the element of the commutant.

theorem MIPRE.BipartiteModel.IsFinitePair.nonneg_iff_A {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} [PartialOrder 𝒜] [StarOrderedRing 𝒜] (hM : M.IsFinitePair) {a : 𝒜} : 0 ≤ M.π (M.πA a) ↔ 0 ≤ a

Order agreement in a finite pair (reports/c6b-paper-proofs.md, §4 Lemma 10, §5 Lemma 13): an element of the first player's algebra is nonnegative exactly when its operator is positive. This is also the statement that equivA preserves and reflects the order, 0 ≤ equivA a ↔ 0 ≤ a, since the commutant carries the operator order; it is the one order-agreement lemma of the library, and every other form (le_iff_A, the doubled model's Doubling.equiv_nonneg_iff) is derived from it.

theorem MIPRE.BipartiteModel.IsFinitePair.le_iff_A {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} [PartialOrder 𝒜] [StarOrderedRing 𝒜] (hM : M.IsFinitePair) {a a' : 𝒜} : M.π (M.πA a) ≤ M.π (M.πA a') ↔ a ≤ a'

Order agreement in a finite pair, for the order itself, first player.

theorem MIPRE.BipartiteModel.IsFinitePair.nonneg_iff_B {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} [PartialOrder ℬ] [StarOrderedRing ℬ] (hM : M.IsFinitePair) {b : ℬ} : 0 ≤ M.π (M.πB b) ↔ 0 ≤ b

Order agreement in a finite pair, for the second player's algebra (nonneg_iff_A for the swapped pair).

theorem MIPRE.BipartiteModel.IsFinitePair.le_iff_B {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} [PartialOrder ℬ] [StarOrderedRing ℬ] (hM : M.IsFinitePair) {b b' : ℬ} : M.π (M.πB b) ≤ M.π (M.πB b') ↔ b ≤ b'

Order agreement in a finite pair, for the order itself, second player.