The partial trace of a matrix on a product index

For a square matrix Y with rows and columns indexed by m × n, the partial trace over the second factor is the m × m matrix Matrix.partialTraceRight Y with entries ∑ k, Y (i, k) (j, k), the sum of the diagonal blocks Matrix.blockDiag Y k. When the index m × n labels the monomial basis of a tensor product of two finite-dimensional spaces, this is the partial trace Tr₂ of quantum mechanics, which forgets the second subsystem.

The partial trace preserves the trace, Matrix.trace_partialTraceRight, sends a Kronecker product A ⊗ₖ B to Tr B • A, Matrix.partialTraceRight_kronecker, sends 1 to card n • 1, Matrix.partialTraceRight_one, and is a bimodule map over the first factor: Tr₂ ((A ⊗ₖ 1) * Y * (B ⊗ₖ 1)) = A * Tr₂ Y * B (Matrix.partialTraceRight_kronecker_one_mul, Matrix.partialTraceRight_mul_kronecker_one). It commutes with conjugate transposition and preserves positive semidefiniteness, since each diagonal block is a compression of Y.

Symmetrically, the partial trace over the first factor is the n × n matrix Matrix.partialTraceLeft Y with entries ∑ k, Y (k, i) (k, j), the partial trace Tr₁ that forgets the first subsystem. It has the mirror-image properties: it preserves the trace and positive semidefiniteness, sends A ⊗ₖ B to Tr A • B, and is a bimodule map over the second factor, Tr₁ ((1 ⊗ₖ A) * Y * (1 ⊗ₖ B)) = A * Tr₁ Y * B. Together, Tr₂ ρ and Tr₁ ρ are the two reduced density matrices of a state ρ of a bipartite system.

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

The partial trace over the second factor of a square matrix indexed by m × n: the m × m matrix with entries ∑ k, Y (i, k) (j, k), the sum of the diagonal blocks of Y.

@[simp]

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

@[simp]

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

@[simp]

theorem Matrix.partialTraceRight_add {R : Type u_1} {m : Type u_2} {n : Type u_3} [Fintype n] [AddCommMonoid R] (Y Z : Matrix (m × n) (m × n) R) : (Y + Z).partialTraceRight = Y.partialTraceRight + Z.partialTraceRight

@[simp]

theorem Matrix.partialTraceRight_smul {R : Type u_1} {m : Type u_2} {n : Type u_3} [Fintype n] [AddCommMonoid R] {α : Type u_4} [DistribSMul α R] (c : α) (Y : Matrix (m × n) (m × n) R) : (c • Y).partialTraceRight = c • Y.partialTraceRight

@[simp]

theorem Matrix.trace_partialTraceRight {R : Type u_1} {m : Type u_2} {n : Type u_3} [Fintype n] [AddCommMonoid R] [Fintype m] (Y : Matrix (m × n) (m × n) R) : Y.partialTraceRight.trace = Y.trace

The partial trace preserves the trace.

@[simp]

theorem Matrix.partialTraceRight_conjTranspose {R : Type u_1} {m : Type u_2} {n : Type u_3} [Fintype n] [AddCommMonoid R] [StarAddMonoid R] (Y : Matrix (m × n) (m × n) R) : Y.conjTranspose.partialTraceRight = Y.partialTraceRight.conjTranspose

The partial trace commutes with conjugate transposition.

@[simp]

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

The partial trace of a Kronecker product A ⊗ₖ B is Tr B • A.

@[simp]

theorem Matrix.partialTraceRight_one {R : Type u_1} {m : Type u_2} {n : Type u_3} [Fintype n] [NonAssocSemiring R] [DecidableEq m] [DecidableEq n] : partialTraceRight 1 = ↑(Fintype.card n) • 1

The partial trace of the identity is card n • 1.

theorem Matrix.partialTraceRight_kronecker_one_mul {R : Type u_1} {m : Type u_2} {n : Type u_3} [Fintype n] [Semiring R] [Fintype m] [DecidableEq n] (A : Matrix m m R) (Y : Matrix (m × n) (m × n) R) : (kroneckerMap (fun (x1 x2 : R) => x1 * x2) A 1 * Y).partialTraceRight = A * Y.partialTraceRight

The partial trace is left linear over the first factor: Tr₂ ((A ⊗ₖ 1) * Y) = A * Tr₂ Y.

theorem Matrix.partialTraceRight_mul_kronecker_one {R : Type u_1} {m : Type u_2} {n : Type u_3} [Fintype n] [Semiring R] [Fintype m] [DecidableEq n] (Y : Matrix (m × n) (m × n) R) (B : Matrix m m R) : (Y * kroneckerMap (fun (x1 x2 : R) => x1 * x2) B 1).partialTraceRight = Y.partialTraceRight * B

The partial trace is right linear over the first factor: Tr₂ (Y * (B ⊗ₖ 1)) = Tr₂ Y * B.

theorem Matrix.PosSemidef.partialTraceRight {R : Type u_1} {m : Type u_2} {n : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [AddLeftMono R] {Y : Matrix (m × n) (m × n) R} (hY : Y.PosSemidef) : Y.partialTraceRight.PosSemidef

The partial trace of a positive semidefinite matrix is positive semidefinite: it is the sum of the compressions of Y to the diagonal blocks.

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

The partial trace over the first factor of a square matrix indexed by m × n: the n × n matrix with entries ∑ k, Y (k, i) (k, j), the sum of the compressions of Y to the blocks {k} × n.

@[simp]

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

@[simp]

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

@[simp]

theorem Matrix.partialTraceLeft_add {R : Type u_1} {m : Type u_2} {n : Type u_3} [Fintype m] [AddCommMonoid R] (Y Z : Matrix (m × n) (m × n) R) : (Y + Z).partialTraceLeft = Y.partialTraceLeft + Z.partialTraceLeft

@[simp]

theorem Matrix.partialTraceLeft_smul {R : Type u_1} {m : Type u_2} {n : Type u_3} [Fintype m] [AddCommMonoid R] {α : Type u_4} [DistribSMul α R] (c : α) (Y : Matrix (m × n) (m × n) R) : (c • Y).partialTraceLeft = c • Y.partialTraceLeft

@[simp]

theorem Matrix.trace_partialTraceLeft {R : Type u_1} {m : Type u_2} {n : Type u_3} [Fintype m] [AddCommMonoid R] [Fintype n] (Y : Matrix (m × n) (m × n) R) : Y.partialTraceLeft.trace = Y.trace

The partial trace over the first factor preserves the trace.

@[simp]

theorem Matrix.partialTraceLeft_conjTranspose {R : Type u_1} {m : Type u_2} {n : Type u_3} [Fintype m] [AddCommMonoid R] [StarAddMonoid R] (Y : Matrix (m × n) (m × n) R) : Y.conjTranspose.partialTraceLeft = Y.partialTraceLeft.conjTranspose

The partial trace over the first factor commutes with conjugate transposition.

@[simp]

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

The partial trace over the first factor of a Kronecker product A ⊗ₖ B is Tr A • B.

@[simp]

theorem Matrix.partialTraceLeft_one {R : Type u_1} {m : Type u_2} {n : Type u_3} [Fintype m] [NonAssocSemiring R] [DecidableEq m] [DecidableEq n] : partialTraceLeft 1 = ↑(Fintype.card m) • 1

The partial trace over the first factor of the identity is card m • 1.

theorem Matrix.partialTraceLeft_one_kronecker_mul {R : Type u_1} {m : Type u_2} {n : Type u_3} [Fintype m] [Semiring R] [Fintype n] [DecidableEq m] (A : Matrix n n R) (Y : Matrix (m × n) (m × n) R) : (kroneckerMap (fun (x1 x2 : R) => x1 * x2) 1 A * Y).partialTraceLeft = A * Y.partialTraceLeft

The partial trace over the first factor is left linear over the second factor: Tr₁ ((1 ⊗ₖ A) * Y) = A * Tr₁ Y.

theorem Matrix.partialTraceLeft_mul_one_kronecker {R : Type u_1} {m : Type u_2} {n : Type u_3} [Fintype m] [Semiring R] [Fintype n] [DecidableEq m] (Y : Matrix (m × n) (m × n) R) (B : Matrix n n R) : (Y * kroneckerMap (fun (x1 x2 : R) => x1 * x2) 1 B).partialTraceLeft = Y.partialTraceLeft * B

The partial trace over the first factor is right linear over the second factor: Tr₁ (Y * (1 ⊗ₖ B)) = Tr₁ Y * B.

theorem Matrix.PosSemidef.partialTraceLeft {R : Type u_1} {m : Type u_2} {n : Type u_3} [Fintype m] [Ring R] [PartialOrder R] [StarRing R] [AddLeftMono R] {Y : Matrix (m × n) (m × n) R} (hY : Y.PosSemidef) : Y.partialTraceLeft.PosSemidef

The partial trace over the first factor of a positive semidefinite matrix is positive semidefinite: it is the sum of the compressions of Y to the blocks {k} × n.