Generators of the Brauer algebra

The Brauer algebra B_k(δ) is generated, as an R-algebra, by the permutation diagrams together with a single cap-cup diagram e = TauCeti.capCup a b on two distinct strands (TauCeti.BrauerAlgebra.adjoin_insert_of_capCup_range_of_permToBrauer). Since the symmetric group is generated by the adjacent transpositions sᵢ, taking a, b adjacent recovers Brauer's classical generators s₁, …, s_{k-1} and e; the statements here use all the permutation diagrams. So an algebra map out of B_k(δ) is determined by its restriction to the symmetric group and its value on e (TauCeti.BrauerAlgebra.algHom_ext_of_capCup). This is how an action of the Brauer algebra is matched against the operators it is built from: on tensor powers, the permutations of the tensor factors and a single contraction-expansion of two slots.

The proof has two steps.

• Every diagram is a loop-free stack of cap-cup diagrams above a permutation diagram (TauCeti.BrauerDiagram.capCup_induction_on), and in the Brauer algebra a stack that closes up no loop is the product of its two diagrams (TauCeti.BrauerAlgebra.of_mul_of_of_middleLoopCount_eq_zero). Since the diagrams form a basis, the permutation diagrams and all the cap-cup diagrams generate the algebra (TauCeti.BrauerAlgebra.adjoin_range_of_permToBrauer_union_range_of_capCup).
• Conjugating a cap-cup diagram by a permutation diagram renames its pair (TauCeti.BrauerAlgebra.of_permToBrauer_mul_of_capCup_mul_of_permToBrauer_inv), and any pair of distinct strands is carried to any other by some permutation, so one cap-cup diagram suffices.

Main results

• TauCeti.BrauerAlgebra.adjoin_range_of_permToBrauer_union_range_of_capCup: the permutation diagrams and the cap-cup diagrams generate the Brauer algebra.
• TauCeti.BrauerAlgebra.adjoin_insert_of_capCup_range_of_permToBrauer: the permutation diagrams and one cap-cup diagram generate the Brauer algebra.
• TauCeti.BrauerAlgebra.algHom_ext_of_capCup: an algebra map out of the Brauer algebra is determined by its values on the permutation diagrams and on one cap-cup diagram.

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.BrauerAlgebra.adjoin_range_of_permToBrauer_union_range_of_capCup (R : Type u_1) [CommSemiring R] (δ : R) (k : ℕ) : Algebra.adjoin R ((Set.range fun (σ : Equiv.Perm (Fin k)) => of (permToBrauer σ)) ∪ Set.range fun (p : Fin k × Fin k) => of (capCup p.1 p.2)) = ⊤

The permutation diagrams and the cap-cup diagrams generate the Brauer algebra.

theorem TauCeti.BrauerAlgebra.adjoin_insert_of_capCup_range_of_permToBrauer (R : Type u_1) [CommSemiring R] (δ : R) {k : ℕ} {a b : Fin k} (hab : a ≠ b) : Algebra.adjoin R (insert (of (capCup a b)) (Set.range fun (σ : Equiv.Perm (Fin k)) => of (permToBrauer σ))) = ⊤

The permutation diagrams and one cap-cup diagram generate the Brauer algebra: the cap-cup diagram e = capCup a b on any two distinct strands, together with the permutation diagrams, generates B_k(δ) as an R-algebra.

theorem TauCeti.BrauerAlgebra.algHom_ext_of_capCup {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} {A : Type u_2} [Semiring A] [Algebra R A] {f g : BrauerAlgebra R δ k →ₐ[R] A} {a b : Fin k} (hab : a ≠ b) (hperm : ∀ (σ : Equiv.Perm (Fin k)), f (of (permToBrauer σ)) = g (of (permToBrauer σ))) (hcapCup : f (of (capCup a b)) = g (of (capCup a b))) : f = g

An algebra map out of the Brauer algebra is determined by its values on the permutation diagrams and on one cap-cup diagram on two distinct strands.