Documentation

TauCeti.Combinatorics.Brauer.TwoStrands

The Brauer diagrams on at most two strands #

On few strands the Brauer diagrams can be listed. This file lists them, and reads off the multiplication table that the loop-weighted stacking of TauCeti/Combinatorics/Brauer/Compose.lean and TauCeti/Combinatorics/Brauer/LoopCount.lean gives them.

What decides the list is the count TauCeti.card_brauerDiagram: there are (2 * k - 1)‼ Brauer diagrams on k strands. On k ≤ 1 strands that count is 1, so the identity diagram is the only diagram (TauCeti.BrauerDiagram.eq_permToBrauer_one_of_le_one). On two strands it is 3, and the three diagrams

1 (two through strands), s (the crossing), and e (the cap on the bottom together with the cup on the top),

are pairwise distinct, hence all of them (TauCeti.BrauerDiagram.univ_two and TauCeti.BrauerDiagram.eq_permToBrauer_one_or_eq_permToBrauer_swap_or_eq_capCup).

Their nine products are then Brauer's relations for B₂(δ). On the diagram basis 1 is a two-sided identity, s composed with itself is 1, and e absorbs every diagram from either side (TauCeti.composeDiagram_capCup_left_two and TauCeti.composeDiagram_capCup_right_two). The loop-weighted multiplication D₁ * D₂ = δ ^ middleLoopCount D₁ D₂ • composeDiagram D₁ D₂ of B₂(δ) differs from that stacking for the product of e with itself alone, where exactly one loop closes up in the middle (TauCeti.middleLoopCount_two). So the relations of B₂(δ) read s * s = 1, s * e = e = e * s and e * e = δ • e.

Main results #

References #

At most one strand #

source
theorem TauCeti.BrauerDiagram.eq_permToBrauer_one_of_le_one {k : ℕ} (D : BrauerDiagram k) (hk : k ≤ 1) :
D = permToBrauer 1

On at most one strand the identity diagram is the only Brauer diagram.

Two strands #

source
theorem TauCeti.BrauerDiagram.univ_two :
Finset.univ = {permToBrauer 1, permToBrauer (Equiv.swap 0 1), capCup 0 1}

The enumeration of the Brauer diagrams on two strands: the identity diagram, the crossing and the cap-cup diagram, which are three in number as TauCeti.card_brauerDiagram asks.

source
theorem TauCeti.BrauerDiagram.eq_permToBrauer_one_or_eq_permToBrauer_swap_or_eq_capCup (D : BrauerDiagram 2) :
D = permToBrauer 1 ∨ D = permToBrauer (Equiv.swap 0 1) ∨ D = capCup 0 1

The three Brauer diagrams on two strands: the identity diagram, the crossing, and the cap-cup diagram.

The multiplication table on two strands #

source
@[simp]
theorem TauCeti.composeDiagram_capCup_left_two (D : BrauerDiagram 2) :
composeDiagram (capCup 0 1) D = capCup 0 1

The cap-cup diagram absorbs on the left: on two strands, stacking any diagram underneath e gives e back.

source
@[simp]
theorem TauCeti.composeDiagram_capCup_right_two (D : BrauerDiagram 2) :
composeDiagram D (capCup 0 1) = capCup 0 1

The cap-cup diagram absorbs on the right: on two strands, stacking any diagram above e gives e back.

source
@[simp]
theorem TauCeti.middleLoopCount_two (D₁ D₂ : BrauerDiagram 2) :
middleLoopCount D₁ D₂ = if D₁ = capCup 0 1 ∧ D₂ = capCup 0 1 then 1 else 0

The loop rule on two strands: the only product of Brauer diagrams on two strands that closes a loop up in the middle is e * e, which closes exactly one. So the loop-weighted multiplication of B₂(δ) is the stacking of diagrams with the single correction e * e = δ • e.

The four products of permutation diagrams complete the table. They are instances of TauCeti.composeDiagram_permToBrauer, so no name is claimed for them; what the examples record is that the general relations do assemble into the table of B₂(δ), with 1 a two-sided identity and s * s = 1.