The Brauer algebra acting on a tensor power of Rⁿ

Equip V = Rⁿ with its standard symmetric bilinear form, the coordinate dot product, whose copairing is ∑ c, e_c ⊗ e_c. A Brauer diagram D on k strands acts on the tensor power V^{⊗k}: its through strands carry tensor slots from the bottom to the top, its caps contract two input slots against the form, and its cups insert the copairing into two output slots. In the monomial basis TauCeti.tensorPowerBasis the coefficient of the output basis tensor e_v in the image of the input basis tensor e_u is 1 when the labelling Sum.elim u v of the boundary points of D is constant on its arcs, and 0 otherwise (TauCeti.BrauerDiagram.orthogonalActionMatrix).

These operators multiply by the loop rule of the Brauer algebra at the loop value δ = n, a closed loop evaluating to the trace n of the form (TauCeti.BrauerDiagram.orthogonalActionMatrix_mul, which rests on the count TauCeti.BrauerDiagram.natCard_middleLabelling), so they assemble into an algebra map TauCeti.brauerActionOrth from the Brauer algebra B_k(n) to the endomorphisms of V^{⊗k}. It extends the two families of generators already available: on a permutation diagram it is the permutation action TauCeti.permTensorAction of Sₖ on the tensor factors, so it restricts along TauCeti.BrauerAlgebra.ofPerm to the group-algebra action TauCeti.permTensorActionAlgHom; and on the cap-cup diagram on two distinct strands it is the single-arc generator TauCeti.orthogonalCupCapAt.

This is the action through which the Brauer algebra is the partner of the orthogonal group in Schur-Weyl duality: over ℂ (more generally, over an algebraically closed field of characteristic zero), its image is the commutant of the diagonal action of the form-orthogonal group of V (Brauer's theorem). That theorem does not hold over an arbitrary commutative semiring, and it is not part of this file.

Main definitions

• TauCeti.BrauerDiagram.orthogonalActionMatrix: the matrix of a Brauer diagram acting on the tensor power of ι → R, indexed by the labellings of the strands.
• TauCeti.brauerActionOrth: the action of the Brauer algebra B_k(n) on (Rⁿ)^{⊗k}.

Main results

• TauCeti.BrauerDiagram.orthogonalActionMatrix_mul: the loop rule for the matrices, M(D₁) * M(D₂) = |ι| ^ c • M(D₁ ∘ D₂) with c the number of closed middle loops.
• TauCeti.BrauerDiagram.transpose_orthogonalActionMatrix and TauCeti.BrauerDiagram.conjTranspose_orthogonalActionMatrix: the transpose of the matrix of a diagram, and also its conjugate transpose, is the matrix of the reflected diagram.
• TauCeti.toMatrix_brauerActionOrth: an element of the Brauer algebra acts by the combination of the matrices of the diagrams with its coefficients.
• TauCeti.brauerActionOrth_of_tensorPowerBasis: a diagram sends a monomial basis tensor to the sum of the basis tensors whose labels, together with those of the input, are constant on its arcs.
• TauCeti.brauerActionOrth_of_permToBrauer and TauCeti.brauerActionOrth_comp_ofPerm: on the permutation diagrams the action is the permutation action of the symmetric group.
• TauCeti.brauerActionOrth_of_capCup: on a cap-cup diagram the action is the single-arc generator TauCeti.orthogonalCupCapAt.
• TauCeti.range_brauerActionOrth_eq_adjoin: the image of the Brauer algebra is the subalgebra generated by the permutations of the tensor factors and one single-arc generator, so an operator lies in the commutant of the image exactly when it commutes with those generators.

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.

def TauCeti.BrauerDiagram.orthogonalActionMatrix (R : Type u) [CommSemiring R] (ι : Type u_1) [DecidableEq ι] {k : ℕ} (D : BrauerDiagram k) : Matrix (Fin k → ι) (Fin k → ι) R

The matrix of a Brauer diagram acting on the k-th tensor power of ι → R with its standard symmetric form, in the monomial basis indexed by the labellings Fin k → ι of the strands: the entry in the row of the output labelling v and the column of the input labelling u is 1 when Sum.elim u v is constant on the arcs of D, and 0 otherwise.

@[simp]

theorem TauCeti.BrauerDiagram.orthogonalActionMatrix_apply (R : Type u) [CommSemiring R] (ι : Type u_1) [DecidableEq ι] {k : ℕ} (D : BrauerDiagram k) (v u : Fin k → ι) : orthogonalActionMatrix R ι D v u = if D.IsConstantOnArcs (Sum.elim u v) then 1 else 0

@[simp]

theorem TauCeti.BrauerDiagram.orthogonalActionMatrix_permToBrauer_one (R : Type u) [CommSemiring R] (ι : Type u_1) [DecidableEq ι] {k : ℕ} : orthogonalActionMatrix R ι (permToBrauer 1) = 1

The identity diagram has the identity matrix.

theorem TauCeti.BrauerDiagram.orthogonalActionMatrix_mul (R : Type u) [CommSemiring R] (ι : Type u_1) [DecidableEq ι] {k : ℕ} [Fintype ι] (D₁ D₂ : BrauerDiagram k) : orthogonalActionMatrix R ι D₁ * orthogonalActionMatrix R ι D₂ = ↑(Fintype.card ι) ^ middleLoopCount D₁ D₂ • orthogonalActionMatrix R ι (composeDiagram D₁ D₂)

The loop rule for the matrices of Brauer diagrams. The matrix of D₁ times the matrix of D₂ is the matrix of the composite TauCeti.composeDiagram D₁ D₂, scaled by |ι| to the number of closed middle loops: summing over the labellings of the middle boundary counts the free labels of those loops.

@[simp]

theorem TauCeti.BrauerDiagram.transpose_orthogonalActionMatrix (R : Type u) [CommSemiring R] (ι : Type u_1) [DecidableEq ι] {k : ℕ} (D : BrauerDiagram k) : (orthogonalActionMatrix R ι D).transpose = orthogonalActionMatrix R ι D.flip

Reflecting a diagram transposes its matrix: the reflection D.flip exchanges the bottom and top boundary points, hence the input and output labellings.

@[simp]

theorem TauCeti.BrauerDiagram.conjTranspose_orthogonalActionMatrix (R : Type u) [CommSemiring R] (ι : Type u_1) [DecidableEq ι] {k : ℕ} [StarRing R] (D : BrauerDiagram k) : (orthogonalActionMatrix R ι D).conjTranspose = orthogonalActionMatrix R ι D.flip

The entries of the matrix of a diagram are 0 and 1, which every star structure fixes, so its conjugate transpose is its transpose, the matrix of the reflected diagram.

noncomputable def TauCeti.brauerActionOrth (R : Type u) [CommSemiring R] (n k : ℕ) : BrauerAlgebra R (↑n) k →ₐ[R] Module.End R (PiTensorProduct R fun (x : Fin k) => Fin n → R)

The Brauer algebra acting on a tensor power of Rⁿ. The Brauer algebra B_k(n) at the loop value n = dim Rⁿ acts on (Rⁿ)^{⊗k} through the standard symmetric form: a diagram acts by the matrix TauCeti.BrauerDiagram.orthogonalActionMatrix in the monomial basis, and these matrices obey the loop rule (TauCeti.BrauerDiagram.orthogonalActionMatrix_mul).

theorem TauCeti.brauerActionOrth_of (R : Type u) [CommSemiring R] (n k : ℕ) (D : BrauerDiagram k) : (brauerActionOrth R n k) (BrauerAlgebra.of D) = (Matrix.toLin (tensorPowerBasis R n k) (tensorPowerBasis R n k)) (BrauerDiagram.orthogonalActionMatrix R (Fin n) D)

A Brauer diagram acts by its matrix in the monomial basis.

theorem TauCeti.toMatrix_brauerActionOrth (R : Type u) [CommSemiring R] (n k : ℕ) (x : BrauerAlgebra R (↑n) k) : (LinearMap.toMatrix (tensorPowerBasis R n k) (tensorPowerBasis R n k)) ((brauerActionOrth R n k) x) = (Finsupp.linearCombination R fun (D : BrauerDiagram k) => BrauerDiagram.orthogonalActionMatrix R (Fin n) D) x.coeff

The matrix of the action. In the monomial basis, an element x of the Brauer algebra acts by the combination ∑ D, x.coeff D • M(D) of the matrices of the diagrams.

theorem TauCeti.brauerActionOrth_of_tensorPowerBasis (R : Type u) [CommSemiring R] (n k : ℕ) (D : BrauerDiagram k) (u : Fin k → Fin n) : ((brauerActionOrth R n k) (BrauerAlgebra.of D)) ((tensorPowerBasis R n k) u) = ∑ v : Fin k → Fin n with D.IsConstantOnArcs (Sum.elim u v), (tensorPowerBasis R n k) v

A Brauer diagram on a monomial basis tensor. The diagram D sends the basis tensor e_u to the sum of the basis tensors e_v for which the labelling Sum.elim u v is constant on the arcs of D.

@[simp]

theorem TauCeti.brauerActionOrth_of_permToBrauer (R : Type u) [CommSemiring R] (n k : ℕ) (σ : Equiv.Perm (Fin k)) : (brauerActionOrth R n k) (BrauerAlgebra.of (permToBrauer σ)) = (permTensorAction R n k) σ

Permutation diagrams act by permuting the tensor factors. The diagram of σ acts on (Rⁿ)^{⊗k} as σ does in the permutation action TauCeti.permTensorAction.

theorem TauCeti.brauerActionOrth_comp_ofPerm (R : Type u) [CommSemiring R] (n k : ℕ) : (brauerActionOrth R n k).comp (BrauerAlgebra.ofPerm R (↑n) k) = permTensorActionAlgHom R n k

The action restricts to the symmetric group. Along the embedding TauCeti.BrauerAlgebra.ofPerm of the group algebra of Sₖ, the action of the Brauer algebra is the action TauCeti.permTensorActionAlgHom of the group algebra by permutations of the tensor factors.

@[simp]

theorem TauCeti.brauerActionOrth_of_capCup (R : Type u) [CommSemiring R] (n k : ℕ) {a b : Fin k} (hab : a ≠ b) : (brauerActionOrth R n k) (BrauerAlgebra.of (capCup a b)) = orthogonalCupCapAt R n k a b

Cap-cup diagrams act by the single-arc generators. On two distinct strands a and b, the cap-cup diagram acts on (Rⁿ)^{⊗k} as the generator TauCeti.orthogonalCupCapAt, contracting the two slots against the dot product and re-expanding them through its copairing.

theorem TauCeti.range_brauerActionOrth_eq_adjoin (R : Type u) [CommSemiring R] (n k : ℕ) {a b : Fin k} (hab : a ≠ b) : (brauerActionOrth R n k).range = Algebra.adjoin R (insert (orthogonalCupCapAt R n k a b) (Set.range ⇑(permTensorAction R n k)))

The image of the Brauer algebra is generated by the permutations and one arc. The image of B_k(n) in the endomorphisms of (Rⁿ)^{⊗k} is the subalgebra generated by the permutations of the tensor factors together with the single-arc generator TauCeti.orthogonalCupCapAt on any two distinct strands, because the Brauer algebra is generated by the permutation diagrams and one cap-cup diagram (TauCeti.BrauerAlgebra.adjoin_insert_of_capCup_range_of_permToBrauer).