Mathlib upstream candidate: partial trace of a matrix over a tensor factor

Category: 1-Mathlib (CSD-free; Mathlib has no partial-trace construction).

For a matrix A on a product index m × n — i.e. an operator on ℂ^m ⊗ ℂ^n in the Kronecker realisation — the partial traces trace out one tensor factor:

• Matrix.traceRight A : Matrix m m R, tracing out the second factor n ((traceRight A) i j = ∑ k, A (i, k) (j, k));
• Matrix.traceLeft A : Matrix n n R, tracing out the first factor m.

These are the matrix-level reduced-operator maps ρ ↦ Tr_n ρ of quantum information. The API records the defining property on Kronecker products (traceRight_kronecker : traceRight (A ⊗ₖ B) = trace B • A), trace-preservation (trace_traceRight), linearity, and that the maps preserve Hermitian-ness and positive-semidefiniteness (traceRight_posSemidef) — the facts needed to send a density operator to its reduced density operator.

The positivity proof is clean: traceRight A = ∑ k, A.submatrix (·,k) (·,k), a finite sum of principal submatrices, so Matrix.PosSemidef.submatrix + Matrix.posSemidef_sum give the result with no test-vector bookkeeping.

Namespace / staging

Declarations live in namespace Matrix (Mathlib's natural symbol namespace), so dot notation is preserved and upstreaming requires only a file move to (or append onto) a Mathlib/LinearAlgebra/Matrix/PartialTrace.lean, no symbol rename.

Provenance

Needed for the CSD empirical suite's no-communication theorem in reduced-density form (E3b) and no-broadcasting (E2): see specs/qm-empirical-tests.md §3bis and specs/partial-trace-plan.md. Mathlib has no partial trace as of the pinned revision (Lean 4.29.0-rc8).

Consumers

• CsdLean4/LF2/ReducedDensity.lean (DensityOperatorIx.reduced).
• (planned) CsdLean4/Empirical/QM/NoCommunication.lean E3b reduced-density form.

Tags

matrix, partial trace, tensor product, kronecker, density operator, positive semidefinite

def Matrix.traceRight {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype n] [AddCommMonoid R] (A : Matrix (m × n) (m × n) R) : Matrix m m R

Partial trace over the second factor. For A on the product index m × n (an operator on ℂ^m ⊗ ℂ^n), traceRight A traces out the n factor: (traceRight A) i j = ∑ k, A (i, k) (j, k).

Equations

• A.traceRight = Matrix.of fun (i j : m) => ∑ k : n, A (i, k) (j, k)

def Matrix.traceLeft {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [AddCommMonoid R] (A : Matrix (m × n) (m × n) R) : Matrix n n R

Partial trace over the first factor. traceLeft A traces out the m factor: (traceLeft A) i j = ∑ k, A (k, i) (k, j).

Equations

• A.traceLeft = Matrix.of fun (i j : n) => ∑ k : m, A (k, i) (k, j)

@[simp]

theorem Matrix.traceRight_apply {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [AddCommMonoid R] (A : Matrix (m × n) (m × n) R) (i j : m) : A.traceRight i j = ∑ k : n, A (i, k) (j, k)

@[simp]

theorem Matrix.traceLeft_apply {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [AddCommMonoid R] (A : Matrix (m × n) (m × n) R) (i j : n) : A.traceLeft i j = ∑ k : m, A (k, i) (k, j)

theorem Matrix.traceRight_eq_sum_submatrix {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [AddCommMonoid R] (A : Matrix (m × n) (m × n) R) : A.traceRight = ∑ k : n, A.submatrix (fun (i : m) => (i, k)) fun (i : m) => (i, k)

traceRight as a finite sum of principal submatrices over the second index.

@[simp]

theorem Matrix.traceRight_zero {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [AddCommMonoid R] : traceRight 0 = 0

theorem Matrix.traceRight_add {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [AddCommMonoid R] (A B : Matrix (m × n) (m × n) R) : (A + B).traceRight = A.traceRight + B.traceRight

theorem Matrix.traceRight_smul {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] {S : Type u_4} [AddCommMonoid R] [Monoid S] [DistribMulAction S R] (c : S) (A : Matrix (m × n) (m × n) R) : (c • A).traceRight = c • A.traceRight

theorem Matrix.traceRight_kronecker {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [CommSemiring R] (A : Matrix m m R) (B : Matrix n n R) : (kroneckerMap (fun (x1 x2 : R) => x1 * x2) A B).traceRight = B.trace • A

Defining property on Kronecker products. Tracing out the second factor of A ⊗ B scales A by Tr B: traceRight (A ⊗ₖ B) = Tr B • A. (traceRight (A ⊗ₖ B)) i j = ∑ k, A i j * B k k = A i j * Tr B = (Tr B • A) i j.

theorem Matrix.traceLeft_kronecker {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [CommSemiring R] (A : Matrix m m R) (B : Matrix n n R) : (kroneckerMap (fun (x1 x2 : R) => x1 * x2) A B).traceLeft = A.trace • B

Defining property on Kronecker products (left). traceLeft (A ⊗ₖ B) = Tr A • B. (traceLeft (A ⊗ₖ B)) i j = ∑ k, A k k * B i j = Tr A * B i j = (Tr A • B) i j.

theorem Matrix.trace_traceRight {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [AddCommMonoid R] (A : Matrix (m × n) (m × n) R) : A.traceRight.trace = A.trace

Partial trace is trace-preserving. Tr (traceRight A) = Tr A. Tr (traceRight A) = ∑ i, ∑ k, A (i,k) (i,k) = ∑ (i,k), A (i,k) (i,k) = Tr A.

theorem Matrix.trace_traceLeft {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [AddCommMonoid R] (A : Matrix (m × n) (m × n) R) : A.traceLeft.trace = A.trace

Partial trace is trace-preserving (left). Tr (traceLeft A) = Tr A.

theorem Matrix.traceRight_conjTranspose {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [AddCommMonoid R] [StarAddMonoid R] (A : Matrix (m × n) (m × n) R) : A.traceRight.conjTranspose = A.conjTranspose.traceRight

traceRight commutes with conjugate-transpose, hence preserves Hermitian-ness.

theorem Matrix.traceLeft_conjTranspose {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [AddCommMonoid R] [StarAddMonoid R] (A : Matrix (m × n) (m × n) R) : A.traceLeft.conjTranspose = A.conjTranspose.traceLeft

theorem Matrix.IsHermitian.traceRight {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [AddCommMonoid R] [StarAddMonoid R] {A : Matrix (m × n) (m × n) R} (hA : A.IsHermitian) : A.traceRight.IsHermitian

traceRight preserves Hermitian-ness.

theorem Matrix.IsHermitian.traceLeft {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [AddCommMonoid R] [StarAddMonoid R] {A : Matrix (m × n) (m × n) R} (hA : A.IsHermitian) : A.traceLeft.IsHermitian

theorem Matrix.PosSemidef.traceRight {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {A : Matrix (m × n) (m × n) R} (hA : A.PosSemidef) : A.traceRight.PosSemidef

Partial trace preserves positive-semidefiniteness. Since traceRight A = ∑ k, A.submatrix (·,k) (·,k) is a finite sum of principal submatrices, this follows from PosSemidef.submatrix + posSemidef_sum. This is the load-bearing fact for the reduced density operator.

theorem Matrix.PosSemidef.traceLeft {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {A : Matrix (m × n) (m × n) R} (hA : A.PosSemidef) : A.traceLeft.PosSemidef

Partial trace preserves positive-semidefiniteness (left).

theorem Matrix.traceLeft_conjTranspose_kronecker_one {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing R] [StarRing R] {U : Matrix m m R} (hU : U.conjTranspose * U = 1) (M : Matrix (m × n) (m × n) R) : (kroneckerMap (fun (x1 x2 : R) => x1 * x2) U 1 * M * (kroneckerMap (fun (x1 x2 : R) => x1 * x2) U 1).conjTranspose).traceLeft = M.traceLeft

Partial trace is invariant under a unitary on the traced-out factor. If U is unitary (Uᴴ U = 1) then conjugating M by U ⊗ I does not change the partial trace over the first factor: traceLeft ((U ⊗ₖ I) · M · (U ⊗ₖ I)ᴴ) = traceLeft M.

This is the matrix form of "a local unitary on Alice's subsystem leaves Bob's reduced state invariant" — the no-communication / no-signalling content. The two Kronecker I factors pin the Bob indices; the Alice factors collapse through Uᴴ U = I.

theorem Matrix.traceLeft_sum_conjTranspose_kronecker_one {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing R] [StarRing R] {p : Type u_4} {ι : Type u_5} [Fintype p] [Fintype ι] {K : ι → Matrix p m R} (hK : ∑ l : ι, (K l).conjTranspose * K l = 1) (M : Matrix (m × n) (m × n) R) : (∑ l : ι, kroneckerMap (fun (x1 x2 : R) => x1 * x2) (K l) 1 * M * (kroneckerMap (fun (x1 x2 : R) => x1 * x2) (K l) 1).conjTranspose).traceLeft = M.traceLeft

Partial trace is invariant under a local channel on the traced-out factor. The Kraus-summed generalisation of traceLeft_conjTranspose_kronecker_one: for any finite family of (possibly rectangular) Kraus operators K : ι → Matrix p m that are trace-preserving (∑ᵢ (K i)ᴴ (K i) = 1),

traceLeft (∑ᵢ (K i ⊗ I) · M · (K i ⊗ I)ᴴ) = traceLeft M.

This is the no-communication / no-signalling content for an arbitrary trace-preserving Kraus family (a Kraus-sum object is automatically CP, so this covers any local channel): applying it on Alice's subsystem leaves Bob's reduced state Tr_A invariant. The load-bearing hypothesis is trace-preservation alone (∑ᵢ (K i)ᴴ (K i) = 1, used to recombine the Alice factors); complete positivity is not needed for the proof. The two Kronecker I factors pin the Bob indices.

theorem Matrix.traceRight_kronecker_one_mul {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [Semiring R] [DecidableEq n] (X : Matrix m m R) (M : Matrix (m × n) (m × n) R) : (kroneckerMap (fun (x1 x2 : R) => x1 * x2) X 1 * M).traceRight = X * M.traceRight

Partial trace is a left module map over X ⊗ I. Pulling a first-factor operator X ⊗ I out of traceRight: traceRight ((X ⊗ₖ I) · M) = X · traceRight M. The I on the Bob factor lets the X commute straight through the partial trace over Bob's index.

theorem Matrix.traceRight_mul_kronecker_one {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [Semiring R] [DecidableEq n] (M : Matrix (m × n) (m × n) R) (X : Matrix m m R) : (M * kroneckerMap (fun (x1 x2 : R) => x1 * x2) X 1).traceRight = M.traceRight * X

Partial trace is a right module map over X ⊗ I. traceRight (M · (X ⊗ₖ I)) = traceRight M · X.