The order of a matrix algebra over an ordered ⋆-ring

The extension of a bipartite model by a finite register (MIPRE.BipartiteModel.expand) gives each player the n × n matrices over the player's algebra. The analyses measure with positive operator valued measures in the players' algebras (MIPRE.POVMIn), which need those algebras to be ordered; matrices over an abstract ordered ⋆-ring are not, in Mathlib. This file orders them the way a ⋆-algebra is ordered: X ≤ Y when Y - X is a sum of elements Z⋆ Z (MatrixStar.instPartialOrderStar, with StarOrderedRing holding by construction).

That the relation is antisymmetric needs the entries' ring to be proper (StarProper): x⋆ x = 0 only for x = 0. Then an element of the cone has nonnegative diagonal entries, and a vanishing diagonal entry kills its row and its column; so an element of the cone whose negative is in the cone vanishes. The matrices are then proper again (MatrixStar.instStarProper), so the construction iterates, which is what registers adjoined to registers need.

C⋆-algebras and their ⋆-subalgebras are proper (StarProper.of_cstarRing, StarSubalgebra.instStarProper), which covers the algebras of the commuting-operator model; the complex matrices are (MatrixStar.instStarProperComplex), which covers the tensor-product model. The order on the complex matrices themselves is Mathlib's positive semidefinite order (MatrixOrder), not this one: ℂ is not given a StarProper instance, so this construction never applies to Matrix n n ℂ.

class MIPRE.StarProper (R : Type u_1) [Mul R] [Star R] [Zero R] : Prop

A proper ⋆-ring: x⋆ x = 0 only for x = 0.

• eq_zero_of_star_mul_self_eq_zero (x : R) : star x * x = 0 → x = 0

  x⋆ x = 0 forces x = 0.

theorem MIPRE.StarProper.of_cstarRing {R : Type u_1} [NonUnitalNormedRing R] [StarRing R] [CStarRing R] : StarProper R

instance MIPRE.StarSubalgebra.instStarProper {A : Type u_1} [NormedRing A] [StarRing A] [CStarRing A] [NormedAlgebra ℂ A] [StarModule ℂ A] (S : StarSubalgebra ℂ A) : StarProper ↥S

instance MIPRE.MatrixStar.instStarProperComplex {n : Type u_1} [Fintype n] [DecidableEq n] : StarProper (Matrix n n ℂ)

The complex matrices are proper: Xᴴ X = 0 forces X = 0.

@[reducible, inline]

abbrev MIPRE.MatrixStar.cone (n : Type u_3) (R : Type u_4) [Fintype n] [Ring R] [StarRing R] : AddSubmonoid (Matrix n n R)

The positive cone of the matrix algebra: the sums of elements Z⋆ Z.

Equations

• MIPRE.MatrixStar.cone n R = AddSubmonoid.closure (Set.range fun (Z : Matrix n n R) => star Z * Z)

theorem MIPRE.MatrixStar.diag_of_mem_cone {n : Type u_1} [Fintype n] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] [StarProper R] {c : Matrix n n R} (hc : c ∈ cone n R) (i : n) : 0 ≤ c i i ∧ (c i i = 0 → ∀ (j : n), c i j = 0 ∧ c j i = 0)

An element of the cone has nonnegative diagonal entries, and a vanishing diagonal entry kills its row and its column.

theorem MIPRE.MatrixStar.eq_zero_of_mem_cone_of_add {n : Type u_1} [Fintype n] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] [StarProper R] {p q : Matrix n n R} (hp : p ∈ cone n R) (hq : q ∈ cone n R) (h : p + q = 0) : p = 0

An element of the cone whose negative is in the cone vanishes.

@[instance_reducible]

instance MIPRE.MatrixStar.instPartialOrderStar {n : Type u_1} [Fintype n] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] [StarProper R] : PartialOrder (Matrix n n R)

The order of the matrix algebra over a proper ordered ⋆-ring: X ≤ Y when Y - X is a sum of elements Z⋆ Z.

Equations

• MIPRE.MatrixStar.instPartialOrderStar = { le := fun (X Y : Matrix n n R) => ∃ p ∈ MIPRE.MatrixStar.cone n R, Y = X + p, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

instance MIPRE.MatrixStar.instStarOrderedRing {n : Type u_1} [Fintype n] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] [StarProper R] : StarOrderedRing (Matrix n n R)

theorem MIPRE.MatrixStar.diag_nonneg {n : Type u_1} [Fintype n] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] [StarProper R] {M : Matrix n n R} (h : 0 ≤ M) (i : n) : 0 ≤ M i i

A nonnegative matrix has nonnegative diagonal entries.

instance MIPRE.MatrixStar.instStarProper {n : Type u_1} [Fintype n] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] [StarProper R] : StarProper (Matrix n n R)

The matrices over a proper ordered ⋆-ring are proper.

theorem MIPRE.real_smul_nonneg {A : Type u_1} [Ring A] [StarRing A] [Algebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] {r : ℝ} (hr : 0 ≤ r) {a : A} (ha : 0 ≤ a) : 0 ≤ ↑r • a

A nonnegative real multiple of a nonnegative element is nonnegative, in a star-ordered complex ⋆-algebra: r • z⋆ z = (√r • z)⋆ (√r • z).