The middle loops of a stack of two Brauer diagrams

Stacking the Brauer diagram D₁ above D₂ identifies the bottom boundary of D₁ with the top boundary of D₂; the arcs of the two diagrams that meet that middle boundary form strands, and TauCeti.composeDiagram reads off the matching those strands induce on the outer boundary. Some of the arcs do not reach the outer boundary at all: they close up into loops in the middle. The multiplication of the Brauer algebra on the diagram basis is the composite diagram weighted by δ raised to the number of those loops, so that number is what this file counts.

Both arcs at a middle point a -- the arc of D₁ at its bottom point a, and the arc of D₂ at its top point a -- stay in the middle exactly when the first is a cap of D₁ and the second a cup of D₂ (TauCeti.IsMiddleVertex). Joining two middle points whenever an arc of either kind runs between them gives a graph on the middle boundary (TauCeti.MiddleAdj) in which every point carries at most one arc of each diagram, so a connected component all of whose points carry both is a cycle: a closed middle loop. That is the definition used here: TauCeti.OnMiddleLoop says that every point reachable from a carries both of its arcs, and TauCeti.middleLoopCount counts the loops by counting their least points.

The count is honest in both directions. It is positive as soon as a cap of D₁ and a cup of D₂ join the same pair of middle points (TauCeti.middleLoopCount_pos_of_val_eq), which is the loop that makes the Brauer generator e satisfy e * e = δ • e; and it vanishes when either diagram is a permutation diagram (TauCeti.middleLoopCount_permToBrauer_left and TauCeti.middleLoopCount_permToBrauer_right), which is why the loop-weighted multiplication will restrict along TauCeti.permToBrauer to the group algebra of the symmetric group. Loops are also disjoint from the strands that TauCeti.composeDiagram reads: no strand starting at the outer boundary ever visits a point of a middle loop (TauCeti.not_onMiddleLoop_of_reflTransGen_stackStep), so the composite diagram and the loop count are independent pieces of the same multiplication.

Main definitions

• TauCeti.MiddleAdj: the middle graph of the stack of D₁ above D₂.
• TauCeti.IsMiddleVertex: both arcs at a middle point stay in the middle.
• TauCeti.OnMiddleLoop: a middle point lies on a closed middle loop.
• TauCeti.middleLoopCount: the number of closed middle loops, the exponent of δ in the loop rule of the Brauer algebra.

Main results

• TauCeti.middleLoopCount_eq_zero_iff: the count vanishes exactly when no middle point lies on a loop.
• TauCeti.middleLoopCount_pos_of_val_eq: a cap of D₁ and a cup of D₂ on the same pair of middle points close up into a loop.
• TauCeti.middleLoopCount_permToBrauer_left, TauCeti.middleLoopCount_permToBrauer_right: stacking with a permutation diagram creates no loop.
• TauCeti.two_mul_middleLoopCount_le: a loop uses at least two of the k middle points, so there are at most k / 2 loops.
• TauCeti.not_onMiddleLoop_of_reflTransGen_stackStep: a strand of the stack never visits a point of a middle loop.

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.middlePoint {k : ℕ} : Fin k ⊕ Fin k → Fin k

The middle point at which a boundary point of one of the two stacked diagrams sits, read off by forgetting which of the two boundaries it lies on. Applied to a middle state of TauCeti.stackStep it is the middle point the strand has reached.

Equations

• TauCeti.middlePoint = Sum.elim id id

@[simp]

theorem TauCeti.middlePoint_inl {k : ℕ} (a : Fin k) : middlePoint (Sum.inl a) = a

The middle point of a bottom boundary point is its index.

@[simp]

theorem TauCeti.middlePoint_inr {k : ℕ} (a : Fin k) : middlePoint (Sum.inr a) = a

The middle point of a top boundary point is its index.

def TauCeti.MiddleAdj {k : ℕ} (D₁ D₂ : BrauerDiagram k) (a b : Fin k) : Prop

The middle graph of a stack. Two points a and b of the middle boundary of the stack of D₁ above D₂ are adjacent when a cap of D₁ or a cup of D₂ joins them: an arc that stays in the middle instead of running out to the outer boundary.

Equations

• TauCeti.MiddleAdj D₁ D₂ a b = (↑D₁ (Sum.inl a) = Sum.inl b ∨ ↑D₂ (Sum.inr a) = Sum.inr b)

theorem TauCeti.middleAdj_def {k : ℕ} (D₁ D₂ : BrauerDiagram k) (a b : Fin k) : MiddleAdj D₁ D₂ a b ↔ ↑D₁ (Sum.inl a) = Sum.inl b ∨ ↑D₂ (Sum.inr a) = Sum.inr b

Adjacency in the middle graph is a cap of D₁ or a cup of D₂ between the two points.

def TauCeti.IsMiddleVertex {k : ℕ} (D₁ D₂ : BrauerDiagram k) (a : Fin k) : Prop

Both arcs at a middle point stay in the middle: the arc of D₁ at the bottom point a is a cap, and the arc of D₂ at the top point a is a cup. These are exactly the middle points that a strand cannot leave the stack through.

Equations

• TauCeti.IsMiddleVertex D₁ D₂ a = (D₁.IsCap (Sum.inl a) ∧ D₂.IsCup (Sum.inr a))

theorem TauCeti.isMiddleVertex_def {k : ℕ} (D₁ D₂ : BrauerDiagram k) (a : Fin k) : IsMiddleVertex D₁ D₂ a ↔ D₁.IsCap (Sum.inl a) ∧ D₂.IsCup (Sum.inr a)

Keeping both arcs in the middle is being capped by D₁ and cupped by D₂.

def TauCeti.OnMiddleLoop {k : ℕ} (D₁ D₂ : BrauerDiagram k) (a : Fin k) : Prop

A middle point lies on a closed loop of the stack of D₁ above D₂ when every middle point reachable from it in the middle graph keeps both of its arcs in the middle. Each point of the middle graph carries at most one arc of D₁ and at most one arc of D₂, so such a connected component is a cycle alternating between caps of D₁ and cups of D₂: a loop that closes up in the middle.

Equations

• TauCeti.OnMiddleLoop D₁ D₂ a = ∀ (b : Fin k), Relation.ReflTransGen (TauCeti.MiddleAdj D₁ D₂) a b → TauCeti.IsMiddleVertex D₁ D₂ b

theorem TauCeti.onMiddleLoop_def {k : ℕ} (D₁ D₂ : BrauerDiagram k) (a : Fin k) : OnMiddleLoop D₁ D₂ a ↔ ∀ (b : Fin k), Relation.ReflTransGen (MiddleAdj D₁ D₂) a b → IsMiddleVertex D₁ D₂ b

Lying on a closed middle loop is every reachable middle point keeping both of its arcs in the middle.

def TauCeti.IsMiddleLoopMin {k : ℕ} (D₁ D₂ : BrauerDiagram k) (a : Fin k) : Prop

a is the least middle point of the closed middle loop it lies on. Each loop has exactly one such point, so these count the loops.

Equations

• TauCeti.IsMiddleLoopMin D₁ D₂ a = (TauCeti.OnMiddleLoop D₁ D₂ a ∧ ∀ (b : Fin k), Relation.ReflTransGen (TauCeti.MiddleAdj D₁ D₂) a b → a ≤ b)

theorem TauCeti.isMiddleLoopMin_def {k : ℕ} (D₁ D₂ : BrauerDiagram k) (a : Fin k) : IsMiddleLoopMin D₁ D₂ a ↔ OnMiddleLoop D₁ D₂ a ∧ ∀ (b : Fin k), Relation.ReflTransGen (MiddleAdj D₁ D₂) a b → a ≤ b

Being the least point of a loop is lying on a loop and being below every reachable point.

noncomputable def TauCeti.middleLoopCount {k : ℕ} (D₁ D₂ : BrauerDiagram k) : ℕ

The middle-loop count of a stack of two Brauer diagrams: the number of loops that close up in the middle when D₁ is stacked above D₂, counted by their least middle points. This is the exponent of δ in the loop rule that weights the multiplication of the Brauer algebra on the diagram basis, D₁ * D₂ = δ ^ middleLoopCount D₁ D₂ • composeDiagram D₁ D₂.

Equations

• TauCeti.middleLoopCount D₁ D₂ = {a : Fin k | TauCeti.IsMiddleLoopMin D₁ D₂ a}.ncard

theorem TauCeti.middleLoopCount_def {k : ℕ} (D₁ D₂ : BrauerDiagram k) : middleLoopCount D₁ D₂ = {a : Fin k | IsMiddleLoopMin D₁ D₂ a}.ncard

The middle-loop count is the number of least points of closed middle loops.

The middle graph

theorem TauCeti.MiddleAdj.symm {k : ℕ} {D₁ D₂ : BrauerDiagram k} {a b : Fin k} (h : MiddleAdj D₁ D₂ a b) : MiddleAdj D₁ D₂ b a

The middle graph is symmetric: an arc joining a to b joins b to a.

theorem TauCeti.MiddleAdj.reflTransGen_symm {k : ℕ} {D₁ D₂ : BrauerDiagram k} {a b : Fin k} (h : Relation.ReflTransGen (MiddleAdj D₁ D₂) a b) : Relation.ReflTransGen (MiddleAdj D₁ D₂) b a

Reachability in the middle graph is symmetric.

theorem TauCeti.BrauerDiagram.val_inl_eq_inl_middlePoint {k : ℕ} {D : BrauerDiagram k} {a : Fin k} (h : D.IsCap (Sum.inl a)) : ↑D (Sum.inl a) = Sum.inl (middlePoint (↑D (Sum.inl a)))

A cap of D₁ at the bottom middle point a lands at the middle point read off its far end, the point BrauerDiagram.capMatching pairs a with.

theorem TauCeti.BrauerDiagram.val_inr_eq_inr_middlePoint {k : ℕ} {D : BrauerDiagram k} {a : Fin k} (h : D.IsCup (Sum.inr a)) : ↑D (Sum.inr a) = Sum.inr (middlePoint (↑D (Sum.inr a)))

A cup of D₂ at the top middle point a lands at the middle point read off its far end, the point BrauerDiagram.cupMatching pairs a with.

Points on a closed middle loop

theorem TauCeti.OnMiddleLoop.isMiddleVertex {k : ℕ} {D₁ D₂ : BrauerDiagram k} {a : Fin k} (h : OnMiddleLoop D₁ D₂ a) : IsMiddleVertex D₁ D₂ a

A point of a closed middle loop keeps both of its arcs in the middle.

theorem TauCeti.OnMiddleLoop.reflTransGen {k : ℕ} {D₁ D₂ : BrauerDiagram k} {a b : Fin k} (ha : OnMiddleLoop D₁ D₂ a) (hab : Relation.ReflTransGen (MiddleAdj D₁ D₂) a b) : OnMiddleLoop D₁ D₂ b

Lying on a closed middle loop is a property of the whole connected component.

theorem TauCeti.OnMiddleLoop.capPartner {k : ℕ} {D₁ D₂ : BrauerDiagram k} {a : Fin k} (h : OnMiddleLoop D₁ D₂ a) : OnMiddleLoop D₁ D₂ (middlePoint (↑D₁ (Sum.inl a)))

The cap of D₁ at a point of a closed middle loop runs to another point of the same loop.

theorem TauCeti.OnMiddleLoop.cupPartner {k : ℕ} {D₁ D₂ : BrauerDiagram k} {a : Fin k} (h : OnMiddleLoop D₁ D₂ a) : OnMiddleLoop D₁ D₂ (middlePoint (↑D₂ (Sum.inr a)))

The cup of D₂ at a point of a closed middle loop runs to another point of the same loop.

theorem TauCeti.OnMiddleLoop.exists_isMiddleLoopMin {k : ℕ} {D₁ D₂ : BrauerDiagram k} {a : Fin k} (ha : OnMiddleLoop D₁ D₂ a) : ∃ (m : Fin k), IsMiddleLoopMin D₁ D₂ m ∧ Relation.ReflTransGen (MiddleAdj D₁ D₂) a m

A loop has a least point. Every point of a closed middle loop reaches the least point of that loop.

The count

theorem TauCeti.middleLoopCount_eq_zero_iff {k : ℕ} {D₁ D₂ : BrauerDiagram k} : middleLoopCount D₁ D₂ = 0 ↔ ∀ (a : Fin k), ¬OnMiddleLoop D₁ D₂ a

No loop, no count. The middle-loop count vanishes exactly when no middle point lies on a closed loop.

theorem TauCeti.middleLoopCount_pos_of_onMiddleLoop {k : ℕ} {D₁ D₂ : BrauerDiagram k} {a : Fin k} (ha : OnMiddleLoop D₁ D₂ a) : 0 < middleLoopCount D₁ D₂

A middle point on a closed loop makes the count positive.

theorem TauCeti.onMiddleLoop_of_val_eq {k : ℕ} {D₁ D₂ : BrauerDiagram k} {a b : Fin k} (h₁ : ↑D₁ (Sum.inl a) = Sum.inl b) (h₂ : ↑D₂ (Sum.inr a) = Sum.inr b) : OnMiddleLoop D₁ D₂ a

A cap of D₁ matching a cup of D₂ closes up into a loop. If the middle points a and b are joined both by a cap of D₁ and by a cup of D₂, then a lies on a closed middle loop, namely the two-point loop {a, b}.

theorem TauCeti.middleLoopCount_pos_of_val_eq {k : ℕ} {D₁ D₂ : BrauerDiagram k} {a b : Fin k} (h₁ : ↑D₁ (Sum.inl a) = Sum.inl b) (h₂ : ↑D₂ (Sum.inr a) = Sum.inr b) : 0 < middleLoopCount D₁ D₂

The two-point loop counts. A cap of D₁ and a cup of D₂ joining the same pair of middle points force at least one closed middle loop. This is the loop behind the Brauer relation e * e = δ • e.

Stacking with a permutation diagram

theorem TauCeti.not_onMiddleLoop_of_isThrough_left {k : ℕ} {D₁ D₂ : BrauerDiagram k} {a : Fin k} (h : D₁.IsThrough (Sum.inl a)) : ¬OnMiddleLoop D₁ D₂ a

A middle point whose arc in D₁ runs through to the outer boundary lies on no middle loop.

theorem TauCeti.not_onMiddleLoop_of_isThrough_right {k : ℕ} {D₁ D₂ : BrauerDiagram k} {a : Fin k} (h : D₂.IsThrough (Sum.inr a)) : ¬OnMiddleLoop D₁ D₂ a

A middle point whose arc in D₂ runs through to the outer boundary lies on no middle loop.

@[simp]

theorem TauCeti.middleLoopCount_permToBrauer_left {k : ℕ} (σ : Equiv.Perm (Fin k)) (D : BrauerDiagram k) : middleLoopCount (permToBrauer σ) D = 0

A permutation diagram on top creates no loop.

@[simp]

theorem TauCeti.middleLoopCount_permToBrauer_right {k : ℕ} (D : BrauerDiagram k) (σ : Equiv.Perm (Fin k)) : middleLoopCount D (permToBrauer σ) = 0

A permutation diagram underneath creates no loop.

How many loops there can be

theorem TauCeti.two_mul_middleLoopCount_le {k : ℕ} (D₁ D₂ : BrauerDiagram k) : 2 * middleLoopCount D₁ D₂ ≤ k

A loop uses at least two middle points, and distinct loops are disjoint, so there are at most k / 2 closed middle loops on k strands.

Loops are disjoint from the strands of the composite

theorem TauCeti.not_onMiddleLoop_of_stackStart {k : ℕ} (D₁ D₂ : BrauerDiagram k) {x s : Fin k ⊕ Fin k} (h : stackStart D₁ D₂ x = Sum.inr s) : ¬OnMiddleLoop D₁ D₂ (middlePoint s)

A strand entering the middle boundary enters at a point off every loop. The first arc of a strand of the stack crosses the middle boundary along a through strand of one of the two diagrams, so the middle point it reaches keeps one of its arcs out of the middle.

theorem TauCeti.onMiddleLoop_of_stackStep {k : ℕ} (D₁ D₂ : BrauerDiagram k) {u v : Fin k ⊕ Fin k} (h : stackStep D₁ D₂ u = Sum.inr v) (hv : OnMiddleLoop D₁ D₂ (middlePoint v)) : OnMiddleLoop D₁ D₂ (middlePoint u)

Loops are closed under following a strand backwards. If the arc continuing a strand from the middle state u stays in the middle, at a middle state v sitting on a loop, then u sits on that same loop.

theorem TauCeti.not_onMiddleLoop_of_reflTransGen_stackStep {k : ℕ} (D₁ D₂ : BrauerDiagram k) {x s t : Fin k ⊕ Fin k} (hstart : stackStart D₁ D₂ x = Sum.inr s) (hpath : Relation.ReflTransGen (fun (u v : Fin k ⊕ Fin k) => stackStep D₁ D₂ u = Sum.inr v) s t) : ¬OnMiddleLoop D₁ D₂ (middlePoint t)

A strand of the stack never visits a middle loop. Following the strand that starts at the outer point x through the middle boundary, every middle state it reaches sits at a middle point off every closed loop. Together with TauCeti.composeDiagram_val_eq_iff, which describes the arcs of the composite by exactly these strands, this is the sense in which the composite diagram and the middle-loop count record disjoint parts of the stack.