Stacking Brauer diagrams is associative

Vertical stacking of Brauer diagrams, TauCeti.composeDiagram, is associative: stacking D₁ above D₂ and the result above D₃ gives the same matching of the outer boundary as stacking D₂ above D₃ and D₁ above that. This is the underlying-matching half of the associativity of the Brauer algebra, whose multiplication is the composite diagram weighted by δ raised to the middle-loop count of TauCeti/Combinatorics/Brauer/LoopCount.lean.

Associativity is what makes the stacking of diagrams the multiplication of an associative algebra, so it is the law every consumer of the Brauer algebra rests on.

Main results

• TauCeti.composeDiagram_assoc: stacking Brauer diagrams is associative.

References

• R. Brauer, On algebras which are connected with the semisimple continuous groups, Annals of Mathematics 38 (1937), 857-872.

The walk along a strand of a stack of two diagrams

The walk along a strand of a stack of three diagrams

The upper two diagrams inside the three-fold stack

The lower two diagrams inside the three-fold stack

Both bracketings leave the three-fold stack at the same point

theorem TauCeti.composeDiagram_assoc {k : ℕ} (D₁ D₂ D₃ : BrauerDiagram k) : composeDiagram (composeDiagram D₁ D₂) D₃ = composeDiagram D₁ (composeDiagram D₂ D₃)

Stacking Brauer diagrams is associative. Stacking D₁ above D₂ and the composite above D₃ matches the outer boundary in the same way as stacking D₂ above D₃ and D₁ above that.