Representation Theory

Why this algebra comparison matters

The walled Brauer algebra organizes the linear operators that commute with a general linear group acting on a tensor product of vector spaces and their duals. Its diagrams mix crossings and contractions, with a wall distinguishing the two tensor factors. This makes it useful in mixed tensor representation theory, where the ordinary symmetric group algebra no longer records every commuting operator. Sartori and Stroppel compare this diagram algebra with a level-two cyclotomic quotient of a degenerate affine walled Brauer algebra. Their comparison identifies a concrete part of the larger algebra by an explicit change of generators Sartori–Stroppel, Theorem 6.2.

The paper's result is a proved theorem. This mission asks for a machine-checked proof of its algebraic statement. The source builds the cyclotomic quotient using parameters arising from parabolic category $\mathcal O$, but the target here is the resulting algebra isomorphism. The dimension comparison that the authors obtain through category $\mathcal O$ is included as a separate milestone, in the exact numerical form used in their injectivity argument Sartori–Stroppel, Theorem 5.2, Corollary 5.8, and Lemma 5.9.

The oriented generators and the cyclotomic quotient

Fix $r,t\in\mathbb N$. An orientation $a$ is a word of length $r+t$ containing exactly $r$ upward arrows and $t$ downward arrows. The walled Brauer algebra $\operatorname{Br}_{r,t}(d)$ is a complex algebra with an idempotent $1_a$ for each orientation. At an adjacent pair of positions $k,k+1$, equal arrows admit a crossing $s_k1_a$. Unequal arrows admit a changed-orientation crossing $\widehat s_k1_a$, an orientation-preserving contraction $e_k1_a$, and a changed-orientation contraction $\widehat e_k1_a$. The relations (Br1)–(Br6) specify orthogonal idempotents, sources and targets, quadratic and braid relations, and interactions among crossings and contractions Sartori–Stroppel, Definition 2.1.

The degenerate affine walled Brauer algebra adds commuting elements $y_1,\ldots,y_{r+t}$ and their relations with the oriented generators. Its level-two cyclotomic quotient imposes a quadratic relation on $y_1$ in each first-arrow component Sartori–Stroppel, Definitions 2.5 and 2.8. Write this quotient as $A$. It uses positive integers $m,n$ and an integer $\delta$, with

$$\begin{aligned} \beta_1^\uparrow&=-\delta+(m+n)/2,&\beta_2^\uparrow&=(n-m)/2,\\ \beta_1^\downarrow&=(m+n)/2,&\beta_2^\downarrow&=\delta+(m-n)/2,\\ \omega_0&=m+n,&\omega_1&=-\delta m+(m+n)^2/2. \end{aligned}$$

The later $\omega_j$ follow the quadratic recurrence determined by the upward cyclotomic polynomial; they are fixed by these parameters. These are the paper's parameters (5.4), with values in $\mathbb C$ Sartori–Stroppel, Definition 5.1 and Lemma 2.9.

For each position $k$ and orientation $a$, let $\eta_k1_a$ project away from the generalized eigenspace of $y_k1_a$ with eigenvalue $\beta_1^{a_k}$. The spectral truncation is $f1_a=\eta_1\cdots\eta_{r+t}1_a$, with $f=\sum_a f1_a$. The intermediate products are $f_k1_a=\eta_1\cdots\eta_k1_a$ and $f_0=1$. This gives the corner algebra $fAf$ Sartori–Stroppel, Definition 5.6. The elements $b_k,c_k$, polynomial square roots, and resulting images $\sigma_k,\widehat\sigma_k,\tau_k,\widehat\tau_k$ are defined by (6.1)–(6.4) Sartori–Stroppel, Definition 6.1.

Formalization targets

The goal is the full form of the paper's isomorphism theorem:

$$\Phi:\operatorname{Br}_{r,t}(-\delta)\xrightarrow{\ \sim\ }fAf, \qquad (1_a,s_k1_a,\widehat s_k1_a,e_k1_a,\widehat e_k1_a) \mapsto(f1_a,\sigma_k1_a,\widehat\sigma_k1_a,\tau_k1_a,\widehat\tau_k1_a).$$

Here $m,n>0$, $m,n\ge r+t$, and $\delta\in\mathbb Z$ satisfy Assumption 5.5: $|\beta_2^\uparrow|+r+t<\beta_1^\uparrow$ and $|\beta_2^\downarrow|+r+t<\beta_1^\downarrow$. The inequalities separate the relevant eigenvalues. The explicit $m,n\ge r+t$ condition is needed for Theorem 5.2 in the paper's dimension argument; Assumption 5.5 alone does not imply it Sartori–Stroppel, Assumption 5.5 and Theorem 5.2.

The milestone list records the finite-dimensional inverse and square-root result (Proposition 4.2), the inverse sandwich identity (Lemma 8.7), the changed contraction parameter (Lemma 8.4), the equal-orientation involution (Lemma 8.5), the Jucys–Murphy image identity (Lemma 6.6), and the dimension of the spectral corner (Corollary 5.8 with Lemma 5.9). The last two are stated in algebraic forms that avoid taking the sought map or category $\mathcal O$ as extra hypotheses.

What the result supplies

The theorem gives an explicit dictionary between diagram generators and operators in a cyclotomic quotient, including the change from the quotient's loop parameter $\omega_0=m+n$ to the source parameter $-\delta$ Sartori–Stroppel, Remark 6.3. It also identifies the whole corner, rather than merely producing a homomorphism into it. This lets properties of the larger algebra be transported to the diagram algebra when their hypotheses are met. The paper discusses graded cellular and Koszul consequences, and an oriented-category extension, separately Sartori–Stroppel, Remarks 6.4–6.5.

A formal development must establish that the presentations do not collapse, that every required oriented relation survives the generator assignment, and that the image fills precisely $fAf$. The milestone statements isolate several of the authors' central identities, while the final theorem retains injectivity and surjectivity. A proof would also create reusable infrastructure for quotient presentations with source and target idempotents and for inverses in idempotent corners.

The central difficulty

The formulas for the images involve inverses and square roots after a spectral truncation, and the quotient need not be semisimple. Substituting a scalar directly into a formal power-series identity does not justify the key contraction identity in that setting; the authors explicitly point out this obstruction Sartori–Stroppel, Remark 6.3. The oriented relations also contain dotted symbols that stand for several local choices, so a single equation between global sums does not fully state every relation. Finally, proving that the map exists is only one part of the theorem: its image and kernel require separate control.

Formalization scope

Lean represents both algebras as quotients of free complex algebras by the paper's generators and relations. An orientation is a Boolean sequence with exactly $r$ true entries; true denotes an upward arrow. Positions start at zero in Lean, so a paper index $k$ corresponds to Lean index $k-1$. Relations involving dotted generators are imposed for every composable choice with the same source and target. Invalid orientation choices are zero. The affine quotient uses $e_k^2=\omega_0e_k$; the source of the theorem uses $e_k^2=-\delta e_k$. The recurrence fixes every $\omega_j$ rather than leaving later parameters free.

The $\eta_k$, intermediate $f_k$, and $f$ are defined from the polynomial spectral-idempotent characterization, rather than supplied as arbitrary hypotheses. An inverse of $xu$ is selected by its two inverse equations in the corner $uAu$. Square roots are not unique in the source, so each theorem holds for every family $R_k$ of polynomial square roots satisfying $R_k^2=b_kf$; the factorized form $Q_k=R_{k+1}R_k^{-1}$ is used. A vacuous hypothesis, a collapsed or under-related presentation, a freely chosen $f$, or a merely linear map does not express this target. The conclusion requires multiplication, the specified generator values, injectivity, and range exactly $fAf$.

The category $\mathcal O$ construction and the paper's later applications are outside this mission. The needed reusable pieces are the finite-dimensional algebra lemma, oriented presentation machinery, polynomial spectral idempotents, and corner algebra operations. Contributions that strengthen the supporting algebraic library or close any of the stated milestones are within scope.

Selected references

• Antonio Sartori and Catharina Stroppel, Walled Brauer algebras as idempotent truncations of level 2 cyclotomic quotients, arXiv preprint, 2015. arXiv:1411.2771v2.

Motivation

The Birman–Murakami–Wenzl (BMW) algebras were introduced by Birman and Wenzl and by Murakami to study the Kauffman link polynomial; they are deformations of the Brauer algebras and act as centralizer algebras of quantum groups of orthogonal and symplectic type on tensor powers of the natural module. Their cyclotomic generalization was introduced by Häring-Oldenburg (J. Pure Appl. Algebra 161 (2001)) as the BMW analogue of the Ariki–Koike algebras, the cyclotomic Hecke algebras of type $G(r,1,n)$. Representation theorists care about when such an algebra is semisimple: in the semisimple case its representation theory is governed by a combinatorial index set (multipartitions with extra data), and outside it one needs decomposition numbers.

For the Ariki–Koike algebra the answer is Ariki's criterion (J. Algebra 169 (1994)). For the ordinary BMW algebra ($r = 1$) it is due to Rui and Si (J. Reine Angew. Math., [17] in the paper). Rui and Xu proved that the cyclotomic BMW algebra is free and cellular for odd $r$ under their u-admissibility conditions (arXiv:0801.0465), and Goodman and Hauschild Mosley (arXiv:math/0612064) and Yu (PhD thesis, Sydney, 2007) obtained freeness by other routes. Rui and Si (arXiv:0807.4149, 2008) extended cellularity to even $r$ and, by computing Gram determinants of cell modules, gave a semisimplicity criterion for all $r \ge 2$. That criterion is the goal of this mission.

Setting

Let $F$ be a field and $r, n$ positive integers. Fix non-zero $q, u_1, \dots, u_r \in F$ with $\delta = q - q^{-1} \ne 0$ and the $u_i$ pairwise distinct, and a sign $\varepsilon \in \{1, -1\}$. Put $\alpha = \varepsilon$ if $r$ is odd and $\alpha = \varepsilon q^{-\varepsilon}$ if $r$ is even, $\varrho^{-1} = \alpha\prod_\ell u_\ell$, $\gamma_r(x) = 1$ ($r$ odd), $-x$ ($r$ even), and

$$\gamma_i = \Big(\gamma_r(u_i) + \delta^{-1}\varrho(u_i^2-1)\prod_{j \ne i}u_j\Big)\prod_{j\ne i}\frac{u_iu_j - 1}{u_i - u_j},\qquad \omega_a = \sum_{j=1}^r u_j^a\gamma_j\quad(a\in\mathbb Z).$$

These are the u-admissible parameters of Assumption 2.2. The cyclotomic Birman–Wenzl algebra $\mathscr B_{r,n}$ is the unital associative $F$-algebra generated by $T_i, E_i$ ($1 \le i < n$) and $X_j^{\pm1}$ ($1 \le j \le n$) subject to the relations a)–k) of Definition 2.1: among them the Kauffman skein relation $T_i^2 - \delta T_i + \delta\varrho E_i = 1$, the braid relations, $E_i^2 = \omega_0E_i$, the skein relations between $T_i$ and $X_i, X_{i+1}$, the unwrapping relations $E_1X_1^aE_1 = \omega_aE_1$ for all $a \in \mathbb Z$, the tangle and untwisting relations, $E_iX_iX_{i+1} = E_i = X_iX_{i+1}E_i$, and the cyclotomic relation $(X_1 - u_1)\cdots(X_1 - u_r) = 0$. The Ariki–Koike algebra $\mathscr H_{r,n}$ is generated by $g_1, \dots, g_{n-1}, y_1, \dots, y_n$ with $(g_i - q)(g_i + q^{-1}) = 0$, the braid relations, $y_{i+1} = g_iy_ig_i$, commuting $y_j$ and $(y_1 - u_1)\cdots(y_1 - u_r) = 0$.

Write $o(q^2) > n$ for "$q^{2k} \ne 1$ for $1 \le k \le n$", and set

$$Q_{r,\varrho} = \begin{cases}\{-\varepsilon q, \varepsilon q^{-1}\}, & 2 \nmid r,\\ \{-q^\varepsilon, q^\varepsilon\}, & 2 \mid r,\end{cases}\qquad S_{r,\varrho} = \begin{cases}\bigcup_{k=3}^n\{\pm q^{3-k}, \pm q^{k-3}, \varepsilon q^{3-2k}, -\varepsilon q^{2k-3}\}, & 2 \nmid r,\\ \bigcup_{k=3}^n\{\pm q^{3-k}, \pm q^{k-3}, \pm q^{(2k-3)\varepsilon}\}, & 2 \mid r.\end{cases}$$

Formalization targets

Goal: Theorem 6.8

For $n \ge 2$ and $r \ge 2$:

(a) if $u_iu_j = 1$ for some $i \ne j$, or $u_i \in Q_{r,\varrho}$ for some $i$, then $\mathscr B_{r,n}$ is not semisimple;

(b) if $u_iu_j \ne 1$ for all $i \ne j$ and no $u_i$ lies in $Q_{r,\varrho}$, then

$$\mathscr B_{r,2}\ \text{semisimple} \iff o(q^2) > 2 \ \text{and}\ \big(u_iu_j^{-1} = q^{2d},\ i<j \Rightarrow |d| \ge 2\big),$$

and for $n \ge 4$, $\mathscr B_{r,n}$ is semisimple if and only if (a) $o(q^2) > n$; (b) $|d| \ge n$ whenever $u_iu_j^{-1} = q^{2d}$, $i < j$; (c) $u_i \notin S_{r,\varrho}$ for all $i$; (d) $u_iu_j \notin \bigcup_{k=3}^n\{q^{4-2k}, q^{2k-4}\}$ for all $i \ne j$. For $n = 3$ the goal states that semisimplicity implies (a)–(d).

The page states (b)(2) as an equivalence for all $n \ge 3$. The goal keeps only necessity at $n = 3$: Proposition 6.2 and Lemma 6.3 describe the same cell module of $\mathscr B_{r,3}$ and list different exclusions ($\varepsilon q$ against $-\varepsilon q^{-1}$ for odd $r$), and $S_{r,\varrho}$ at $n = 3$ contains neither.

Milestones

The rank $\dim_F\mathscr B_{r,n} = r^n(2n-1)!!$ (Theorem 2.14); the corner identities $E_{n-1}\mathscr B_{r,n}E_{n-1} = E_{n-1}\mathscr B_{r,n-2}$ (Lemma 3.1) and $E_{f,n}\mathscr B_{r,n}E_{f,n} = \mathscr B_{r,n-2f}E_{f,n}$ (Corollary 3.2), corrected at the two-strand boundary by requiring some $\omega_a\ne0$; Proposition 6.1, which says that $\det G_{1,\emptyset} = \det(\omega_{a+b})_{a,b\in N_r}$ is non-zero exactly when $u_iu_j \ne 1$ ($i \ne j$) and no $u_i$ lies in $Q_{r,\varrho}$; Proposition 6.5(b), non-semisimplicity when that determinant vanishes; and the reduction "$\mathscr H_{r,n}$ not semisimple $\Rightarrow \mathscr B_{r,n}$ not semisimple" from the proof of Theorem 6.8.

Significance

The criterion gives a closed list of parameter values at which the cyclotomic BMW algebra fails to be semisimple, and so, by Graham–Lehrer theory, the parameters at which all cell modules are simple and pairwise non-isomorphic. Outside that list the algebra's simple modules, their dimensions and the decomposition of tensor-type modules are given by the combinatorics of up-down tableaux; inside it, the list says which Gram determinants vanish and where decomposition numbers begin. For $r = 1$ it specializes to the semisimplicity criterion for BMW algebras, and its conditions (a)–(b) are Ariki's conditions for $\mathscr H_{r,n}$.

As far as is known, none of this is machine-checked: Mathlib has no BMW, Brauer, Ariki–Koike or Iwahori–Hecke algebras and no cellular algebras. The mission formalizes the statements of the paper on a presentation of $\mathscr B_{r,n}$ by generators and relations; a solver must supply a basis (or at least a dimension count), the cellular structure and the Gram-determinant computations. The paper leaves several of its proofs to the reader ("by arguments in the proof of [19, 5.41]"), so the formal proofs would also close gaps in the published argument.

Difficulty

Non-semisimplicity in part (a) needs only one degenerate bilinear form on a non-zero cell module, but showing that the module is non-zero, or that $\mathscr B_{r,n}$ does not collapse, already needs a lower bound on the dimension of a presented algebra, which no rewriting argument provides: the rank $r^n(2n-1)!!$ is proved in the literature through seminormal representations. Sufficiency in part (b) requires the Gram determinants of all cell modules $\Delta(f,\lambda)$, which the paper obtains by a recursion over up-down tableaux; vanishing of a single factor must be traced through branching and Morita-type functors between levels $n-2$, $n-1$ and $n$. Ariki's criterion for $\mathscr H_{r,n}$ is itself an external input.

Formalization scope

$\mathscr B_{r,n}$ and $\mathscr H_{r,n}$ are RingQuot quotients of FreeAlgebra F on finite generator types; indices are 0-based (the Lean T i is the paper's $T_{i+1}$), and $X_j^{-1}$ is a separate generator tied to $X_j$ by relation a). The sign $\varepsilon \in \mathbb Z^\times$ is the free parameter and $\alpha, \varrho, \gamma_i, \omega_a$ are computed from $(q, u, \varepsilon)$, so the parameters are u-admissible by construction. The $u_i$ are pairwise distinct (Assumption 2.2(1) divides by $u_i - u_j$; the paper extends 2.2 to coincident $u_i$ through [19, 3.11]). "Semisimple" is Mathlib's IsSemisimpleRing. The condition $o(q^2) > n$ is written as $q^{2k} \ne 1$ for $1 \le k \le n$, not through orderOf, which is $0$ for elements of infinite order. Relations d) and g) both use $\omega_0 = \sum_j\gamma_j$, which equals the paper's $1 - \delta^{-1}(\varrho - \varrho^{-1})$ for these parameters; were they different, the presentation would collapse. The corrected corner milestones require $n\ge3$ or some $\omega_a\ne0$ in Lemma 3.1, and $2f<n$ or some $\omega_a\ne0$ in Corollary 3.2. At $n=2$, $r=2$, $q=3$, $u=(2,\tfrac12)$, and $\varepsilon=1$, every $\omega_a$ vanishes, exposing the missing condition. $\det G_{1,\emptyset}$ is expressed as the Hankel determinant of the $\omega_a$, and $\mathscr B_{r,m} \subseteq \mathscr B_{r,n}$ is the subalgebra generated by the first generators.

A presentation that collapses to the zero algebra would make the goal false in part (a) but trivially true elsewhere; the rank milestone rules this out. Replacing semisimplicity by non-vanishing of Gram determinants would turn the goal into a different theorem and is not acceptable.

A complete development needs a basis theorem for $\mathscr B_{r,n}$, cellular algebras and Graham–Lehrer's semisimplicity criterion, the Ariki–Koike algebra and Ariki's criterion, and Gram-determinant computations. The cellular-algebra layer and the Ariki–Koike algebra are reusable beyond this mission; contributions of any of these, or of the milestones on their own, are welcome.

Selected references

• H. Rui and M. Si, The representation theory of cyclotomic BMW algebras (printed title The representations of cyclotomic BMW algebras, II), preprint, 2008. https://arxiv.org/abs/0807.4149
• H. Rui and J. Xu, The representations of cyclotomic BMW algebras, preprint, 2007. https://arxiv.org/abs/0801.0465
• R. Häring-Oldenburg, Cyclotomic Birman–Murakami–Wenzl algebras, J. Pure Appl. Algebra 161 (2001), 113–144. https://doi.org/10.1016/S0022-4049(00)00100-6
• S. Ariki, On the semi-simplicity of the Hecke algebra of $(\mathbb Z/r\mathbb Z)\wr\mathfrak S_n$, J. Algebra 169 (1994), 216–225. https://doi.org/10.1006/jabr.1994.1280
• J. J. Graham and G. I. Lehrer, Cellular algebras, Invent. Math. 123 (1996), 1–34. https://doi.org/10.1007/BF01232365
• J. S. Birman and H. Wenzl, Braids, link polynomials and a new algebra, Trans. Amer. Math. Soc. 313 (1989), 249–273. https://doi.org/10.1090/S0002-9947-1989-0992598-X

Motivation

The Brauer algebra packages pairings of points into an algebra whose multiplication records how pairings join when diagrams are stacked. It was introduced by Brauer as the centralizer algebra of orthogonal and symplectic groups acting on tensor powers of their natural representation (Brauer 1937), and is semisimple for generic $\delta$ (Wenzl 1988). It provides an example where diagram combinatorics and the choice of coefficient ring affect the same algebraic question. King, Martin, and Parker study central idempotents that separate the diagrams with few propagating lines from the remaining part of the algebra. Their construction works over a ring $K$ designed to retain useful specializations of the parameter $\delta$; a solution obtained only in the field $\mathbb Q(\delta)$ would lose that arithmetic information. King–Martin–Parker, §1–§2

The mission concerns their main result, Theorem 14. It asks for the precise bridge between a diagram equation, coefficients constrained to $K$, and an idempotent that splits an ideal quotient. The source is the 2016 arXiv version; all page and result numbers here refer to that version. King–Martin–Parker, Theorem 14

Setting

A Brauer diagram on $n$ strands is a perfect matching of two rows of $n$ nodes. A strand joining the rows is a propagating line; a strand within one row is a horizontal arc. The set of all such diagrams is a basis for $B_n$, here over $F=\mathbb Q(\delta)$, where $\delta$ is an indeterminate. To multiply diagrams $A$ and $B$, place $A$ over $B$ and identify the adjacent rows. The resulting outer pairing is another diagram $C$. If $v(A,B)$ connected components close entirely in the middle row, then

$$AB=\delta^{v(A,B)}C.$$

This loop factor is part of the algebra, even when no loop is visible in a particular example. The span $J_n(\ell)$ of diagrams with at most $\ell$ propagating lines is a two-sided ideal. Simultaneous relabelling of the upper and lower rows by $\mathfrak S_n$ partitions diagrams into orbits $O$. The orbit sum $D_O=\sum_{A\in O}A$ uses each original, unnormalised diagram once. King–Martin–Parker, §2.2–§2.3

The source works with a coefficient ring inside $F$:

$$K=\{f/g:f,g\in\mathbb Z[\delta],\ g\text{ monic},\ \deg f\leq\deg g\}.$$

For $\ell<n$ and even $n-\ell$, let $u$ be the diagram with cups at $(1,2),(3,4),\ldots,(n-\ell-1,n-\ell)$ in each row and vertical lines elsewhere. The paper uses the normalized element $\bar u=\delta^{-(n-\ell)/2}u$. Its required equation $\bar uX=-\bar u$ has the same solutions as $uX=-u$ over $F$. King–Martin–Parker, §2.2, equation (4), and §3, equation (5)

Formalization targets

The goal is Theorem 14. For orbit coefficients $c_O$ and $X_c=\sum_Oc_OD_O$, it asserts a unique solution with $c_O\in K$ to

$$uX_c=-u.$$

It further asserts that $\varphi=1+X_c$ satisfies $\varphi-1\in J_n(\ell)$ and $\varphi J_n(\ell)=J_n(\ell)\varphi=0$, and is central and idempotent. By Lemma 10, these properties identify the splitting of $0\to J_n(\ell)\to B_n\to B_n/J_n(\ell)\to0$. King–Martin–Parker, Lemma 10 and Theorem 14

The milestones follow the paper's proof, in attack order: the general bimodule splitting criterion (Lemma 10); the basis of the $\mathfrak S_n$-centralizer $Z_{\mathfrak S_n}(B_n)$ given by the orbit sums (Lemma 11); the paper's assertion that for $\ell<n$ the splitting idempotent $\varphi_n(\ell)$ exists with coefficients in $K$ (p. 8); the fact that $\bar u$ fixes every diagram $A_{\mathfrak t}$ carrying its cups and maps no other diagram onto $A_{\mathfrak t}$ without a negative power of $\delta$ (Proposition 12); the independence of the linear equations in the $c_{\mathfrak t}$, i.e. injectivity of $X\mapsto uX$ on orbit-sum combinations (equation (6)); and membership of every solution coefficient in $K$ (Proposition 13). Lemma 10 is reusable beyond diagram algebras. King–Martin–Parker, §3

Significance

The idempotent separates the ideal of diagrams with few propagating lines from the quotient as bimodules. Its centrality means this separation is compatible with multiplication on either side. Specifying the coefficients in $K$ also preserves information about specializations of $\delta$ that a field-only existence statement would omit. The paper uses the resulting splitting idempotents in its discussion of primitive central idempotents and Brauer algebra representations. King–Martin–Parker, §4

The theorem is proved in the cited paper. This mission supplies a machine-checkable interface for its definitions and statements; the theorem proofs remain open. A completed development would verify the diagram multiplication, the ideal and orbit descriptions, the ring-theoretic splitting criterion, and the coefficient claim in one Lean environment. These components can support later formalizations involving diagram algebras or central idempotents.

Difficulty

An equation over $F$ alone does not give a splitting idempotent with coefficients in $K$. The coefficient restriction is sensitive to the exact loop factor in multiplication and to whether orbit sums use normalized or original diagrams. The equations indexed by diagrams also need to determine the orbit coefficients uniquely, while the two-sided annihilation requirement concerns every element of the ideal, not just the displayed cup diagram. These are distinct claims in the source; checking one of them does not silently establish the others. King–Martin–Parker, §3

Formalization scope

Lean represents a diagram as a fixed-point-free involution on Fin n ⊕ Fin n; the left summand is the upper row. A three-row graph defines its composite and loop count. The Brauer space is the finite-dimensional function space Diagram n → RatFunc ℚ, with an explicit bilinear multiplication bmul; the statements do not assume a ring instance whose associativity has not yet been proved. The parameter is RatFunc.X, representing the indeterminate $\delta$. The ideal is the $F$-span of exactly the basis diagrams with propagating count at most $\ell$.

The goal fixes $\ell<n$ and additionally assumes even $n-\ell$ (the existence milestone, stated on the page for every $\ell<n$, does not). That parity condition makes the paper's displayed product $\bar u_1\bar u_3\cdots\bar u_{n-\ell-1}$ well defined. Lean uses zero-based indices, so the paper's cup $(2j+1,2j+2)$ is represented by $(2j,2j+1)$. The equation uses unnormalised $u$ but has the same solutions as the paper's normalized equation because $\delta$ is nonzero in $F$. Orbit sums are unnormalised, as in the printed Theorem 14. The centralizer $Z_{\mathfrak S_n}(B_n)$ is the set of elements commuting with every diagram having $n$ propagating lines. The index set of the goal consists only of orbits of diagrams with at most $\ell$ propagating lines; it is equivalent to the paper's Spore-tableau index set, without introducing that classification into this mission.

The statement constructs $\varphi$ as $1+X_c$ from coefficients $c$, rather than postulating an arbitrary splitting idempotent. Neither the ideal nor the equation is replaced with a degenerate special case: with $J=B_n$ condition (ii) would force $\varphi=0$, and with $J=0$ it would be vacuous, so the ideal is exactly the span of the diagrams with at most $\ell$ propagating lines, and the loop factor $\delta^{v(A,B)}$ is kept in the product. The main reusable infrastructure comprises finite diagrams, the loop-weighted product, orbit sums, and the generic bimodule splitting lemma. Contributions may establish these structural facts, the milestone statements, and the final theorem.

Selected references

• O. H. King, P. P. Martin, and A. E. Parker, On central idempotents in the Brauer algebra, Journal of Algebra, 2016; arXiv:1609.01183v1. Page references use the arXiv version.
• R. Brauer, On algebras which are connected with the semisimple continuous groups, Annals of Mathematics 38 (1937), 857–872. https://doi.org/10.2307/1968843
• H. Wenzl, On the structure of Brauer's centralizer algebras, Annals of Mathematics 128 (1988), 173–193. https://doi.org/10.2307/1971466

Motivation

The Temperley–Lieb algebra is a family of algebras built from generators that satisfy local relations. It appears in diagrammatic representation theory and provides a tractable setting in which to study cellular bases and Gram determinants. A Gram determinant tests whether the bilinear form on a module is degenerate after specializing its parameter. Thus an explicit determinant formula records information about when a cell module may cease to be simple. Enyang's 2007 paper develops a Murphy-style basis, a commuting family of operators and an orthogonal basis, then gives a closed product for these determinants. The mission targets that final product, with the preceding statements retained as milestones. Enyang, 2007

The generic cellular-algebra definitions and spectral-projector construction have already been formalized in the published package associated with Mathas's work. This mission specializes those objects to the actual Temperley–Lieb presentation and computes its explicit polynomial factors. Mathas, 2006

Setting

Let $R=\mathbb Z[x]$, with $x$ an indeterminate. For $n\ge1$, the algebra $A_n(x)$ has generators $e_1,\ldots,e_{n-1}$ and relations

$$e_i^2=xe_i,\qquad e_ie_{i\pm1}e_i=e_i,\qquad e_ie_j=e_je_i\quad\text{when }|i-j|\ge2.$$

A shape at level $n$ is a pair $\lambda=(f,n-2f)$ with $0\le2f\le n$. A standard up–down tableau of shape $\lambda$ is a path of shapes from $(0,0)$ to $\lambda$: at each level its cup count stays fixed or increases by one. Write $\mathfrak T_n(\lambda)$ for the set of these paths and $\dim(\lambda)=|\mathfrak T_n(\lambda)|$. The paper orders paths by comparing their cup counts at every level; $u\triangleright t$ means strict pointwise dominance. Enyang, §§1–2

For each shape, $m_\lambda$ is the product $e_1e_3\cdots e_{2f-1}$. Ordered generator products $w_{i,j}$ and their tableau products $v_t,v_t^*$ give the Murphy elements $m_{uv}=v_u^*m_\lambda v_v$. Lemma 2.3 asserts that they form a cellular basis. The cellular multiplication law computes a Gram form on each cell module $C^\lambda$. The determinant $\det(\lambda)$ is the determinant of this computed form in the Murphy basis; it is not assigned the desired closed product by definition. Enyang, Lemma 2.3 and §5

The Jucys–Murphy elements $T_k$ form a commuting family in $A_n(x)$. Their triangular action on a tableau $t$ has content $r_t(k)\in R$. Over the fraction field $F=\operatorname{Frac}(R)$, the spectral product $F_t$ produces a vector $f_t=m_tF_t$. These vectors form an orthogonal basis, with squared norms $\langle f_t,f_t\rangle$ whose product equals $\det(\lambda)$. The auxiliary polynomials are fixed by $p_0=0$, $p_1=1$ and $p_{i+1}=xp_i-p_{i-1}$. Enyang, §§3–5

Formalization targets

The milestones follow the paper's own sequence: the Murphy cellular basis (Lemma 2.3) and the neighbour criterion for the elements $v_t$ (Corollary 2.2); the basic properties of $T_i$ and $z_i$ (Lemma 3.1), the sum identities for $p_i$ (Lemma 3.4), the action of $z_i$ on the generator of a cell module (Lemma 3.5), the triangular action of $T_k$ and $z_k$ with diagonals $r_t(k)$ and $z_t(k)=p_ip_{k-i+1}$ (Corollaries 3.6, 3.7) and the alternative recursion for $T_{i+1}$ (Corollary 4.2); the seminormal basis (Lemma 4.4), the diagonal coefficients of $e_k$ on it (Corollary 4.6) and the norm ratio of neighbouring seminormal vectors (Lemma 4.7); the identification of $\det(\lambda)$ with $\prod_t\langle f_t,f_t\rangle$ (§5) and the branching law (Lemma 5.1). The goal is Lemma 5.2, the closed product. When $n>2f$,

$$\det(f,n-2f)=\prod_{i=1}^{f}\left(\frac{p_{n-2f+i+1}}{p_i}\right)^{\dim(f-i,n-2f+2i)}.$$

When $n=2f$, the predecessor shape $\mu=(f-1,1)$ lies at level $n-1$, and the target is

$$\det(f,0)=\det(\mu)x^{\dim(f,0)}.$$

The quotient in the first formula is evaluated in $F$; the second equality is in $R$. Both clauses occur in the printed Lemma 5.2. Enyang, Lemma 5.2, p. 20

Significance

The result turns a determinant of a matrix indexed by all tableaux of a shape into a finite product of explicit recursive polynomials. It makes the factors that can vanish under specialization visible and lets later representation-theoretic questions be asked in terms of those factors. The branching law supplies a compatible description across levels of the algebra tower. Enyang, §5

The paper proves the formulas mathematically. The statements in this mission are compiled Lean targets with proof holes; they do not yet constitute machine-checked proofs of Enyang's results. A complete development would supply the cellular-basis theorem, establish the paper's explicit content action, connect the integral and field Gram forms, and prove the norm and determinant formulas. The quotient presentation, tableau encoding and cellular package can be reused for related specializations and diagram-algebra calculations.

Difficulty

The generator relations make local products manageable, but a determinant does not expose its factors directly. The cell module is indexed by whole paths, and the operators act triangularly rather than diagonally in the Murphy basis. Passing to seminormal vectors changes the basis while keeping track of the bilinear form; this requires the local coefficient and norm statements, not just the commutation of the operators. At the boundary $n=2f$, one of the two possible predecessor shapes disappears, so a uniform two-factor branching formula would introduce a nonexistent module. Enyang, §§3–5

Formalization scope

The Lean algebra is a quotient of a free algebra by all three defining relation families. It uses one-based generators; an out-of-range generator is set to zero, and every stated result guards its meaningful indices. Shapes are finite cup-count indices and tableaux are finite paths with a pointwise order. The unrolled products defining $v_t$ and $v_t^*$ follow the page's multiplication order. The integral statements use $R=\mathbb Z[x]$; seminormal vectors use $F=\operatorname{Frac}(R)$ and the published cellular-algebra package's coordinate-space cell module and Gram form. Existence of the required Murphy and JM data is asserted, preventing a theorem about an empty class of such data from passing vacuously.

Several printed details need explicit treatment. The page-2 endpoint $e_{2f+1}$ in $m_\lambda$ is replaced by $e_{2f-1}$, giving exactly $f$ factors and $m_{(0,n)}=1$. The missing $z_0$ is zero by the paper's sum formula. The $r_s(k)$ denominator in the definition of $F_t$ means $r_t(k)$. Lemma 4.4(3) says “orthonormal,” but later nonunit norms show that the valid conclusion is pairwise orthogonality. The direction of $\triangleright$ in the printed definition of $g_{\lambda,\mu}$ and Lemma 5.2 is reversed relative to the formula's denominator and the proof; the target product runs over shapes with fewer cups. Identity (3.3) of Lemma 3.4 is false as printed (at $i=j=2$, $k=1$ it reads $x^3-2x=x$); the target is the form its proof derives, with last factor $p_{j+k-1}$. The goal and the cellular milestones take $n\ge1$, since the paper's tower starts at $A_1(x)=R$; for $n=0$ the even case of Lemma 5.2 would refer to the non-existent shape $(-1,1)$. Enyang, pp. 2, 10, 17, 19–20

Useful contributions include proofs of the algebraic Murphy-basis statement, the content formulas, the seminormal basis properties, the integral-to-field determinant identification and the branching law. Each has a separate mission item and source index.

Selected references

• John Enyang, Representations of Temperley–Lieb Algebras, arXiv preprint arXiv:0710.3218v1, 2007. arXiv
• Andrew Mathas, Seminormal forms and Gram determinants for cellular algebras, arXiv preprint arXiv:math/0604108v4, 2006. arXiv

Motivation

Let $V$ be the natural representation of $GL_n$ and $V^*$ its dual. The walled Brauer algebra $B_{r,s}(\delta)$ describes the endomorphisms of mixed tensor space $V^{\otimes r}\otimes V^{*\otimes s}$ that commute with $GL_n$, through mixed Schur–Weyl duality. It was introduced in this role independently by Turaev, Koike and Benkart–Chakrabarti–Halverson–Leduc–Lee–Stroomer around 1989–1994. It is also a diagram algebra in its own right, defined for every parameter $\delta$ in the ground field. Its representation theory controls the decomposition of mixed tensor space, and it serves as a test case for the cellular and "tower of recollement" methods used for the Brauer and partition algebras.

Cox, De Visscher, Doty and Martin (arXiv:0709.0851, 2007) determine the blocks of $B_{r,s}(\delta)$ in characteristic zero. They also classify the semisimple walled Brauer algebras and give a linkage principle in positive characteristic. Their characteristic-zero answer has the shape familiar from algebraic Lie theory: blocks are orbits of a Weyl group, $\Sigma_{r+s}$, under a dot action shifted by a vector $\rho(\delta)$. The analogous result for the ordinary Brauer algebra, with the Weyl group of type $D$, is due to Cox, De Visscher and Martin (arXiv:math/0601387, 2009).

Setting

Fix $r,s\in\mathbb N$, an algebraically closed field $k$ and $\delta\in k$. A Brauer diagram on $n=r+s$ strands pairs up $2n$ nodes, $n$ northern and $n$ southern. Lines joining the two rows are propagating lines; the others are arcs. Put a wall after the first $r$ nodes of each row. A diagram is walled if no propagating line crosses the wall and every arc does. Two diagrams are multiplied by stacking the first above the second. Each closed loop formed in the middle row is removed and contributes a factor $\delta$. The walled Brauer algebra $B_{r,s}(\delta)$ is the $k$-span of the walled diagrams with this product. The permutation diagrams span the group algebra $k\Sigma_{r,s}$ of $\Sigma_{r,s}=\Sigma_r\times\Sigma_s$.

The algebra is cellular. Its cell modules $\Delta_{r,s}(\lambda^L,\lambda^R)$ are indexed by bipartitions $(\lambda^L,\lambda^R)$ with $\lambda^L\vdash r-t$ and $\lambda^R\vdash s-t$, for $0\le t\le\min(r,s)$. Here $t$ is the number of northern arcs. In characteristic zero the simple modules $L_{r,s}(\lambda^L,\lambda^R)$, the heads of the cell modules, are indexed by the same set. The one exception is $(\emptyset,\emptyset)$, which is excluded when $\delta=0$ and $0<r=s$. At $r=s=0$, the algebra is $k$ and its unique simple has the empty bipartition as label. Two simple modules lie in the same block when no central idempotent of $B_{r,s}(\delta)$ separates them.

A box in row $i$ and column $j$ of a Young diagram has content $j-i$. Two bipartitions are $\delta$-balanced when the boxes of $\lambda^L\setminus\mu^L$ can be paired with those of $\lambda^R\setminus\mu^R$, and the boxes of $\mu^L\setminus\lambda^L$ with those of $\mu^R\setminus\lambda^R$, so that the contents in each pair sum to $-\delta$.

For $\delta\in\mathbb Z$, the weight lattice is $X_{r,s}=\mathbb Z^{r+s}$, with coordinates indexed by $-r,\dots,-1,1,\dots,s$. Put

$$\rho(\delta)=(r,r-1,\dots,1;\ \delta,\delta-1,\dots,\delta-s+1).$$

The group $W=\Sigma_{r+s}$ permutes the coordinates and acts by the dot action $w.\lambda=w(\lambda+\rho)-\rho$. A bipartition is sent to the weight $(\bar\lambda^L;\lambda^R)=(-\lambda^L_r,\dots,-\lambda^L_1;\lambda^R_1,\dots,\lambda^R_s)$.

Formalization targets

Goal: Corollary 8.4 (characteristic zero)

For $k$ of characteristic $0$, $\delta\in\mathbb Z$, and labels $\lambda,\mu$ of simple $B_{r,s}(\delta)$-modules,

$$L_{r,s}(\lambda)\ \text{and}\ L_{r,s}(\mu)\ \text{lie in the same block}\iff (\bar\lambda^L;\lambda^R)=w.(\bar\mu^L;\mu^R)\ \text{for some } w\in\Sigma_{r+s}.$$

The balanced classification: Corollary 7.7

For every $\delta\in k$ in characteristic $0$, two labels are in the same block if and only if they are $\delta$-balanced, and each block contains a unique minimal weight.

Supporting results

The milestones, in proof order, are the following.

• Lemma 4.1: the action of $T_{r,s}=\sum E_{i,j}$ on cell modules.
• Theorem 4.2 and Corollary 4.3: content conditions on composition factors and on blocks.
• Theorem 6.2: two-box homomorphisms, $\operatorname{Hom}(\Delta(\lambda),\Delta(\mu))\cong k$.
• Proposition 7.1 and Corollary 7.3: box pairings and the necessity of balance.
• Lemma 8.1: the counting form of balance.
• Propositions 8.2 and 8.3: orbit $\Leftrightarrow$ balance.

Significance

The goal reduces the block structure of $B_{r,s}(\delta)$ to a combinatorial test. Two weights are in the same block exactly when their $\rho(\delta)$-shifted vectors are permutations of each other, a check that takes linear time. Within a block there is a unique minimal weight. The Weyl-group description is the starting point for the paper's positive-characteristic linkage principle, in which the affine Weyl group $W_p$ takes the place of $W$. It also places the walled Brauer algebra alongside the Brauer algebra and the algebraic groups as an algebra whose characteristic-zero blocks are governed by a reflection group.

The result has been proved since 2007. As far as is known, no part of it has been machine-checked. This mission produces three things.

1. A diagram-level definition of $B_{r,s}(\delta)$ for every $\delta$, together with its cell and simple modules. This layer is reusable for the Brauer, partition and Temperley–Lieb algebras.
2. A content calculus for bipartitions.
3. Formal proofs of the paper's chain of results. The combinatorial half (Lemma 8.1, Propositions 8.2 and 8.3) is independent of the algebra, and it can be completed first.

Difficulty

The obvious first idea is to treat the walled Brauer algebra through mixed Schur–Weyl duality, as a centraliser algebra. That gives only a quotient of $B_{r,s}(\delta)$ when $\delta$ is a small integer, and nothing at all when $\delta$ is not a natural number, so it cannot reach the full statement. The obstruction is the non-semisimple regime ($\delta\in\mathbb Z$, $|\delta|\le r+s-2$), where cell modules have nontrivial composition factors.

The necessary condition is a scalar computation, obtained by evaluating a central-like element on cell modules. Sufficiency is the hard direction. It needs explicit nonzero homomorphisms between cell modules that differ by a removable strip of boxes, built from the two-box homomorphisms of Theorem 6.2 by an induction using restriction and induction along the tower $B_{r-1,s}\subset B_{r,s}$. The final step, matching balance with dot orbits, is a combinatorial argument on edges of skew diagrams in which the shift by $\rho(\delta)$ must be tracked exactly.

Formalization scope

1. Characteristic. The goal and the algebraic milestones take $k$ algebraically closed of characteristic $0$; the goal takes $\delta\in\mathbb Z$, cast into $k$. The paper's hypothesis "$\Sigma$-semisimple" also allows characteristic $p>\max(r,s)$. That case is not posed, because there the integer in $\rho(\delta)$ is not determined by $\delta\in k$. Lemma 8.1 and Propositions 8.2 and 8.3 are purely combinatorial, with $\delta\in\mathbb Z$.
2. The algebra. $B_{r,s}(\delta)$ has the $\delta^{\#\text{loops}}$ product and is never the centraliser algebra. It is realised as its faithful left regular representation: the subalgebra of matrices on the walled diagrams generated by left multiplication by each diagram, which is isomorphic to the paper's algebra.
3. Cell modules. In characteristic $0$ they are modelled as $B_{r,s}X_t\,y_\lambda$ modulo $J_{t+1}$. Here $X_t$ is the diagram with arcs $r-u$ — $r+1+u$ ($u<t$), $y_\lambda$ is the Young symmetrizer $\sum_{\sigma\in C}\sum_{\tau\in R}\operatorname{sgn}(\sigma)\sigma\tau$ on the propagating nodes, and $J_{t+1}$ is the span of the diagrams with more than $t$ arcs.
4. Simple modules and blocks. Simple modules are heads, i.e. quotients by the intersection of the maximal submodules. "Same block" is the central-idempotent criterion on simple modules.
5. Combinatorial conventions. Young diagrams are Mathlib's YoungDiagram, with 0-based cells; contents are unchanged by the shift. Nodes are Fin (r+s). The weight lattice is Fin r ⊕ Fin s → ℤ, where Sum.inl i is the paper's coordinate $-(i+1)$ and Sum.inr j is coordinate $j+1$. $W$ is Equiv.Perm (Fin r ⊕ Fin s).
6. Statements over weights. These assume at most $r$ and $s$ rows, so that the embedding loses nothing.

Two corrections to the printed text are adopted. Lemma 8.1 is stated "for all $i\in\mathbb Z$", and the reflection formula on p. 31 is read as $s_\beta(\lambda)=\lambda-(\lambda,\beta)\beta$, the transposition of two coordinates. The label exception in Theorem 2.7(iii) is applied only when $r=s>0$; its literal wording would incorrectly leave $B_{0,0}(0)=k$ without a simple module.

A trivializing formalization would replace the block relation by a relation defined through contents or orbits, or would replace the algebra by a centraliser algebra or by $k\Sigma_{r,s}$. Both are excluded: the block relation is the algebra's own central-idempotent relation, and the algebra is the diagram algebra itself.

Contributions are welcome at every layer. Useful general infrastructure includes associativity of diagram composition, Young symmetrizers and Specht modules over a field of characteristic $0$, and the Jucys–Murphy content formula. Proofs of the combinatorial Section 8 results and of the cellular structure of $B_{r,s}(\delta)$ are also needed.

Selected references

• A. Cox, M. De Visscher, S. Doty, P. Martin, On the blocks of the walled Brauer algebra, preprint arXiv:0709.0851v1, 2007. https://arxiv.org/abs/0709.0851
• A. Cox, M. De Visscher, P. Martin, The blocks of the Brauer algebra in characteristic zero, Represent. Theory 13 (2009). https://arxiv.org/abs/math/0601387
• G. Benkart, M. Chakrabarti, T. Halverson, R. Leduc, C. Lee, J. Stroomer, Tensor product representations of general linear groups and their connections with Brauer algebras, J. Algebra 166 (1994). https://doi.org/10.1006/jabr.1994.1165
• T. Halverson, Characters of the centralizer algebras of mixed tensor representations of GL(r,C) and the quantum group U_q(gl(r,C)), Pacific J. Math. 174 (1996). https://doi.org/10.2140/pjm.1996.174.359
• J. J. Graham, G. I. Lehrer, Cellular algebras, Invent. Math. 123 (1996). https://doi.org/10.1007/BF01232365

Why trace class representations matter

A strongly continuous unitary representation turns each group element into a unitary operator on a Hilbert space. Averaging those operators against a smooth, compactly supported function gives a bounded operator. When every such average is trace class, its trace defines a distribution character. The trace condition is therefore a bridge from an operator representation to a scalar distribution that can be studied by harmonic analysis. Van Dijk, Neeb, Salmasian and Zellner collect and extend characterizations of this condition for finite-dimensional Lie groups in their 2015 preprint. Their Theorem 1.3 is the target here.

The authors identify one of the equivalences, between the trace class property and a trace class negative power of the Nelson Laplacian, with an earlier statement of Cartier that had appeared without a proof or reference. Their further conclusion that one finite degree of differentiability suffices is presented as a new result; it gives finite order for the distribution character. These are claims about the cited preprint, not claims of prior machine verification. Source: introduction and Theorem 1.3, pp. 2–5.

The representation and its test functions

Let $G$ be a finite-dimensional real Lie group, let $H$ be a complex Hilbert space, and let $\pi:G\to\mathrm U(H)$ be a strongly continuous unitary representation. Fix a left Haar measure $\mu$. For a compactly supported continuous function $f:G\to\mathbb C$, the integrated operator is $\pi(f)v=\int_G f(g)\pi(g)v\,d\mu(g)$ for each $v\in H$. Write $C^m_c(G)$ for compactly supported functions with $m$ continuous derivatives and $C^\infty_c(G)$ for smooth compactly supported functions. Write $B_1(H)$ and $B_2(H)$ for the trace class and Hilbert–Schmidt ideals of bounded operators on $H$.

Choose a basis $X_1,\ldots,X_n$ of the Lie algebra $\mathfrak g$. The Nelson Laplacian is $\Delta=\sum_{j=1}^n X_j^2$ in the enveloping algebra. The derived representation applies $d\pi(\Delta)$ on smooth vectors. Its closure $D=\overline{d\pi(\Delta)}$ is a non-positive self-adjoint operator, and $(1-D)^{-1}$ is bounded. The choice of basis determines $D$, while the theorem holds for an arbitrary fixed basis. Source: §1 and proof of Theorem 1.3, pp. 3–4.

Formalization targets

Five equivalent conditions

The mission goal is the complete five-way equivalence in Theorem 1.3:

$$\begin{aligned} \text{(i)}\;&\exists m\ge1:\ \pi(C^m_c(G))\subseteq B_1(H) \text{ and }\pi:C^m_c(G)\to B_1(H)\text{ is continuous};\\ \text{(ii)}\;&\pi(C^\infty_c(G))\subseteq B_1(H) \text{ and }\pi:C^\infty_c(G)\to B_1(H)\text{ is continuous};\\ \text{(iii)}\;&\pi(C^\infty_c(G))\subseteq B_1(H);\\ \text{(iv)}\;&\pi(C^\infty_c(G))\subseteq B_2(H);\\ \text{(v)}\;&\exists k\ge1:\ (1-D)^{-k}\in B_1(H). \end{aligned}$$

The continuity clauses are part of the target; they cannot be inferred merely from the displayed inclusions. The milestone list includes the four nontrivial implications named in the paper's proof, its finite-order claim and the two displayed identities needed to connect the function and operator Laplacians. Source: Theorem 1.3 and proof, pp. 3–5.

What the equivalence gives

Condition (iii) is formulated using every smooth compactly supported function. Condition (i) replaces smoothness by one finite differentiability order that works uniformly for the representation, while retaining continuity into the trace class ideal. This is the form needed to conclude that the distribution character has finite order. Condition (v) tests the same property with one operator associated with the Lie algebra basis. These consequences are stated by the authors in the introduction and derived in §1. Source: pp. 2–5.

A formal proof would connect Lie-group differentiation, Bochner integration, Schatten ideals and the topology of compactly supported function spaces in one reusable development. The target and milestones here are open Lean statements: compilation checks their types, not their proofs. The previously posed Lemmas 1.1 and 1.2 of the same paper remain separate open platform items, and can be used by solvers without being re-posed here.

Where the difficulty lies

Showing that each $\pi(f)$ is trace class does not immediately give continuity of $f\mapsto\pi(f)$ in trace norm: operator-norm convergence alone does not control trace norm. The paper also needs to pass from trace class images of smooth functions to an operator statement about $(1-D)^{-k}$, and then back to functions with only finitely many derivatives. The obvious shortcut of treating $d\pi(\Delta)$ as a bounded operator fails because its natural domain is the smooth-vector space and its closure is generally unbounded. The proof therefore has substantial analytic content beyond elementary ideal inclusions. Source: proof of Theorem 1.3, pp. 4–5.

Formalization scope

Lean represents $G$ as a Hausdorff finite-dimensional Lie group modelled on a finite-dimensional real normed space $E$, equipped with a regular left Haar measure. It represents $H$ as a complete complex inner-product space, without a separability assumption, and the representation by a strongly continuous monoid homomorphism into unitary continuous linear equivalences. The Lie algebra is the tangent space $E$ at the identity, and the basis is an arbitrary finite basis of $E$. The quantifiers for $m$ and $k$ include explicit lower bounds $1\le m$ and $1\le k$, matching the paper's convention $\mathbb N_0=\mathbb N\cup\{0\}$.

Smooth vectors are exactly those whose orbit maps are smooth. The derived action is the manifold derivative of that orbit map at the identity, used only on smooth vectors. The function-side Laplacian uses right-invariant directional derivatives; its second-order sign agrees with the paper's action. A bounded operator $R$ is characterized by $R(w-d\pi(\Delta)w)=w$ on every smooth vector. The paper's essential self-adjointness and density statement identifies this $R$ uniquely with $(1-D)^{-1}$; the theorem carries that characterization as a hypothesis. The hypothesis must be satisfiable, and the interpretation must remain the paper's resolvent.

Continuity on $C^m_c(G)$ is encoded by a bound on the Schatten $1$-norm for every compact support set, with one constant for all functions supported there. For $C^\infty_c(G)$, the derivative order may depend on the compact set. The Schatten norms and classes are reused published definitions, with norm values in $[0,\infty]$; no alternate trace norm is introduced. Equation (1) is an identity of distributions tested against smooth compactly supported functions. A complete proof needs the smooth-vector integration lemma, Lie-group test-function approximation, the function-side parametrix and operator ideal estimates. These components are useful beyond this mission.

Selected references

• G. van Dijk, K.-H. Neeb, H. Salmasian and C. Zellner, On the characterization of trace class representations and Schwartz operators, arXiv preprint, 2015, arXiv:1512.02451v1.

Motivation

Integrals of polynomial functions of the matrix entries of a random element of a compact group appear across mathematical physics and probability: in random matrix theory (moments of Haar-distributed unitary, orthogonal and symplectic matrices), in lattice gauge theory (the link integrals of $U(N)$ gauge fields), and in quantum information (averages of quantum channels over random unitaries, twirling, unitary designs). Weingarten first computed asymptotics of such integrals for $U(N)$ in 1978 (Weingarten, J. Math. Phys. 19 (1978)); Collins (IMRN 2003) and Collins–Śniady (CMP 2006) gave exact formulas for the unitary, orthogonal and symplectic groups in terms of what is now called the Weingarten function.

The survey of Collins, Matsumoto and Novak, The Weingarten Calculus (arXiv:2109.14890), isolates the single statement underneath all these formulas, valid for every compact group and every finite-dimensional unitary representation. This mission formalizes that statement, Theorem 2.1 of the survey, together with the steps of its proof as written in Section 2.

Setting

Let $G$ be a compact Hausdorff topological group and $\mu$ its Haar probability measure, the unique Borel probability measure on $G$ invariant under left translation. Let $H=\mathbb{C}^N$ with its standard orthonormal basis $e_1,\dots,e_N$, and let $U:G\to\mathrm U(N)$ be a continuous group homomorphism into the unitary $N\times N$ matrices. Its matrix elements are $U_{xy}(g)=\langle e_x,U(g)e_y\rangle$, the $(x,y)$ entry of $U(g)$.

Fix $d\in\mathbb N$. A multi-index is a function $i:[d]\to[N]$; the set of them is $\mathrm{Fun}(d,N)$. The Weingarten integrals of degree $d$ are

$$I_{ij}=\int_G\prod_{x=1}^d U_{i(x)j(x)}(g)\,d\mu(g),\qquad i,j\in\mathrm{Fun}(d,N).$$

The tensor power $H^{\otimes d}$ has the orthonormal basis $e_i=e_{i(1)}\otimes\cdots\otimes e_{i(d)}$, and the tensor-power matrix $U^{\otimes d}(g)$ has entries $U^{\otimes d}_{ij}(g)=\prod_{x=1}^dU_{i(x)j(x)}(g)$. The invariant tensors are

$$(H^{\otimes d})^G=\{t\in H^{\otimes d}: U^{\otimes d}(g)\,t=t\ \text{for all }g\in G\},$$

and the Haar average is the matrix $P=\int_GU^{\otimes d}(g)\,d\mu(g)$. Given vectors $a_1,\dots,a_m\in H^{\otimes d}$, let $A=[\langle e_i,a_x\rangle]$ be the $N^d\times m$ matrix whose columns are their coordinates, $A^*$ its conjugate transpose, $A^*A=[\langle a_x,a_y\rangle]$ their Gram matrix, and, when it is invertible, $W=(A^*A)^{-1}$ the Weingarten matrix of $a_1,\dots,a_m$.

Formalization targets

Goal: Theorem 2.1 (p. 4)

If $a_1,\dots,a_m$ is a basis of $(H^{\otimes d})^G$, then for all $i,j\in\mathrm{Fun}(d,N)$

$$I_{ij}=\sum_{x,y=1}^mA_{ix}\,W_{xy}\,A^*_{yj}.$$

The identity is exact and holds for every compact group, every continuous unitary representation, every degree $d$ and every choice of basis; nothing is fixed beyond the data.

Milestones (Section 2, pp. 3–4)

1. $I_{ij}=P_{ij}$: the Weingarten integrals are the matrix elements of the Haar average.
2. $P^*=P$, $P^2=P$, and $\operatorname{im}P=(H^{\otimes d})^G$: $P$ is the orthogonal projection onto the invariant tensors (the existing platform theorem that a Haar average of a compact group representation is an idempotent fixing exactly the invariant vectors is included as a supporting reference item).
3. For linearly independent columns, the selfadjoint idempotent with image $\operatorname{span}\{a_x\}$ is $A(A^*A)^{-1}A^*$.

Significance

Theorem 2.1 reduces a family of analytic problems — Haar integrals of polynomials in matrix entries — to two algebraic ones: find a basis of the invariant tensors of $G$ in $H^{\otimes d}$ (classical invariant theory), and invert its Gram matrix. For $U(N)$ the invariants come from Schur–Weyl duality and the Weingarten matrix becomes the Weingarten function on permutations; for $O(N)$ and $Sp(N)$ the invariants are indexed by pair partitions; for the symmetric group $S(N)$ acting by permutation matrices the invariants are indicators of set partitions. Each of these case-specific formulas, surveyed in Sections 3–5 of the paper, is an instance of Theorem 2.1, so a formal proof of the theorem is the common entry point for formalizing any of them.

The theorem is classical and its proof is elementary once stated; it is not open. No machine-checked proof is known to exist in Mathlib or on this platform: Mathlib has Haar measure, unitary groups and Gram matrices (including the equivalence of linear independence with invertibility of the Gram matrix), but not the averaging projection of a representation in matrix form nor the formula $A(A^*A)^{-1}A^*$ for orthogonal projections. The mission produces both as reusable lemmas and the Fundamental Theorem itself.

Difficulty

The argument is short on paper; the formal work sits in three places. First, selfadjointness of $P$ needs $\int_GF(g^{-1})\,d\mu=\int_GF(g)\,d\mu$, i.e. unimodularity of a compact group, which Mathlib does not provide as an instance for non-commutative groups. Second, identifying the image of $P$ with the invariant tensors needs both directions: invariant vectors are fixed by $P$, and every vector $Pt$ is invariant, which uses left invariance of $\mu$ inside a matrix-valued Bochner integral. Third, the projection formula needs invertibility of $A^*A$ from linear independence and an argument that a selfadjoint idempotent is determined by its image. Commuting the integral with matrix entries and products is routine but must be done with care for the matrix norm chosen.

Formalization scope

• $H$ is $\mathbb C^N$ with its standard basis (a finite-dimensional Hilbert space with a specified orthonormal basis is the same thing after identification); $U$ is a monoid homomorphism G →* Matrix.unitaryGroup (Fin N) ℂ, assumed continuous. Indices are 0-based: $[N]$ is Fin N, multi-indices are Fin d → Fin N, tensors are (Fin d → Fin N) → ℂ.
• $G$ carries [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [BorelSpace G], and $\mu$ is a Haar measure that is a probability measure. Right invariance is not assumed; it is a consequence that solvers must prove.
• $d$ ranges over all of $\mathbb N$, including $d=0$, where both sides equal $1$; the paper takes $d$ positive.
• The inner product is conjugate-linear in the first slot, so $A^*_{yj}=\overline{A_{jy}}$ and $A^*$ is Mathlib's conjugate transpose.
• $P$ is a Bochner integral of matrices, taken with the entrywise sup norm; in finite dimension the integral is independent of the norm.
• The basis hypothesis is two hypotheses: LinearIndependent ℂ a and span (range a) = invariants U d, with the invariant subspace defined from the representation. Without independence Mathlib's matrix inverse returns $0$ on a singular Gram matrix, and the statement would be false; it is therefore not a trivializing gap but a necessary hypothesis.
• Correction. The paper says "a basis $a_1,\dots,a_m$ of $(H)^{\otimes d}$"; the same paragraph calls the $a_x$ "the basic invariants", and with a basis of all of $H^{\otimes d}$ the right-hand side would be the identity. The formal statement uses a basis of $(H^{\otimes d})^G$.
• A trivializing formalization — defining the Weingarten integral as $AWA^*$, defining the invariant space as the image of $P$, or assuming that $P$ projects onto the span of the $a_x$ — is excluded: the left side is the Haar integral of the product of matrix elements written out, and the invariant space is defined by $U^{\otimes d}(g)t=t$.

Needed infrastructure: matrix-valued Bochner integrals commuting with entries and with matrix multiplication; unimodularity of compact groups; the orthogonal-projection formula. All three are reusable well beyond this mission, and contributions of these general lemmas are welcome.

Selected references

• B. Collins, S. Matsumoto, J. Novak, The Weingarten Calculus, arXiv preprint, 2021. https://arxiv.org/abs/2109.14890
• D. Weingarten, Asymptotic behavior of group integrals in the limit of infinite rank, J. Math. Phys. 19 (1978), 999–1001. https://doi.org/10.1063/1.523807
• B. Collins, Moments and cumulants of polynomial random variables on unitary groups, the Itzykson–Zuber integral, and free probability, Int. Math. Res. Not. 2003, no. 17, 953–982. https://doi.org/10.1155/S107379280320917X
• B. Collins, P. Śniady, Integration with respect to the Haar measure on unitary, orthogonal and symplectic group, Comm. Math. Phys. 264 (2006), 773–795. https://doi.org/10.1007/s00220-006-1554-3