The Brauer algebra acts by intertwiners of the orthogonal group

The action TauCeti.brauerActionOrth of the Brauer algebra B_k(n) on the tensor power (Rⁿ)^{⊗k} commutes with the diagonal action g ↦ g^{⊗k} of every matrix g preserving the standard symmetric form, that is, with gᵀ * g = 1. Equivalently, the image of the Brauer algebra lies in the commutant of the orthogonal group acting on the tensor power (TauCeti.range_brauerActionOrth_le_centralizer). This is the easy half of Brauer's Schur-Weyl duality for the orthogonal group; the converse inclusion, the first fundamental theorem of invariant theory for O(n), needs more hypotheses on R and is not part of this file.

The proof works one diagram at a time and does not use generators of the Brauer algebra. In the monomial basis a diagram D acts by the matrix M whose (v, u) entry is 1 when the labelling Sum.elim u v of the 2 * k boundary points is constant on the arcs of D, and g^{⊗k} acts by the Kronecker power K = Matrix.kroneckerPower (Fin k) g with (v, u) entry ∏ i, g (v i) (u i). Conjugating M by K sums, over the labellings m constant on the arcs of D, the product of the entries g (ℓ x) (m x) at all boundary points x, where ℓ is the outer labelling. Such an m is the same as a free choice of one label per arc (TauCeti.BrauerDiagram.isConstantOnArcsEquiv), so the sum factors as a product over the arcs, and the factor of an arc with endpoints x and y is ∑ c, g (ℓ x) c * g (ℓ y) c = (g * gᵀ) (ℓ x) (ℓ y), which is 1 when ℓ x = ℓ y and 0 otherwise (TauCeti.BrauerDiagram.sum_isConstantOnArcs_prod_apply). So K * M * Kᵀ = M, and since also Kᵀ * K = 1 the matrices M and K commute.

Main results

• TauCeti.BrauerDiagram.sum_isConstantOnArcs_prod_apply: the invariance of the arc tensor of a Brauer diagram under a matrix with A * Aᵀ = 1.
• TauCeti.BrauerDiagram.commute_orthogonalActionMatrix_kroneckerPower: the matrix of a Brauer diagram commutes with the Kronecker power of a matrix with Aᵀ * A = 1.
• TauCeti.commute_brauerActionOrth_piTensorProductMap: every element of the Brauer algebra acts by an operator commuting with A^{⊗k} when Aᵀ * A = 1.
• TauCeti.commute_brauerActionOrth_tensorPower and TauCeti.range_brauerActionOrth_le_centralizer: the same for the tensor power of the standard representation of the orthogonal group, packaged as an inclusion of the image of the Brauer algebra in the commutant of the group.

References

• R. Brauer, On algebras which are connected with the semisimple continuous groups, Annals of Mathematics 38 (1937), 857-872.
• R. Goodman and N. R. Wallach, Symmetry, Representations, and Invariants, Springer GTM 255 (2009), §10.1.

theorem TauCeti.BrauerDiagram.sum_isConstantOnArcs_prod_apply {k : ℕ} {R : Type u} [CommSemiring R] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (D : BrauerDiagram k) {A : Matrix ι ι R} (hA : A * A.transpose = 1) (ℓ : Fin k ⊕ Fin k → ι) : ∑ m : Fin k ⊕ Fin k → ι with D.IsConstantOnArcs m, ∏ x : Fin k ⊕ Fin k, A (ℓ x) (m x) = if D.IsConstantOnArcs ℓ then 1 else 0

The arc tensor of a Brauer diagram is invariant. For a matrix A with A * Aᵀ = 1, summing the products ∏ x, A (ℓ x) (m x) over the labellings m of the boundary points constant on the arcs of D gives 1 when the labelling ℓ is itself constant on the arcs of D, and 0 otherwise. In other words, the tensor ∑ m, e_m over those labellings, the product over the arcs of the copairing ∑ c, e_c ⊗ e_c, is fixed by A acting on every boundary point.

theorem TauCeti.BrauerDiagram.commute_orthogonalActionMatrix_kroneckerPower {k : ℕ} {R : Type u} [CommSemiring R] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (D : BrauerDiagram k) {A : Matrix ι ι R} (hA : A.transpose * A = 1) : Commute (orthogonalActionMatrix R ι D) (Matrix.kroneckerPower (Fin k) A)

The matrix of a Brauer diagram commutes with orthogonal matrices. For a matrix A with Aᵀ * A = 1, the matrix TauCeti.BrauerDiagram.orthogonalActionMatrix of D commutes with the Kronecker power of A, the matrix of A acting diagonally on the k-th tensor power.

theorem TauCeti.commute_brauerActionOrth_piTensorProductMap (R : Type u) (n k : ℕ) [CommSemiring R] (x : BrauerAlgebra R (↑n) k) {A : Matrix (Fin n) (Fin n) R} (hA : A.transpose * A = 1) : Commute ((brauerActionOrth R n k) x) (PiTensorProduct.map fun (x : Fin k) => A.mulVecLin)

The Brauer algebra commutes with orthogonal matrices. Every element of the Brauer algebra B_k(n) acts on (Rⁿ)^{⊗k} by an operator commuting with the diagonal action of each matrix A with Aᵀ * A = 1.

theorem TauCeti.commute_brauerActionOrth_tensorPower (R : Type u) (n k : ℕ) [CommRing R] (x : BrauerAlgebra R (↑n) k) (g : ↥(Matrix.orthogonalGroup (Fin n) R)) : Commute ((brauerActionOrth R n k) x) (((stdOrthogonalRep R n).tensorPower k) g)

The Brauer algebra acts by intertwiners of the orthogonal group. Every element of the Brauer algebra B_k(n) acts on (Rⁿ)^{⊗k} by an operator commuting with the tensor power of the standard representation of the orthogonal group.

theorem TauCeti.range_brauerActionOrth_le_centralizer (R : Type u) (n k : ℕ) [CommRing R] : (brauerActionOrth R n k).range ≤ Subalgebra.centralizer R (Set.range ⇑((stdOrthogonalRep R n).tensorPower k))

The image of the Brauer algebra lies in the commutant of the orthogonal group acting on the tensor power (Rⁿ)^{⊗k}.