Every Brauer diagram is built from cap-cup diagrams and a permutation diagram

A Brauer diagram D with a cap has a cup as well, since it has as many caps as cups. Take a cap of D, joining the bottom points a and b, and a cup, joining the top points c and d. Reconnecting these two arcs into the through strands a–c and b–d gives a diagram X with one cap fewer, X = D.reconnect (Sum.inr c) (Sum.inl a). Stacking the cap-cup diagram TauCeti.capCup c d above X undoes the reconnection: its cup restores the cup c–d, and its cap joins the middle points c and d, where the strands of X from a and from b arrive, so it restores the cap a–b. Every other strand of X passes straight through the cap-cup diagram. No closed loop is formed in the middle, because every middle point lies on a through strand of one of the two diagrams. So

D = capCup c d ∘ X with no middle loop (TauCeti.composeDiagram_capCup_reconnect and TauCeti.middleLoopCount_capCup_reconnect).

Repeating this until no cap is left reaches a diagram without caps, which is a permutation diagram. This gives an induction principle for Brauer diagrams (TauCeti.BrauerDiagram.capCup_induction_on): a property of diagrams that holds for the permutation diagrams, and passes from X to capCup a b ∘ X whenever no loop closes up in the middle, holds for every diagram. In the Brauer algebra, where a loop-free stack is the product, this says that the permutation diagrams and the cap-cup diagrams generate the algebra (TauCeti/Algebra/BrauerAlgebra/Generation.lean).

Main results

• TauCeti.composeDiagram_capCup_reconnect: stacking capCup c d above the reconnected diagram gives back D.
• TauCeti.middleLoopCount_capCup_reconnect: that stack closes up no loop.
• TauCeti.BrauerDiagram.bottomCap_reconnect: the reconnected diagram caps the bottom points of D other than a and b, so it has one cap fewer (TauCeti.BrauerDiagram.card_bottomCap_reconnect).
• TauCeti.BrauerDiagram.capCup_induction_on: induction on Brauer diagrams from the permutation diagrams by stacking cap-cup diagrams on top.

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.

The arcs of the reconnected diagram

theorem TauCeti.BrauerDiagram.bottomCap_reconnect {k : ℕ} {a b c d : Fin k} {D : BrauerDiagram k} (hcap : ↑D (Sum.inl a) = Sum.inl b) (hcup : ↑D (Sum.inr c) = Sum.inr d) : bottomCap (PerfectMatching.reconnect D (Sum.inr c) (Sum.inl a)) = (D.bottomCap.erase a).erase b

The reconnected diagram has one cap fewer: it caps exactly the bottom points capped by D other than a and b.

theorem TauCeti.BrauerDiagram.card_bottomCap_reconnect {k : ℕ} {a b c d : Fin k} {D : BrauerDiagram k} (hcap : ↑D (Sum.inl a) = Sum.inl b) (hcup : ↑D (Sum.inr c) = Sum.inr d) : (bottomCap (PerfectMatching.reconnect D (Sum.inr c) (Sum.inl a))).card + 2 = D.bottomCap.card

The reconnected diagram has two capped bottom points fewer than D.

Undoing the reconnection by a cap-cup diagram

theorem TauCeti.composeDiagram_capCup_reconnect {k : ℕ} {a b c d : Fin k} {D : BrauerDiagram k} (hcap : ↑D (Sum.inl a) = Sum.inl b) (hcup : ↑D (Sum.inr c) = Sum.inr d) : composeDiagram (capCup c d) (PerfectMatching.reconnect D (Sum.inr c) (Sum.inl a)) = D

A cap-cup diagram undoes the reconnection of a cap and a cup. If D caps the bottom points a and b and cups the top points c and d, then stacking capCup c d above the diagram D.reconnect (Sum.inr c) (Sum.inl a), in which these two arcs have become the through strands a–c and b–d, gives back D.

theorem TauCeti.middleLoopCount_capCup_reconnect {k : ℕ} {a b c d : Fin k} {D : BrauerDiagram k} (hcap : ↑D (Sum.inl a) = Sum.inl b) (hcup : ↑D (Sum.inr c) = Sum.inr d) : middleLoopCount (capCup c d) (PerfectMatching.reconnect D (Sum.inr c) (Sum.inl a)) = 0

Undoing the reconnection closes up no loop: every middle point lies on a through strand, of the reconnected diagram at the two middle points c and d of the cap, and of the cap-cup diagram at every other middle point.

Induction on Brauer diagrams

theorem TauCeti.BrauerDiagram.exists_composeDiagram_capCup_eq {k : ℕ} {a : Fin k} {D : BrauerDiagram k} (ha : a ∈ D.bottomCap) : ∃ (c : Fin k) (d : Fin k) (X : BrauerDiagram k), c ≠ d ∧ middleLoopCount (capCup c d) X = 0 ∧ X.bottomCap.card + 2 = D.bottomCap.card ∧ composeDiagram (capCup c d) X = D

A diagram with a cap is a loop-free stack of a cap-cup diagram on a diagram with one cap fewer.

theorem TauCeti.BrauerDiagram.capCup_induction_on {k : ℕ} {motive : BrauerDiagram k → Prop} (D : BrauerDiagram k) (permToBrauer : ∀ (σ : Equiv.Perm (Fin k)), motive (permToBrauer σ)) (capCup_compose : ∀ (a b : Fin k) (X : BrauerDiagram k), a ≠ b → middleLoopCount (capCup a b) X = 0 → motive X → motive (composeDiagram (capCup a b) X)) : motive D

Induction on Brauer diagrams. A property of Brauer diagrams that holds for every permutation diagram, and passes from a diagram X to the stack capCup a b ∘ X of a cap-cup diagram on two distinct strands above it whenever that stack closes up no loop, holds for every Brauer diagram.