Relabelling the boundary of a Brauer diagram

Renaming the bottom points of a Brauer diagram by a permutation σ and its top points by a permutation τ gives another Brauer diagram, TauCeti.BrauerDiagram.relabel: the arc joining x to y becomes the arc joining the renamed x to the renamed y, so the underlying perfect matching is conjugated by the renaming Equiv.Perm.sumCongr σ τ of the boundary points.

Relabelling twice is relabelling by the product, (D.relabel σ τ).relabel σ' τ' = D.relabel (σ' * σ) (τ' * τ), so relabelling is an action of Sₖ × Sₖ on the Brauer diagrams on k strands. It moves the arcs of a diagram around but does not change their kinds, so it preserves the numbers of caps, of cups and of through strands. The number of through strands is the statistic that stratifies the Brauer algebra, so that statistic is constant on each Sₖ × Sₖ orbit.

Relabelling is exactly what stacking a permutation diagram onto a Brauer diagram does, since a permutation diagram has neither a cap nor a cup and so extends no strand of the other diagram past the middle boundary; that is TauCeti.composeDiagram_permToBrauer_left and TauCeti.composeDiagram_permToBrauer_right, in TauCeti/Combinatorics/Brauer/Compose.lean, which imports this file.

Main definitions

• TauCeti.BrauerDiagram.relabel: renaming the bottom points of a Brauer diagram by σ and its top points by τ.

Main results

• TauCeti.BrauerDiagram.relabel_relabel: relabelling twice is relabelling by the product, so Sₖ × Sₖ acts on the Brauer diagrams.
• TauCeti.BrauerDiagram.relabel_permToBrauer: relabelling a permutation diagram conjugates the permutation.
• TauCeti.BrauerDiagram.bottomCap_relabel, TauCeti.BrauerDiagram.topCup_relabel, TauCeti.BrauerDiagram.bottomThrough_relabel and TauCeti.BrauerDiagram.topThrough_relabel: relabelling permutes the capped, cupped and through boundary points, so it preserves their numbers.

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, the permToBrauer build item.

def TauCeti.BrauerDiagram.relabel {k : ℕ} (D : BrauerDiagram k) (σ τ : Equiv.Perm (Fin k)) : BrauerDiagram k

Relabelling the boundary of a Brauer diagram: σ renames its bottom points and τ its top points, the arc joining x to y becoming the arc joining the renamed x to the renamed y.

Equations

• D.relabel σ τ = (TauCeti.PerfectMatching.congr (σ.sumCongr τ)) D

theorem TauCeti.BrauerDiagram.relabel_def {k : ℕ} (D : BrauerDiagram k) (σ τ : Equiv.Perm (Fin k)) : D.relabel σ τ = (PerfectMatching.congr (σ.sumCongr τ)) D

Relabelling is the conjugation of the underlying perfect matching by the renaming Equiv.Perm.sumCongr σ τ of the boundary points.

theorem TauCeti.BrauerDiagram.relabel_val_map {k : ℕ} (D : BrauerDiagram k) (σ τ : Equiv.Perm (Fin k)) (x : Fin k ⊕ Fin k) : ↑(D.relabel σ τ) (Sum.map (⇑σ) (⇑τ) x) = Sum.map (⇑σ) (⇑τ) (↑D x)

Relabelling carries the arc at x to the arc at the renamed x.

@[simp]

theorem TauCeti.BrauerDiagram.relabel_val_inl {k : ℕ} (D : BrauerDiagram k) (σ τ : Equiv.Perm (Fin k)) (i : Fin k) : ↑(D.relabel σ τ) (Sum.inl i) = Sum.map (⇑σ) (⇑τ) (↑D (Sum.inl ((Equiv.symm σ) i)))

The arc of a relabelled diagram at the bottom point i is the renamed arc at the bottom point σ.symm i that i was renamed from.

@[simp]

theorem TauCeti.BrauerDiagram.relabel_val_inr {k : ℕ} (D : BrauerDiagram k) (σ τ : Equiv.Perm (Fin k)) (j : Fin k) : ↑(D.relabel σ τ) (Sum.inr j) = Sum.map (⇑σ) (⇑τ) (↑D (Sum.inr ((Equiv.symm τ) j)))

The arc of a relabelled diagram at the top point j is the renamed arc at the top point τ.symm j that j was renamed from.

@[simp]

theorem TauCeti.BrauerDiagram.relabel_one_one {k : ℕ} (D : BrauerDiagram k) : D.relabel 1 1 = D

Relabelling by the identity permutations changes nothing.

@[simp]

theorem TauCeti.BrauerDiagram.relabel_relabel {k : ℕ} (D : BrauerDiagram k) (σ τ σ' τ' : Equiv.Perm (Fin k)) : (D.relabel σ τ).relabel σ' τ' = D.relabel (σ' * σ) (τ' * τ)

Relabelling twice is relabelling by the product. With TauCeti.BrauerDiagram.relabel_one_one this makes relabelling an action of Sₖ × Sₖ on the Brauer diagrams on k strands.

@[simp]

theorem TauCeti.BrauerDiagram.relabel_permToBrauer {k : ℕ} (σ τ ρ : Equiv.Perm (Fin k)) : (permToBrauer ρ).relabel σ τ = permToBrauer (τ * ρ * σ⁻¹)

Relabelling a permutation diagram conjugates the permutation: renaming the bottom points by σ and the top points by τ turns the strand i ↦ ρ i into the strand σ i ↦ τ (ρ i).

Relabelling preserves the kinds of the arcs

@[simp]

theorem TauCeti.BrauerDiagram.isThrough_relabel {k : ℕ} (D : BrauerDiagram k) (σ τ : Equiv.Perm (Fin k)) (x : Fin k ⊕ Fin k) : (D.relabel σ τ).IsThrough (Sum.map (⇑σ) (⇑τ) x) ↔ D.IsThrough x

Relabelling carries a through strand to a through strand: the renamed point lies on a through strand of the relabelled diagram exactly when the point lies on a through strand.

@[simp]

theorem TauCeti.BrauerDiagram.isCap_relabel {k : ℕ} (D : BrauerDiagram k) (σ τ : Equiv.Perm (Fin k)) (x : Fin k ⊕ Fin k) : (D.relabel σ τ).IsCap (Sum.map (⇑σ) (⇑τ) x) ↔ D.IsCap x

Relabelling carries a cap to a cap.

@[simp]

theorem TauCeti.BrauerDiagram.isCup_relabel {k : ℕ} (D : BrauerDiagram k) (σ τ : Equiv.Perm (Fin k)) (x : Fin k ⊕ Fin k) : (D.relabel σ τ).IsCup (Sum.map (⇑σ) (⇑τ) x) ↔ D.IsCup x

Relabelling carries a cup to a cup.

@[simp]

theorem TauCeti.BrauerDiagram.isThrough_relabel_inl {k : ℕ} (D : BrauerDiagram k) (σ τ : Equiv.Perm (Fin k)) (i : Fin k) : (D.relabel σ τ).IsThrough (Sum.inl (σ i)) ↔ D.IsThrough (Sum.inl i)

Relabelling carries a through strand starting at the bottom to a through strand.

@[simp]

theorem TauCeti.BrauerDiagram.isThrough_relabel_inr {k : ℕ} (D : BrauerDiagram k) (σ τ : Equiv.Perm (Fin k)) (j : Fin k) : (D.relabel σ τ).IsThrough (Sum.inr (τ j)) ↔ D.IsThrough (Sum.inr j)

Relabelling carries a through strand starting at the top to a through strand.

@[simp]

theorem TauCeti.BrauerDiagram.isCap_relabel_inl {k : ℕ} (D : BrauerDiagram k) (σ τ : Equiv.Perm (Fin k)) (i : Fin k) : (D.relabel σ τ).IsCap (Sum.inl (σ i)) ↔ D.IsCap (Sum.inl i)

Relabelling carries a cap to a cap, read off at the bottom boundary.

@[simp]

theorem TauCeti.BrauerDiagram.isCup_relabel_inr {k : ℕ} (D : BrauerDiagram k) (σ τ : Equiv.Perm (Fin k)) (j : Fin k) : (D.relabel σ τ).IsCup (Sum.inr (τ j)) ↔ D.IsCup (Sum.inr j)

Relabelling carries a cup to a cup, read off at the top boundary.

theorem TauCeti.BrauerDiagram.bottomCap_relabel {k : ℕ} (D : BrauerDiagram k) (σ τ : Equiv.Perm (Fin k)) : (D.relabel σ τ).bottomCap = Finset.image (⇑σ) D.bottomCap

The capped bottom points of a relabelled diagram are the renamed capped bottom points.

Not a simp lemma: rewriting by it takes TauCeti.BrauerDiagram.card_bottomCap_relabel out of simp-normal form, and simp cannot finish the resulting cardinality goal on its own.

theorem TauCeti.BrauerDiagram.topCup_relabel {k : ℕ} (D : BrauerDiagram k) (σ τ : Equiv.Perm (Fin k)) : (D.relabel σ τ).topCup = Finset.image (⇑τ) D.topCup

The cupped top points of a relabelled diagram are the renamed cupped top points.

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

theorem TauCeti.BrauerDiagram.bottomThrough_relabel {k : ℕ} (D : BrauerDiagram k) (σ τ : Equiv.Perm (Fin k)) : (D.relabel σ τ).bottomThrough = Finset.image (⇑σ) D.bottomThrough

The bottom endpoints of the through strands of a relabelled diagram are the renamed ones.

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

theorem TauCeti.BrauerDiagram.topThrough_relabel {k : ℕ} (D : BrauerDiagram k) (σ τ : Equiv.Perm (Fin k)) : (D.relabel σ τ).topThrough = Finset.image (⇑τ) D.topThrough

The top endpoints of the through strands of a relabelled diagram are the renamed ones.

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

@[simp]

theorem TauCeti.BrauerDiagram.card_bottomCap_relabel {k : ℕ} (D : BrauerDiagram k) (σ τ : Equiv.Perm (Fin k)) : (D.relabel σ τ).bottomCap.card = D.bottomCap.card

Relabelling does not change the number of caps.

@[simp]

theorem TauCeti.BrauerDiagram.card_topCup_relabel {k : ℕ} (D : BrauerDiagram k) (σ τ : Equiv.Perm (Fin k)) : (D.relabel σ τ).topCup.card = D.topCup.card

Relabelling does not change the number of cups.

@[simp]

theorem TauCeti.BrauerDiagram.card_bottomThrough_relabel {k : ℕ} (D : BrauerDiagram k) (σ τ : Equiv.Perm (Fin k)) : (D.relabel σ τ).bottomThrough.card = D.bottomThrough.card

Relabelling does not change the number of through strands.

@[simp]

theorem TauCeti.BrauerDiagram.card_topThrough_relabel {k : ℕ} (D : BrauerDiagram k) (σ τ : Equiv.Perm (Fin k)) : (D.relabel σ τ).topThrough.card = D.topThrough.card

Relabelling does not change the number of through strands, counted at the top.