The Brauer generators and their relations

Besides the permutation diagrams, the Brauer diagrams on k strands are generated by the cap-cup diagrams: for a pair of distinct indices a ≠ b, the diagram TauCeti.capCup a b whose only horizontal arcs are the cap joining the bottom points a and b and the cup joining the top points a and b, every other boundary point lying on the through strand joining the two points with its index. These are the diagrams written e in Brauer's presentation; the classical generator eᵢ of B_k(δ) is the cap-cup diagram on a pair of consecutive indices, the two indices of Fin k with values i and i + 1 where i + 1 < k — writing that pair as i and i + 1 in Fin k would be wrong at the last index, where the successor wraps back to 0. Nothing below needs the pair to be adjacent, so the pair is arbitrary throughout.

A cap-cup diagram is the identity diagram transported along the transposition that exchanges the top point a with the bottom point b, which bends the two strands ending at a and at b into a cap and a cup. On the degenerate pair a = a that transposition is still a nontrivial exchange of two boundary points, but those two points are the two ends of one and the same strand of the identity diagram, so it carries that strand to itself and leaves the matching unchanged; thus capCup a a is the identity diagram (TauCeti.capCup_self), and the lemmas below carry the distinctness a ≠ b exactly where they need it.

This file builds these diagrams and proves, on the diagram basis, the relations that the loop- weighted multiplication D₁ * D₂ = δ ^ middleLoopCount D₁ D₂ • composeDiagram D₁ D₂ of the Brauer algebra turns into Brauer's relations:

• e * e = δ • e: stacking a cap-cup diagram on itself returns that diagram (TauCeti.composeDiagram_capCup_capCup) and closes up exactly one loop in the middle (TauCeti.middleLoopCount_capCup_capCup), the single loop formed by the cap of the upper copy and the cup of the lower one. This is the relation the loop rule exists for, and the first place a nonzero middle-loop count is computed exactly rather than only bounded below.
• s * e = e = e * s for the transposition s of the pair (TauCeti.composeDiagram_permToBrauer_swap_capCup and TauCeti.composeDiagram_capCup_permToBrauer_swap), with no loop closing up because a permutation diagram has neither a cap nor a cup.
• the far-commutation relation s e = e s for a permutation s renaming the generator to itself (TauCeti.composeDiagram_permToBrauer_capCup_comm): a permutation diagram that does not move {a, b} slides past a cap-cup diagram on {a, b}. It is the case of the unconditional slide TauCeti.composeDiagram_permToBrauer_capCup in which the renaming gives the diagram back.
• the mixed permutation/generator relation σ e_{a,b} σ⁻¹ = e_{σ a, σ b} (TauCeti.composeDiagram_permToBrauer_conj_capCup): conjugating a cap-cup diagram by a permutation diagram moves it to the renamed pair.
• the adjacent mixed relation e s e = e for the transposition s of a point of the pair with a third point (TauCeti.composeDiagram_capCup_permToBrauer_swap_capCup, which holds for every third point, and TauCeti.middleLoopCount_capCup_permToBrauer_swap_capCup, which needs the third point to lie off the pair for no loop to close up).

The Brauer relation s * s = 1 is TauCeti.composeDiagram_permToBrauer together with Equiv.swap_mul_self, and the braid relations are the same lemma applied to the braid relation in Equiv.Perm (Fin k); both are already available on the permutation diagrams and are not restated here.

Main definitions

• TauCeti.capCup: the cap-cup diagram on a pair of indices, the Brauer generator e.

Main results

• TauCeti.eq_capCup_iff: a diagram is capCup a b exactly when it caps a to b, cups a to b and sends every other point through.
• TauCeti.capCup_comm, TauCeti.capCup_eq_capCup_iff: a cap-cup diagram depends exactly on the unordered pair it caps.
• TauCeti.BrauerDiagram.bottomCap_capCup, TauCeti.BrauerDiagram.topCup_capCup: its cap and its cup are the pair, and TauCeti.BrauerDiagram.bottomThrough_capCup, TauCeti.BrauerDiagram.topThrough_capCup: its through strands are the rest.
• TauCeti.capCup_ne_permToBrauer: a cap-cup diagram on a pair of distinct indices is not a permutation diagram.
• TauCeti.composeDiagram_capCup_capCup, TauCeti.middleLoopCount_capCup_capCup: the relation e * e = δ • e.
• TauCeti.composeDiagram_permToBrauer_swap_capCup, TauCeti.composeDiagram_capCup_permToBrauer_swap: the relation s * e = e = e * s.
• TauCeti.composeDiagram_permToBrauer_capCup: a permutation diagram slides past a generator at the cost of renaming its pair, and TauCeti.composeDiagram_permToBrauer_capCup_comm: a permutation diagram preserving the pair commutes with the generator.
• TauCeti.composeDiagram_permToBrauer_conj_capCup: conjugating a generator by a permutation diagram renames its pair.
• TauCeti.composeDiagram_capCup_permToBrauer_swap_capCup, TauCeti.middleLoopCount_capCup_permToBrauer_swap_capCup: the adjacent mixed relation e s e = e.

References

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

def TauCeti.capCup {k : ℕ} (a b : Fin k) : BrauerDiagram k

The cap-cup diagram on the pair {a, b}: the Brauer diagram whose only horizontal arcs are the cap joining the bottom points a and b and the cup joining the top points a and b. It is the Brauer generator e of the pair; the classical generator eᵢ is the case of a consecutive pair, the two indices of Fin k with values i and i + 1 where i + 1 < k.

It is the identity diagram transported along the transposition exchanging the top point a with the bottom point b, which bends the strands ending at a and at b into a cap and a cup. On the degenerate pair a = a that transposition exchanges the two ends of a single identity strand, so it carries that strand to itself and TauCeti.capCup_self gives back the identity diagram.

Equations

• TauCeti.capCup a b = (TauCeti.PerfectMatching.congr (Equiv.swap (Sum.inr a) (Sum.inl b))) (TauCeti.permToBrauer 1)

@[simp]

theorem TauCeti.capCup_self {k : ℕ} (a : Fin k) : capCup a a = permToBrauer 1

A cap-cup diagram on a degenerate pair is the identity diagram: the transposition that transports it exchanges the top point a with the bottom point a, which are the two ends of a single strand of the identity diagram, so it carries that strand to itself and leaves the matching unchanged.

The arcs of a cap-cup diagram

@[simp]

theorem TauCeti.capCup_val_inl_left {k : ℕ} {a b : Fin k} (hab : a ≠ b) : ↑(capCup a b) (Sum.inl a) = Sum.inl b

The cap of capCup a b joins the bottom point a to the bottom point b.

@[simp]

theorem TauCeti.capCup_val_inl_right {k : ℕ} {a b : Fin k} (hab : a ≠ b) : ↑(capCup a b) (Sum.inl b) = Sum.inl a

The cap of capCup a b joins the bottom point b to the bottom point a.

@[simp]

theorem TauCeti.capCup_val_inl_of_ne {k : ℕ} {a b i : Fin k} (hia : i ≠ a) (hib : i ≠ b) : ↑(capCup a b) (Sum.inl i) = Sum.inr i

Away from the capped pair, capCup a b joins the bottom point i to the top point i.

@[simp]

theorem TauCeti.capCup_val_inr_left {k : ℕ} {a b : Fin k} (hab : a ≠ b) : ↑(capCup a b) (Sum.inr a) = Sum.inr b

The cup of capCup a b joins the top point a to the top point b.

@[simp]

theorem TauCeti.capCup_val_inr_right {k : ℕ} {a b : Fin k} (hab : a ≠ b) : ↑(capCup a b) (Sum.inr b) = Sum.inr a

The cup of capCup a b joins the top point b to the top point a.

@[simp]

theorem TauCeti.capCup_val_inr_of_ne {k : ℕ} {a b j : Fin k} (hja : j ≠ a) (hjb : j ≠ b) : ↑(capCup a b) (Sum.inr j) = Sum.inl j

Away from the cupped pair, capCup a b joins the top point j to the bottom point j.

theorem TauCeti.eq_capCup_iff {k : ℕ} {a b : Fin k} {D : BrauerDiagram k} (hab : a ≠ b) : D = capCup a b ↔ ↑D (Sum.inl a) = Sum.inl b ∧ ↑D (Sum.inr a) = Sum.inr b ∧ ∀ (i : Fin k), i ≠ a → i ≠ b → ↑D (Sum.inl i) = Sum.inr i

Recognising a cap-cup diagram: a Brauer diagram is capCup a b exactly when it caps the bottom point a to the bottom point b, cups the top point a to the top point b, and sends every other bottom point through to the top point with the same index. The remaining arcs are then forced, since a perfect matching is determined by the partners it assigns.

@[simp]

theorem TauCeti.BrauerDiagram.isCap_capCup_inl_iff {k : ℕ} {a b i : Fin k} (hab : a ≠ b) : (capCup a b).IsCap (Sum.inl i) ↔ i = a ∨ i = b

A cap-cup diagram caps exactly its pair: a bottom point of capCup a b lies on a cap exactly when it is a or b.

@[simp]

theorem TauCeti.BrauerDiagram.isCup_capCup_inr_iff {k : ℕ} {a b j : Fin k} (hab : a ≠ b) : (capCup a b).IsCup (Sum.inr j) ↔ j = a ∨ j = b

A cap-cup diagram cups exactly its pair: a top point of capCup a b lies on a cup exactly when it is a or b.

@[simp]

theorem TauCeti.BrauerDiagram.isThrough_capCup_inl_iff {k : ℕ} {a b i : Fin k} (hab : a ≠ b) : (capCup a b).IsThrough (Sum.inl i) ↔ i ≠ a ∧ i ≠ b

The through strands of a cap-cup diagram are the ones off its pair, read at the bottom boundary: a bottom point goes through exactly when it does not lie on the cap.

@[simp]

theorem TauCeti.BrauerDiagram.isThrough_capCup_inr_iff {k : ℕ} {a b j : Fin k} (hab : a ≠ b) : (capCup a b).IsThrough (Sum.inr j) ↔ j ≠ a ∧ j ≠ b

The through strands of a cap-cup diagram are the ones off its pair, read at the top boundary: a top point goes through exactly when it does not lie on the cup.

@[simp]

theorem TauCeti.BrauerDiagram.bottomCap_capCup {k : ℕ} {a b : Fin k} (hab : a ≠ b) : (capCup a b).bottomCap = {a, b}

The capped bottom points of capCup a b are a and b.

@[simp]

theorem TauCeti.BrauerDiagram.topCup_capCup {k : ℕ} {a b : Fin k} (hab : a ≠ b) : (capCup a b).topCup = {a, b}

The cupped top points of capCup a b are a and b.

theorem TauCeti.BrauerDiagram.bottomThrough_capCup {k : ℕ} {a b : Fin k} (hab : a ≠ b) : (capCup a b).bottomThrough = {a, b}ᶜ

The bottom endpoints of the through strands of capCup a b are the points off the pair, the complement of its cap.

Not a simp lemma: simp rewrites the complement of a pair further, so the right-hand side is not in simp-normal form.

theorem TauCeti.BrauerDiagram.topThrough_capCup {k : ℕ} {a b : Fin k} (hab : a ≠ b) : (capCup a b).topThrough = {a, b}ᶜ

The top endpoints of the through strands of capCup a b are the points off the pair, the complement of its cup.

Not a simp lemma, for the reason given for TauCeti.BrauerDiagram.bottomThrough_capCup.

@[simp]

theorem TauCeti.capCup_ne_permToBrauer {k : ℕ} {a b : Fin k} (hab : a ≠ b) (σ : Equiv.Perm (Fin k)) : capCup a b ≠ permToBrauer σ

A cap-cup diagram on a pair of distinct indices is not a permutation diagram: it has a cap, and every arc of a permutation diagram goes through.

A cap-cup diagram depends only on the unordered pair

theorem TauCeti.capCup_comm {k : ℕ} (a b : Fin k) : capCup b a = capCup a b

A cap-cup diagram depends only on the unordered pair it caps.

@[simp]

theorem TauCeti.capCup_eq_capCup_iff {k : ℕ} {a b c d : Fin k} (hab : a ≠ b) : capCup a b = capCup c d ↔ a = c ∧ b = d ∨ a = d ∧ b = c

Two cap-cup diagrams agree exactly when they cap the same unordered pair, once one of them is built on a pair of distinct indices.

Relabelling a cap-cup diagram

@[simp]

theorem TauCeti.BrauerDiagram.relabel_capCup {k : ℕ} (a b : Fin k) (σ : Equiv.Perm (Fin k)) : (capCup a b).relabel σ σ = capCup (σ a) (σ b)

Relabelling both boundaries of a cap-cup diagram by the same permutation moves it to the renamed pair: relabelling conjugates the underlying matching by Equiv.Perm.sumCongr σ σ, which carries the transposition that bends the identity diagram into capCup a b to the one that bends it into capCup (σ a) (σ b) and fixes the identity diagram itself.

@[simp]

theorem TauCeti.BrauerDiagram.relabel_one_swap_capCup {k : ℕ} (a b : Fin k) : (capCup a b).relabel 1 (Equiv.swap a b) = capCup a b

Renaming the top boundary by the transposition of the pair fixes a cap-cup diagram: for a ≠ b the cap and the cup of capCup a b are both the pair {a, b}, which the transposition preserves. On the degenerate pair the transposition is trivial (Equiv.swap_self) and the diagram is the identity diagram (TauCeti.capCup_self), so it is fixed for that reason instead.

@[simp]

theorem TauCeti.BrauerDiagram.relabel_swap_one_capCup {k : ℕ} (a b : Fin k) : (capCup a b).relabel (Equiv.swap a b) 1 = capCup a b

Renaming the bottom boundary by the transposition of the pair fixes a cap-cup diagram. Renaming both boundaries renames the pair, which the transposition leaves unordered.

The Brauer relations on the diagram basis

@[simp]

theorem TauCeti.composeDiagram_capCup_capCup {k : ℕ} (a b : Fin k) : composeDiagram (capCup a b) (capCup a b) = capCup a b

The composite of e with itself is e: stacking a cap-cup diagram on itself returns that diagram. Together with TauCeti.middleLoopCount_capCup_capCup, which counts the loop the stack closes up, this is Brauer's relation e * e = δ • e for the loop-weighted multiplication of the diagram basis.

@[simp]

theorem TauCeti.middleLoopCount_capCup_capCup {k : ℕ} {a b : Fin k} (hab : a ≠ b) : middleLoopCount (capCup a b) (capCup a b) = 1

e * e = δ • e, the loop half: stacking a cap-cup diagram on itself closes up exactly one loop in the middle, so the loop-weighted multiplication of the Brauer algebra sends e * e to δ • e.

theorem TauCeti.composeDiagram_permToBrauer_swap_capCup {k : ℕ} (a b : Fin k) : composeDiagram (permToBrauer (Equiv.swap a b)) (capCup a b) = capCup a b

s * e = e on the diagram basis: stacking the diagram of the transposition of the pair above a cap-cup diagram returns that diagram. No loop closes up in the middle (TauCeti.middleLoopCount_permToBrauer_left), so this is Brauer's relation s * e = e.

This and TauCeti.composeDiagram_capCup_permToBrauer_swap are not simp lemmas: simp already reduces their left-hand sides, through TauCeti.composeDiagram_permToBrauer_left and TauCeti.composeDiagram_permToBrauer_right followed by the relabelling lemmas above, so simp proves them and tagging them would leave them out of simp-normal form.

theorem TauCeti.composeDiagram_capCup_permToBrauer_swap {k : ℕ} (a b : Fin k) : composeDiagram (capCup a b) (permToBrauer (Equiv.swap a b)) = capCup a b

e * s = e on the diagram basis: stacking a cap-cup diagram above the diagram of the transposition of its pair returns that diagram. No loop closes up in the middle (TauCeti.middleLoopCount_permToBrauer_right), so this is Brauer's relation e * s = e.

Not a simp lemma, for the reason given for TauCeti.composeDiagram_permToBrauer_swap_capCup.

theorem TauCeti.composeDiagram_permToBrauer_capCup {k : ℕ} (a b : Fin k) (σ : Equiv.Perm (Fin k)) : composeDiagram (permToBrauer σ) (capCup a b) = composeDiagram (capCup (σ a) (σ b)) (permToBrauer σ)

Sliding a permutation diagram past a generator: a permutation diagram moves through a cap-cup diagram from either side at the cost of renaming its pair, with no hypothesis on the permutation. This is the two-factor form of the mixed permutation/generator relation, of which TauCeti.composeDiagram_permToBrauer_capCup_comm is the case where the renaming gives the pair back.

Not a simp lemma: simp reduces both sides, through TauCeti.composeDiagram_permToBrauer_left and TauCeti.composeDiagram_permToBrauer_right, to the two relabellings (capCup a b).relabel 1 σ and (capCup (σ a) (σ b)).relabel σ⁻¹ 1, so neither side is a simp-normal form of the other.

theorem TauCeti.composeDiagram_permToBrauer_capCup_comm {k : ℕ} (a b : Fin k) {σ : Equiv.Perm (Fin k)} (h : capCup (σ a) (σ b) = capCup a b) : composeDiagram (permToBrauer σ) (capCup a b) = composeDiagram (capCup a b) (permToBrauer σ)

Far commutation: a permutation diagram commutes with a cap-cup diagram as soon as it renames that diagram to itself. This is the relation that makes a Brauer generator commute with a distant transposition: for σ a transposition disjoint from {a, b} the hypothesis is discharged by Equiv.swap_apply_of_ne_of_ne, and the conclusion reads s e_{a,b} = e_{a,b} s.

The hypothesis is exactly what the conclusion needs, and is weaker than preserving the ordered or the unordered pair: TauCeti.capCup_comm supplies it from the transposition of the pair itself, TauCeti.capCup_eq_capCup_iff from any permutation preserving {a, b}, and TauCeti.capCup_self supplies it for free on the degenerate pair a = b, where a cap-cup diagram is the identity diagram and commutes with everything.

Not a simp lemma, for the reason given for TauCeti.composeDiagram_permToBrauer_capCup.

theorem TauCeti.composeDiagram_permToBrauer_conj_capCup {k : ℕ} (a b : Fin k) (σ : Equiv.Perm (Fin k)) : composeDiagram (permToBrauer σ) (composeDiagram (capCup a b) (permToBrauer σ⁻¹)) = capCup (σ a) (σ b)

The mixed permutation/generator relation: conjugating a cap-cup diagram by a permutation diagram moves it to the cap-cup diagram on the renamed pair. Taking σ to fix a and b specializes it to σ e_{a,b} σ⁻¹ = e_{a,b}, the conjugated form of the far commutation that TauCeti.composeDiagram_permToBrauer_capCup_comm states with two factors; taking σ to be the transposition of the pair specializes it to s e s⁻¹ = e, which together with TauCeti.composeDiagram_capCup_permToBrauer_swap gives TauCeti.composeDiagram_permToBrauer_swap_capCup.

theorem TauCeti.composeDiagram_capCup_permToBrauer_swap_capCup {k : ℕ} {a b c : Fin k} (hab : a ≠ b) : composeDiagram (capCup a b) (composeDiagram (permToBrauer (Equiv.swap b c)) (capCup a b)) = capCup a b

The adjacent mixed relation e s e = e on the diagram basis: a cap-cup diagram absorbs the diagram of a transposition that exchanges one point of its pair with a third point, when that transposition diagram is stacked between two copies of it. For an adjacent pair this is Brauer's relation eᵢ sᵢ₊₁ eᵢ = eᵢ; nothing needs the pair to be adjacent, so the third point c is arbitrary, and nothing needs it to lie off the pair either: for c = b the transposition diagram is the identity one and for c = a it is absorbed on its own by TauCeti.composeDiagram_permToBrauer_swap_capCup, so either way the composite collapses to TauCeti.composeDiagram_capCup_capCup.

Off the pair, the strand carrying the relation is the one starting at the bottom point c: it runs up the lower composite to the middle point b, back along the cap of the upper copy to a, along the cup of the lower composite to c, and out at the top point c, crossing the middle boundary three times. Together with TauCeti.middleLoopCount_capCup_permToBrauer_swap_capCup and TauCeti.middleLoopCount_permToBrauer_left, which say that no loop closes up in either middle once c lies off the pair, this is the relation e * (s * e) = e for the loop-weighted multiplication of the diagram basis; on the pair the diagrams still compose to e, but the first middle closes up a loop and the relation carries a factor of δ.

Not a simp lemma: simp rewrites the inner composite into a relabelling, through TauCeti.composeDiagram_permToBrauer_left, so the left-hand side is not in simp-normal form.

theorem TauCeti.middleLoopCount_capCup_permToBrauer_swap_capCup {k : ℕ} {a b c : Fin k} (hac : a ≠ c) (hbc : b ≠ c) : middleLoopCount (capCup a b) (composeDiagram (permToBrauer (Equiv.swap b c)) (capCup a b)) = 0

The adjacent mixed relation closes no loop: stacking a cap-cup diagram above the composite of the transposition diagram with that same cap-cup diagram closes up no loop in the middle. The only middle point keeping both of its arcs in the middle is a, since the lower composite cups {a, c} while the upper copy caps {a, b}; the cap of the upper copy runs from a to b, where the arc of the lower composite leaves for the boundary, so a lies on no loop. On the degenerate pair a = b there is no cap at all: the upper copy is the identity diagram (TauCeti.capCup_self), which closes up no loop either.

Not a simp lemma, for the reason given for TauCeti.composeDiagram_capCup_permToBrauer_swap_capCup.