The boundary points of a Brauer diagram

Every boundary point of a Brauer diagram lies on exactly one of a through strand, a cap or a cup. This file sorts the boundary points accordingly -- the bottom and top endpoints of the through strands, the bottom endpoints of the caps and the top endpoints of the cups -- and follows an arc from one of its endpoints to the other.

Following a through strand matches the bottom endpoints of the through strands with their top endpoints (BrauerDiagram.throughEquiv); since the capped bottom points and the cupped top points are the points those two sets leave over, a diagram has as many capped bottom points as cupped top points (BrauerDiagram.card_bottomCap_eq_card_topCup), that is, as many caps as cups. Following a cap instead matches the capped bottom points among themselves (BrauerDiagram.capMatching), so they are even in number; following a cup likewise matches the cupped top points among themselves (BrauerDiagram.cupMatching).

These are the data that vertical stacking consumes: composing D₁ with D₂ identifies the bottom boundary of D₁ with the top boundary of D₂ and reads the arcs of the composite by concatenating through strands (throughEquiv) along that middle boundary. Counting the closed loops that form there, by alternately following the caps of D₁ (capMatching) and the cups of D₂ (cupMatching), is done in TauCeti/Combinatorics/Brauer/LoopCount.lean.

Main definitions

• TauCeti.BrauerDiagram.bottomThrough, topThrough, bottomCap, topCup: the boundary points carrying an arc of each kind.
• TauCeti.BrauerDiagram.throughEquiv: a through strand matches its bottom endpoint with its top endpoint.
• TauCeti.BrauerDiagram.capMatching, TauCeti.BrauerDiagram.cupMatching: the perfect matchings of the capped bottom points and of the cupped top points.

Main results

• TauCeti.BrauerDiagram.card_bottomCap_eq_card_topCup: a diagram has as many capped bottom points as cupped top points, hence as many caps as cups.
• TauCeti.BrauerDiagram.even_card_bottomCap: a diagram has an even number of capped bottom points.
• TauCeti.BrauerDiagram.forall_isThrough_iff_bottomCap_eq_empty, TauCeti.BrauerDiagram.exists_eq_permToBrauer_iff_bottomCap_eq_empty: a diagram is a permutation diagram exactly when it caps no bottom point.

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.

theorem TauCeti.BrauerDiagram.isCap_inl_iff {k : ℕ} (D : BrauerDiagram k) (i : Fin k) : D.IsCap (Sum.inl i) ↔ ¬D.IsThrough (Sum.inl i)

A bottom point lies on a cap exactly when it does not lie on a through strand.

theorem TauCeti.BrauerDiagram.isCup_inr_iff {k : ℕ} (D : BrauerDiagram k) (j : Fin k) : D.IsCup (Sum.inr j) ↔ ¬D.IsThrough (Sum.inr j)

A top point lies on a cup exactly when it does not lie on a through strand.

def TauCeti.BrauerDiagram.bottomThrough {k : ℕ} (D : BrauerDiagram k) : Finset (Fin k)

The bottom endpoints of the through strands of D.

Equations

• D.bottomThrough = {i : Fin k | D.IsThrough (Sum.inl i)}

def TauCeti.BrauerDiagram.topThrough {k : ℕ} (D : BrauerDiagram k) : Finset (Fin k)

The top endpoints of the through strands of D.

Equations

• D.topThrough = {j : Fin k | D.IsThrough (Sum.inr j)}

def TauCeti.BrauerDiagram.bottomCap {k : ℕ} (D : BrauerDiagram k) : Finset (Fin k)

The bottom endpoints of the caps of D.

Equations

• D.bottomCap = {i : Fin k | D.IsCap (Sum.inl i)}

def TauCeti.BrauerDiagram.topCup {k : ℕ} (D : BrauerDiagram k) : Finset (Fin k)

The top endpoints of the cups of D.

Equations

• D.topCup = {j : Fin k | D.IsCup (Sum.inr j)}

@[simp]

theorem TauCeti.BrauerDiagram.mem_bottomThrough {k : ℕ} (D : BrauerDiagram k) {i : Fin k} : i ∈ D.bottomThrough ↔ D.IsThrough (Sum.inl i)

@[simp]

theorem TauCeti.BrauerDiagram.mem_topThrough {k : ℕ} (D : BrauerDiagram k) {j : Fin k} : j ∈ D.topThrough ↔ D.IsThrough (Sum.inr j)

@[simp]

theorem TauCeti.BrauerDiagram.mem_bottomCap {k : ℕ} (D : BrauerDiagram k) {i : Fin k} : i ∈ D.bottomCap ↔ D.IsCap (Sum.inl i)

@[simp]

theorem TauCeti.BrauerDiagram.mem_topCup {k : ℕ} (D : BrauerDiagram k) {j : Fin k} : j ∈ D.topCup ↔ D.IsCup (Sum.inr j)

theorem TauCeti.BrauerDiagram.bottomCap_eq_compl {k : ℕ} (D : BrauerDiagram k) : D.bottomCap = D.bottomThroughᶜ

The capped bottom points are the ones that no through strand reaches.

theorem TauCeti.BrauerDiagram.topCup_eq_compl {k : ℕ} (D : BrauerDiagram k) : D.topCup = D.topThroughᶜ

The cupped top points are the ones that no through strand reaches.

def TauCeti.BrauerDiagram.throughEquiv {k : ℕ} (D : BrauerDiagram k) : { i : Fin k // D.IsThrough (Sum.inl i) } ≃ { j : Fin k // D.IsThrough (Sum.inr j) }

Following an arc through matches the bottom endpoints of the through strands of D with their top endpoints.

Equations

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

@[simp]

theorem TauCeti.BrauerDiagram.inr_throughEquiv {k : ℕ} (D : BrauerDiagram k) (i : { i : Fin k // D.IsThrough (Sum.inl i) }) : Sum.inr ↑(D.throughEquiv i) = ↑D (Sum.inl ↑i)

The top endpoint that BrauerDiagram.throughEquiv assigns to a bottom point is the point that the diagram matches with it.

@[simp]

theorem TauCeti.BrauerDiagram.inl_throughEquiv_symm {k : ℕ} (D : BrauerDiagram k) (j : { j : Fin k // D.IsThrough (Sum.inr j) }) : Sum.inl ↑(D.throughEquiv.symm j) = ↑D (Sum.inr ↑j)

The bottom endpoint that BrauerDiagram.throughEquiv assigns to a top point is the point that the diagram matches with it.

theorem TauCeti.BrauerDiagram.card_bottomThrough_eq_card_topThrough {k : ℕ} (D : BrauerDiagram k) : D.bottomThrough.card = D.topThrough.card

A diagram has as many bottom endpoints of through strands as top endpoints.

theorem TauCeti.BrauerDiagram.card_bottomCap_eq_card_topCup {k : ℕ} (D : BrauerDiagram k) : D.bottomCap.card = D.topCup.card

A diagram has as many capped bottom points as cupped top points, hence as many caps as cups.

theorem TauCeti.BrauerDiagram.forall_isThrough_iff_bottomCap_eq_empty {k : ℕ} (D : BrauerDiagram k) : (∀ (x : Fin k ⊕ Fin k), D.IsThrough x) ↔ D.bottomCap = ∅

A diagram all of whose arcs go through is one that caps no bottom point, and conversely.

theorem TauCeti.BrauerDiagram.exists_eq_permToBrauer_iff_bottomCap_eq_empty {k : ℕ} (D : BrauerDiagram k) : (∃ (σ : Equiv.Perm (Fin k)), D = permToBrauer σ) ↔ D.bottomCap = ∅

A diagram is a permutation diagram exactly when it caps no bottom point. The permutation is then TauCeti.BrauerDiagram.throughPerm.

def TauCeti.BrauerDiagram.capMatching {k : ℕ} (D : BrauerDiagram k) : PerfectMatching { i : Fin k // D.IsCap (Sum.inl i) }

The perfect matching that a diagram induces on its capped bottom points: the caps pair those points off among themselves.

Equations

• D.capMatching = TauCeti.PerfectMatching.mk (Function.Involutive.toPerm (TauCeti.BrauerDiagram.capFun✝ D) ⋯) ⋯ ⋯

@[simp]

theorem TauCeti.BrauerDiagram.inl_capMatching {k : ℕ} (D : BrauerDiagram k) (i : { i : Fin k // D.IsCap (Sum.inl i) }) : Sum.inl ↑(↑D.capMatching i) = ↑D (Sum.inl ↑i)

BrauerDiagram.capMatching matches a capped bottom point with the other end of its cap.

theorem TauCeti.BrauerDiagram.even_card_bottomCap {k : ℕ} (D : BrauerDiagram k) : Even D.bottomCap.card

A diagram has an even number of capped bottom points: the caps pair those points off among themselves.

def TauCeti.BrauerDiagram.cupMatching {k : ℕ} (D : BrauerDiagram k) : PerfectMatching { j : Fin k // D.IsCup (Sum.inr j) }

The perfect matching that a diagram induces on its cupped top points: the cups pair those points off among themselves.

Equations

• D.cupMatching = TauCeti.PerfectMatching.mk (Function.Involutive.toPerm (TauCeti.BrauerDiagram.cupFun✝ D) ⋯) ⋯ ⋯

@[simp]

theorem TauCeti.BrauerDiagram.inr_cupMatching {k : ℕ} (D : BrauerDiagram k) (j : { j : Fin k // D.IsCup (Sum.inr j) }) : Sum.inr ↑(↑D.cupMatching j) = ↑D (Sum.inr ↑j)

BrauerDiagram.cupMatching matches a cupped top point with the other end of its cup.