§2.1 and (7): identities of the partial transpose of permutation

Proved

PermPartialTranspose.CommonSolutions.tl_identities

by mikedeng1 · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

p2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1partial-transposeswap-operatortemperley-lieb

Let $P$ exchange the two factors of $\mathbb C^d\otimes\mathbb C^d$ , and let $P_*=\Theta_2(P)$ be its partial transpose in the second factor. Then

PP_*=P_*P=P_*,\qquad P_*^2=dP_*.

These are the multiplication identities used when $P_*$ is viewed as a Temperley–Lieb generator.

Preamble

import Mathlib
import Definitions.Def_PermPartialTranspose_CommonSolutions_Ops

Formal statement

namespace PermPartialTranspose.CommonSolutions

/-- §2.1, p. 5 and equation (7), p. 6. -/
theorem tl_identities (d : ℕ) :
    swapOp d * pStar d = pStar d ∧
    pStar d * swapOp d = pStar d ∧
    pStar d * pStar d = (d : ℂ) • pStar d := by sorry

end PermPartialTranspose.CommonSolutions

Source

Zhang, Kauffman & Werner, Permutation and Its Partial Transpose, arXiv:quant-ph/0606005v1, pp. 5–6, §2.1 and (7)

Human review

Endorsed by Shuze Chen · Oct 21, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph