Brauer diagrams

A Brauer diagram on k strands is a perfect matching of the 2 * k boundary points Fin k ⊕ Fin k, where Sum.inl i is the i-th bottom point and Sum.inr j the j-th top point; the matched pairs are the arcs of the diagram. Brauer diagrams index a basis of the Brauer algebra B_k(δ), which acts on the k-th tensor power of the defining representation of an orthogonal or symplectic group. The image of that action is the centralizer of the group, but the action is faithful, so that B_k(δ) is itself that centralizer, only when the defining representation is large enough relative to k.

Every boundary point lies on exactly one of three kinds of arc: a through strand, joining a bottom point to a top point; a cap, joining two bottom points; or a cup, joining two top points. The diagrams with no cap and no cup are exactly the diagrams permToBrauer σ of permutations σ : Equiv.Perm (Fin k), so there are k ! of them among the (2 * k - 1)‼ diagrams in all.

Main definitions

• TauCeti.BrauerDiagram k: the Brauer diagrams on k strands.
• TauCeti.BrauerDiagram.IsThrough, IsCap, IsCup: the three kinds of arc.
• TauCeti.permToBrauer: the diagram of a permutation.
• TauCeti.permToBrauerEquiv: permutations are the diagrams all of whose arcs go through.

Main results

• TauCeti.card_brauerDiagram: there are (2 * k - 1)‼ Brauer diagrams on k strands.
• TauCeti.BrauerDiagram.isThrough_or_isCap_or_isCup, together with the three exclusivity lemmas: every boundary point lies on an arc of exactly one of the three kinds.
• TauCeti.card_brauerDiagram_forall_isThrough: there are k ! diagrams all of whose arcs go through.

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.

@[reducible, inline]

abbrev TauCeti.BrauerDiagram (k : ℕ) : Type

A Brauer diagram on k strands: a perfect matching of the 2 * k boundary points Fin k ⊕ Fin k, with Sum.inl i the i-th bottom point and Sum.inr j the j-th top point. The value D.val x is the boundary point that the diagram matches with x.

Equations

• TauCeti.BrauerDiagram k = TauCeti.PerfectMatching (Fin k ⊕ Fin k)

theorem TauCeti.card_brauerDiagram (k : ℕ) : Fintype.card (BrauerDiagram k) = (2 * k - 1).doubleFactorial

The number of Brauer diagrams. There are (2 * k - 1)‼ perfect matchings of the 2 * k boundary points, hence (2 * k - 1)‼ Brauer diagrams on k strands.

def TauCeti.BrauerDiagram.IsThrough {k : ℕ} (D : BrauerDiagram k) (x : Fin k ⊕ Fin k) : Prop

The boundary point x lies on a through strand: it is matched with a point on the opposite boundary.

Equations

• D.IsThrough x = ((↑D x).isLeft ≠ x.isLeft)

def TauCeti.BrauerDiagram.IsCap {k : ℕ} (D : BrauerDiagram k) (x : Fin k ⊕ Fin k) : Prop

The boundary point x lies on a cap: it is a bottom point matched with another bottom point.

Equations

• D.IsCap x = (x.isLeft = true ∧ (↑D x).isLeft = true)

def TauCeti.BrauerDiagram.IsCup {k : ℕ} (D : BrauerDiagram k) (x : Fin k ⊕ Fin k) : Prop

The boundary point x lies on a cup: it is a top point matched with another top point.

Equations

• D.IsCup x = (x.isRight = true ∧ (↑D x).isRight = true)

@[instance_reducible]

instance TauCeti.BrauerDiagram.instDecidableIsThrough {k : ℕ} (D : BrauerDiagram k) (x : Fin k ⊕ Fin k) : Decidable (D.IsThrough x)

Equations

• D.instDecidableIsThrough x = { decide := !decide ((↑D x).isLeft = x.isLeft), reflects_decide := ⋯ }

@[instance_reducible]

instance TauCeti.BrauerDiagram.instDecidableIsCap {k : ℕ} (D : BrauerDiagram k) (x : Fin k ⊕ Fin k) : Decidable (D.IsCap x)

Equations

• D.instDecidableIsCap x = { decide := decide (x.isLeft = true) && decide ((↑D x).isLeft = true), reflects_decide := ⋯ }

@[instance_reducible]

instance TauCeti.BrauerDiagram.instDecidableIsCup {k : ℕ} (D : BrauerDiagram k) (x : Fin k ⊕ Fin k) : Decidable (D.IsCup x)

Equations

• D.instDecidableIsCup x = { decide := decide (x.isRight = true) && decide ((↑D x).isRight = true), reflects_decide := ⋯ }

theorem TauCeti.BrauerDiagram.isThrough_def {k : ℕ} (D : BrauerDiagram k) (x : Fin k ⊕ Fin k) : D.IsThrough x ↔ (↑D x).isLeft ≠ x.isLeft

Lying on a through strand means being matched across the two boundaries.

theorem TauCeti.BrauerDiagram.isCap_def {k : ℕ} (D : BrauerDiagram k) (x : Fin k ⊕ Fin k) : D.IsCap x ↔ x.isLeft = true ∧ (↑D x).isLeft = true

Lying on a cap means being a bottom point matched with a bottom point.

theorem TauCeti.BrauerDiagram.isCup_def {k : ℕ} (D : BrauerDiagram k) (x : Fin k ⊕ Fin k) : D.IsCup x ↔ x.isRight = true ∧ (↑D x).isRight = true

Lying on a cup means being a top point matched with a top point.

theorem TauCeti.BrauerDiagram.isThrough_or_isCap_or_isCup {k : ℕ} (D : BrauerDiagram k) (x : Fin k ⊕ Fin k) : D.IsThrough x ∨ D.IsCap x ∨ D.IsCup x

Every boundary point lies on a through strand, on a cap, or on a cup.

theorem TauCeti.BrauerDiagram.not_isThrough_of_isCap {k : ℕ} (D : BrauerDiagram k) (x : Fin k ⊕ Fin k) (h : D.IsCap x) : ¬D.IsThrough x

A cap is not a through strand.

theorem TauCeti.BrauerDiagram.not_isThrough_of_isCup {k : ℕ} (D : BrauerDiagram k) (x : Fin k ⊕ Fin k) (h : D.IsCup x) : ¬D.IsThrough x

A cup is not a through strand.

theorem TauCeti.BrauerDiagram.not_isCup_of_isCap {k : ℕ} (D : BrauerDiagram k) (x : Fin k ⊕ Fin k) (h : D.IsCap x) : ¬D.IsCup x

A cap is not a cup.

@[simp]

theorem TauCeti.BrauerDiagram.isThrough_val {k : ℕ} (D : BrauerDiagram k) (x : Fin k ⊕ Fin k) : D.IsThrough (↑D x) ↔ D.IsThrough x

Lying on a through strand is a property of the arc, not of the endpoint chosen.

@[simp]

theorem TauCeti.BrauerDiagram.isCap_val {k : ℕ} (D : BrauerDiagram k) (x : Fin k ⊕ Fin k) : D.IsCap (↑D x) ↔ D.IsCap x

Lying on a cap is a property of the arc, not of the endpoint chosen.

@[simp]

theorem TauCeti.BrauerDiagram.isCup_val {k : ℕ} (D : BrauerDiagram k) (x : Fin k ⊕ Fin k) : D.IsCup (↑D x) ↔ D.IsCup x

Lying on a cup is a property of the arc, not of the endpoint chosen.

def TauCeti.permToBrauer {k : ℕ} (σ : Equiv.Perm (Fin k)) : BrauerDiagram k

The permutation diagram of σ, joining the bottom point i to the top point σ i.

Equations

• TauCeti.permToBrauer σ = TauCeti.PerfectMatching.mk ((Equiv.sumComm (Fin k) (Fin k)).trans ((Equiv.symm σ).sumCongr σ)) ⋯ ⋯

@[simp]

theorem TauCeti.BrauerDiagram.permToBrauer_val_inl {k : ℕ} (σ : Equiv.Perm (Fin k)) (i : Fin k) : ↑(permToBrauer σ) (Sum.inl i) = Sum.inr (σ i)

@[simp]

theorem TauCeti.BrauerDiagram.permToBrauer_val_inr {k : ℕ} (σ : Equiv.Perm (Fin k)) (j : Fin k) : ↑(permToBrauer σ) (Sum.inr j) = Sum.inl ((Equiv.symm σ) j)

@[simp]

theorem TauCeti.BrauerDiagram.isThrough_permToBrauer {k : ℕ} (σ : Equiv.Perm (Fin k)) (x : Fin k ⊕ Fin k) : (permToBrauer σ).IsThrough x

A permutation diagram has no cap and no cup: every arc goes through.

theorem TauCeti.BrauerDiagram.isRight_val_inl {k : ℕ} {D : BrauerDiagram k} {i : Fin k} (hi : D.IsThrough (Sum.inl i)) : (↑D (Sum.inl i)).isRight = true

A bottom point on a through strand is matched with a top point.

theorem TauCeti.BrauerDiagram.isLeft_val_inr {k : ℕ} {D : BrauerDiagram k} {j : Fin k} (hj : D.IsThrough (Sum.inr j)) : (↑D (Sum.inr j)).isLeft = true

A top point on a through strand is matched with a bottom point.

noncomputable def TauCeti.BrauerDiagram.throughPerm {k : ℕ} (D : BrauerDiagram k) (hD : ∀ (x : Fin k ⊕ Fin k), D.IsThrough x) : Equiv.Perm (Fin k)

The permutation read off a Brauer diagram all of whose arcs go through: it sends the bottom point i to the top point matched with it.

Equations

• D.throughPerm hD = Equiv.ofBijective (fun (i : Fin k) => (↑D (Sum.inl i)).getRight ⋯) ⋯

@[simp]

theorem TauCeti.BrauerDiagram.throughPerm_apply {k : ℕ} {D : BrauerDiagram k} (hD : ∀ (x : Fin k ⊕ Fin k), D.IsThrough x) (i : Fin k) : (D.throughPerm hD) i = (↑D (Sum.inl i)).getRight ⋯

@[simp]

theorem TauCeti.BrauerDiagram.permToBrauer_throughPerm {k : ℕ} {D : BrauerDiagram k} (hD : ∀ (x : Fin k ⊕ Fin k), D.IsThrough x) : permToBrauer (D.throughPerm hD) = D

The diagram of the permutation read off a through diagram is the diagram itself.

@[simp]

theorem TauCeti.BrauerDiagram.throughPerm_permToBrauer {k : ℕ} (σ : Equiv.Perm (Fin k)) : (permToBrauer σ).throughPerm ⋯ = σ

The permutation read off the diagram of σ is σ.

noncomputable def TauCeti.permToBrauerEquiv (k : ℕ) : Equiv.Perm (Fin k) ≃ { D : BrauerDiagram k // ∀ (x : Fin k ⊕ Fin k), D.IsThrough x }

Permutations are exactly the Brauer diagrams with no horizontal arc.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.permToBrauerEquiv_apply {k : ℕ} (σ : Equiv.Perm (Fin k)) : ↑((permToBrauerEquiv k) σ) = permToBrauer σ

@[simp]

theorem TauCeti.permToBrauerEquiv_symm_apply {k : ℕ} (D : { D : BrauerDiagram k // ∀ (x : Fin k ⊕ Fin k), D.IsThrough x }) : (permToBrauerEquiv k).symm D = (↑D).throughPerm ⋯

theorem TauCeti.card_brauerDiagram_forall_isThrough (k : ℕ) : Fintype.card { D : BrauerDiagram k // ∀ (x : Fin k ⊕ Fin k), D.IsThrough x } = k.factorial

The Brauer diagrams with no cap and no cup are k ! in number.

theorem TauCeti.permToBrauer_injective (k : ℕ) : Function.Injective permToBrauer

The permutation diagram determines the permutation.