(3.37) — partial transpose preserves symmetric operators

Proved

BraneBrauer.Orthogonal.eq_3_37

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

brauer-algebrap2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1partial-transposepermutation-symmetry

Let $P_{\sigma,\tau}$ represent $(\sigma,\tau)\in S_m\times S_n$ on the mixed tensor space. For every operator $X$ ,

P_{\sigma,\tau}XP_{\sigma^{-1},\tau^{-1}}=X \quad\Longleftrightarrow\quad P_{\sigma,\tau}\Sigma(X)P_{\sigma^{-1},\tau^{-1}}=\Sigma(X).

Thus the partial transpose preserves the subgroup-conjugation invariance that defines a symmetric operator.

Formalization Note The matrix identity holds on the full operator space; the paper states it for Brauer elements.

Preamble

import Mathlib
import Definitions.Def_BraneBrauer_Orthogonal_Setting

noncomputable section

Formal statement

namespace BraneBrauer.Orthogonal

/-- (3.37), p. 15: partial transpose preserves invariance under
conjugation by the `Sₘ × Sₙ` tensor-factor permutation action. -/
theorem eq_3_37 {N m n : ℕ}
    (σ : Equiv.Perm (Fin m)) (τ : Equiv.Perm (Fin n))
    (X : Op N m n) :
    (permOp N m n σ τ * X * permOp N m n σ⁻¹ τ⁻¹ = X) ↔
    (permOp N m n σ τ * sigma X * permOp N m n σ⁻¹ τ⁻¹ = sigma X) := by sorry

end BraneBrauer.Orthogonal

Source

Kimura & Ramgoolam, Branes, Anti-Branes and Brauer Algebras in Gauge-Gravity duality, arXiv:0709.2158v2, p. 15, (3.37)

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