The propagating number of a Brauer diagram

The arcs of a Brauer diagram on k strands are of three kinds: through strands, caps and cups. The propagating number TauCeti.BrauerDiagram.propagatingNumber counts the through strands. It is the basic numerical invariant of a diagram: it is at most k, it has the same parity as k because the remaining bottom points are matched in pairs by the caps, and it equals k exactly for the permutation diagrams.

The point of the invariant is that vertical stacking can only destroy through strands, never create them: a through strand of TauCeti.composeDiagram D₁ D₂ is a through strand of D₂ continued by a through strand of D₁, so the propagating number of a composite is at most the propagating number of either factor. Consequently the diagrams of propagating number at most t absorb stacking on both sides -- the diagram-level shadow of the ideals in the cell filtration of the Brauer algebra -- and, at the top of the filtration, a product of diagrams is a permutation diagram only if both factors already are (TauCeti.BrauerDiagram.composeDiagram_eq_permToBrauer_iff). That last statement is the precise sense in which TauCeti.permToBrauer is the inclusion of the invertible diagrams: a diagram divides the identity diagram exactly when it is a permutation diagram (TauCeti.BrauerDiagram.exists_composeDiagram_right_eq_permToBrauer_one_iff).

Main definitions

• TauCeti.BrauerDiagram.propagatingNumber: the number of through strands of a Brauer diagram.

Main results

• TauCeti.BrauerDiagram.propagatingNumber_add_card_bottomCap: the through strands and the capped bottom points exhaust the bottom boundary, so the propagating number is at most k (TauCeti.BrauerDiagram.propagatingNumber_le) and k minus it is even (TauCeti.BrauerDiagram.even_sub_propagatingNumber).
• TauCeti.BrauerDiagram.propagatingNumber_eq_iff_exists_eq_permToBrauer: the propagating number is k exactly for the permutation diagrams, and TauCeti.BrauerDiagram.propagatingNumber_eq_zero_iff: it is 0 exactly for the diagrams built out of caps and cups alone.
• TauCeti.BrauerDiagram.propagatingNumber_composeDiagram_le_left and TauCeti.BrauerDiagram.propagatingNumber_composeDiagram_le_right: stacking cannot raise the propagating number.
• TauCeti.BrauerDiagram.composeDiagram_eq_permToBrauer_iff and TauCeti.BrauerDiagram.exists_composeDiagram_right_eq_permToBrauer_one_iff: the diagrams dividing a permutation diagram are exactly the permutation diagrams.

Implementation notes

The propagating number is defined as the number of bottom endpoints of the through strands, that is as the cardinality of TauCeti.BrauerDiagram.bottomThrough, and TauCeti.BrauerDiagram.propagatingNumber_eq_card_topThrough proves it equal to the number of top endpoints.

Stacking is left as TauCeti.composeDiagram rather than being packaged as a multiplication: the multiplication of the Brauer algebra weights the stacking by the number of loops closed up in the middle, which the bounds below do not need.

References

• R. Brauer, On algebras which are connected with the semisimple continuous groups, Annals of Mathematics 38 (1937), 857-872.
• T. Halverson and T. N. Jacobson, Set-partition tableaux and representations of diagram algebras, Algebraic Combinatorics 3 (2020), 509-538, §2.4, for the propagating number of a diagram and the two-sided ideals of a diagram algebra it filters by.

def TauCeti.BrauerDiagram.propagatingNumber {k : ℕ} (D : BrauerDiagram k) : ℕ

The propagating number of a Brauer diagram: the number of its through strands, counted at their bottom endpoints.

Equations

• D.propagatingNumber = D.bottomThrough.card

theorem TauCeti.BrauerDiagram.propagatingNumber_def {k : ℕ} (D : BrauerDiagram k) : D.propagatingNumber = D.bottomThrough.card

The propagating number counts the bottom endpoints of the through strands.

theorem TauCeti.BrauerDiagram.propagatingNumber_eq_card_topThrough {k : ℕ} (D : BrauerDiagram k) : D.propagatingNumber = D.topThrough.card

The propagating number counts the top endpoints of the through strands just as well: following an arc through matches the two sets of endpoints.

theorem TauCeti.BrauerDiagram.propagatingNumber_add_card_bottomCap {k : ℕ} (D : BrauerDiagram k) : D.propagatingNumber + D.bottomCap.card = k

Every bottom point lies on a through strand or on a cap, so the two counts add up to the number of bottom points.

theorem TauCeti.BrauerDiagram.propagatingNumber_le {k : ℕ} (D : BrauerDiagram k) : D.propagatingNumber ≤ k

A diagram on k strands has at most k through strands.

theorem TauCeti.BrauerDiagram.even_sub_propagatingNumber {k : ℕ} (D : BrauerDiagram k) : Even (k - D.propagatingNumber)

The propagating number has the parity of k: the bottom points off the through strands are matched in pairs by the caps.

@[simp]

theorem TauCeti.BrauerDiagram.propagatingNumber_relabel {k : ℕ} (D : BrauerDiagram k) (σ τ : Equiv.Perm (Fin k)) : (D.relabel σ τ).propagatingNumber = D.propagatingNumber

Relabelling the boundary does not change the propagating number.

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

A diagram has full propagating number exactly when all its arcs go through.

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

A diagram has full propagating number exactly when it is a permutation diagram.

@[simp]

theorem TauCeti.BrauerDiagram.propagatingNumber_permToBrauer {k : ℕ} (σ : Equiv.Perm (Fin k)) : (permToBrauer σ).propagatingNumber = k

A permutation diagram has k through strands.

theorem TauCeti.BrauerDiagram.propagatingNumber_lt_of_isCap {k : ℕ} (D : BrauerDiagram k) {x : Fin k ⊕ Fin k} (h : D.IsCap x) : D.propagatingNumber < k

A single horizontal arc already lowers the propagating number.

theorem TauCeti.BrauerDiagram.propagatingNumber_eq_zero_iff {k : ℕ} (D : BrauerDiagram k) : D.propagatingNumber = 0 ↔ ∀ (x : Fin k ⊕ Fin k), ¬D.IsThrough x

A diagram propagates nothing exactly when none of its arcs goes through, that is, when it is built out of caps and cups alone.

Stacking cannot raise the propagating number

theorem TauCeti.BrauerDiagram.propagatingNumber_composeDiagram_le_left {k : ℕ} (D₁ D₂ : BrauerDiagram k) : (composeDiagram D₁ D₂).propagatingNumber ≤ D₁.propagatingNumber

A through strand of a composite comes from a through strand of the upper diagram, so stacking cannot raise the propagating number.

theorem TauCeti.BrauerDiagram.propagatingNumber_composeDiagram_le_right {k : ℕ} (D₁ D₂ : BrauerDiagram k) : (composeDiagram D₁ D₂).propagatingNumber ≤ D₂.propagatingNumber

A through strand of a composite comes from a through strand of the lower diagram, so stacking cannot raise the propagating number.

The diagrams dividing a permutation diagram

theorem TauCeti.BrauerDiagram.exists_eq_permToBrauer_left_of_composeDiagram_eq_permToBrauer {k : ℕ} {D₁ D₂ : BrauerDiagram k} {σ : Equiv.Perm (Fin k)} (h : composeDiagram D₁ D₂ = permToBrauer σ) : ∃ (ρ : Equiv.Perm (Fin k)), D₁ = permToBrauer ρ

A composite is a permutation diagram only if the upper factor already is.

theorem TauCeti.BrauerDiagram.exists_eq_permToBrauer_right_of_composeDiagram_eq_permToBrauer {k : ℕ} {D₁ D₂ : BrauerDiagram k} {σ : Equiv.Perm (Fin k)} (h : composeDiagram D₁ D₂ = permToBrauer σ) : ∃ (ρ : Equiv.Perm (Fin k)), D₂ = permToBrauer ρ

A composite is a permutation diagram only if the lower factor already is.

theorem TauCeti.BrauerDiagram.composeDiagram_eq_permToBrauer_iff {k : ℕ} {D₁ D₂ : BrauerDiagram k} {σ : Equiv.Perm (Fin k)} : composeDiagram D₁ D₂ = permToBrauer σ ↔ ∃ (ρ : Equiv.Perm (Fin k)) (τ : Equiv.Perm (Fin k)), D₁ = permToBrauer ρ ∧ D₂ = permToBrauer τ ∧ ρ * τ = σ

Stacking yields a permutation diagram exactly when both factors are permutation diagrams, and then the permutations multiply.

theorem TauCeti.BrauerDiagram.exists_composeDiagram_right_eq_permToBrauer_one_iff {k : ℕ} {D : BrauerDiagram k} : (∃ (E : BrauerDiagram k), composeDiagram D E = permToBrauer 1) ↔ ∃ (σ : Equiv.Perm (Fin k)), D = permToBrauer σ

The invertible Brauer diagrams are exactly the permutation diagrams: a diagram admits a right stacking factor giving the identity diagram exactly when it is a permutation diagram.

theorem TauCeti.BrauerDiagram.exists_composeDiagram_left_eq_permToBrauer_one_iff {k : ℕ} {D : BrauerDiagram k} : (∃ (E : BrauerDiagram k), composeDiagram E D = permToBrauer 1) ↔ ∃ (σ : Equiv.Perm (Fin k)), D = permToBrauer σ

The invertible Brauer diagrams are exactly the permutation diagrams, in the left-factor form.