Documentation

TauCeti.Combinatorics.Brauer.Compose

Composing Brauer diagrams #

Two Brauer diagrams on k strands are composed by vertical stacking: place D₁ above D₂, identify the bottom boundary of D₁ with the top boundary of D₂, and read off the matching induced on the outer boundary. A strand of the composite starts at an outer point, follows an arc of one diagram, crosses the middle boundary into the other diagram, and repeats until it emerges at another outer point; TauCeti.composeDiagram is the Brauer diagram of those strands. It is the multiplication of the Brauer algebra on the diagram basis, up to the power of δ counting the loops that close up in the middle.

A strand is followed here by iterating a single permutation of the stacked boundary points -- the arcs of the two diagrams, followed by the gluing that identifies the two copies of the middle boundary -- and stopping the first time an outer point is reached. That the result is again a perfect matching rests on two identities: the gluing conjugates that permutation into its inverse, so walking from the far end of a strand retraces it, and the permutation is a gluing followed by a fixed-point-free involution, so a strand cannot return to its own starting point.

Stacking a permutation diagram onto a diagram creates no new strand, because a permutation diagram has neither a cap nor a cup: it only renames the boundary points that the strands of the other diagram end at, that is, it relabels that boundary in the sense of TauCeti.BrauerDiagram.relabel. The consequence that Layer 9 of the Schur--Weyl roadmap is after is the multiplicativity TauCeti.composeDiagram_permToBrauer: stacking two permutation diagrams gives the permutation diagram of the product, so σ ↦ permToBrauer σ turns the group law of Sₖ into the multiplication of the Brauer algebra on the diagram basis. That is the sense in which the symmetric group sits inside the Brauer algebra: once the loop-weighted multiplication of the Brauer algebra is available, this is what will make it restrict to the group algebra ℂ[Sₖ] along permToBrauer, since no loop can close up in the middle when one of the two diagrams has only through strands. The middle-loop count itself is built in TauCeti/Combinatorics/Brauer/LoopCount.lean.

Main definitions #

Main results #

References #

source
def TauCeti.composeDiagram {k : ℕ} (D₁ D₂ : BrauerDiagram k) :
BrauerDiagram k

Vertical stacking of Brauer diagrams. composeDiagram D₁ D₂ places D₁ above D₂, identifies the bottom boundary of D₁ with the top boundary of D₂, and matches two points of the outer boundary when a strand joins them: a strand follows an arc of one diagram, crosses the middle boundary into the other, and repeats until it reaches the outer boundary again. This is the multiplication of the Brauer algebra on the diagram basis, up to the power of δ counting the loops that close up in the middle.

Equations
Instances For
    source
    def TauCeti.stackStep {k : ℕ} (D₁ D₂ : BrauerDiagram k) :
    Fin k ⊕ Fin k → (Fin k ⊕ Fin k) ⊕ Fin k ⊕ Fin k

    Following a strand of the stack of D₁ above D₂ one arc further, from a middle state: a point of the middle boundary together with the diagram the strand runs through next. The middle state Sum.inl a is the middle point a reached as a bottom point of the upper diagram D₁, so the strand next follows the arc of D₁ at Sum.inl a; the middle state Sum.inr a is the middle point a reached as a top point of the lower diagram D₂, so the strand next follows the arc of D₂ at Sum.inr a. The value is Sum.inl y when that arc leaves the stack at the outer point y, and Sum.inr t when it crosses the middle boundary again, at the middle state t.

    Equations
    Instances For
      source
      def TauCeti.stackStart {k : ℕ} (D₁ D₂ : BrauerDiagram k) :
      Fin k ⊕ Fin k → (Fin k ⊕ Fin k) ⊕ Fin k ⊕ Fin k

      Following the strand of the stack of D₁ above D₂ that starts at the outer point x along its first arc, an arc of D₂ at a bottom point x = Sum.inl i and an arc of D₁ at a top point x = Sum.inr j. The value is Sum.inl y when that arc already leaves the stack, at the outer point y, and Sum.inr s when it crosses the middle boundary, at the middle state s of TauCeti.stackStep.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.stackStep_inl {k : ℕ} (D₁ D₂ : BrauerDiagram k) (a : Fin k) :
        stackStep D₁ D₂ (Sum.inl a) = Sum.elim (fun (a' : Fin k) => Sum.inr (Sum.inr a')) (fun (j : Fin k) => Sum.inl (Sum.inr j)) (↑D₁ (Sum.inl a))

        A strand at the middle point a, about to run up through D₁, follows the arc of D₁ at Sum.inl a.

        source
        @[simp]
        theorem TauCeti.stackStep_inr {k : ℕ} (D₁ D₂ : BrauerDiagram k) (a : Fin k) :
        stackStep D₁ D₂ (Sum.inr a) = Sum.elim (fun (i : Fin k) => Sum.inl (Sum.inl i)) (fun (a' : Fin k) => Sum.inr (Sum.inl a')) (↑D₂ (Sum.inr a))

        A strand at the middle point a, about to run down through D₂, follows the arc of D₂ at Sum.inr a.

        source
        @[simp]
        theorem TauCeti.stackStart_inl {k : ℕ} (D₁ D₂ : BrauerDiagram k) (i : Fin k) :
        stackStart D₁ D₂ (Sum.inl i) = Sum.elim (fun (i' : Fin k) => Sum.inl (Sum.inl i')) (fun (a : Fin k) => Sum.inr (Sum.inl a)) (↑D₂ (Sum.inl i))

        A strand starting at the bottom point i of the stack follows the arc of D₂ at Sum.inl i.

        source
        @[simp]
        theorem TauCeti.stackStart_inr {k : ℕ} (D₁ D₂ : BrauerDiagram k) (j : Fin k) :
        stackStart D₁ D₂ (Sum.inr j) = Sum.elim (fun (a : Fin k) => Sum.inr (Sum.inr a)) (fun (j' : Fin k) => Sum.inl (Sum.inr j')) (↑D₁ (Sum.inr j))

        A strand starting at the top point j of the stack follows the arc of D₁ at Sum.inr j.

        source
        theorem TauCeti.composeDiagram_val_eq_iff {k : ℕ} (D₁ D₂ : BrauerDiagram k) {x y : Fin k ⊕ Fin k} :
        ↑(composeDiagram D₁ D₂) x = y ↔ stackStart D₁ D₂ x = Sum.inl y ∨ ∃ (s : Fin k ⊕ Fin k) (t : Fin k ⊕ Fin k), stackStart D₁ D₂ x = Sum.inr s ∧ Relation.ReflTransGen (fun (u v : Fin k ⊕ Fin k) => stackStep D₁ D₂ u = Sum.inr v) s t ∧ stackStep D₁ D₂ t = Sum.inl y

        The strands of a stack of two Brauer diagrams. The composite of D₁ above D₂ matches the outer points x and y exactly when the strand starting at x emerges at y: either its first arc already leaves the stack at y, or it crosses the middle boundary at a middle state s, runs from there through finitely many further middle states to a middle state t, and leaves the stack at y from t.

        source
        theorem TauCeti.composeDiagram_val_inl_eq_inl_of_cap_lower {k : ℕ} (D₁ D₂ : BrauerDiagram k) {i i' : Fin k} (h : ↑D₂ (Sum.inl i) = Sum.inl i') :
        ↑(composeDiagram D₁ D₂) (Sum.inl i) = Sum.inl i'

        A cap of the lower diagram is a cap of the composite.

        source
        theorem TauCeti.composeDiagram_val_inr_eq_inr_of_cup_upper {k : ℕ} (D₁ D₂ : BrauerDiagram k) {j j' : Fin k} (h : ↑D₁ (Sum.inr j) = Sum.inr j') :
        ↑(composeDiagram D₁ D₂) (Sum.inr j) = Sum.inr j'

        A cup of the upper diagram is a cup of the composite.

        source
        theorem TauCeti.composeDiagram_val_inl_eq_inr_of_through {k : ℕ} (D₁ D₂ : BrauerDiagram k) {i a j : Fin k} (h₂ : ↑D₂ (Sum.inl i) = Sum.inr a) (h₁ : ↑D₁ (Sum.inl a) = Sum.inr j) :
        ↑(composeDiagram D₁ D₂) (Sum.inl i) = Sum.inr j

        A through strand of the lower diagram continued by a through strand of the upper diagram is a through strand of the composite.

        source
        theorem TauCeti.composeDiagram_val_inr_eq_inl_of_through {k : ℕ} (D₁ D₂ : BrauerDiagram k) {i a j : Fin k} (h₁ : ↑D₁ (Sum.inr j) = Sum.inl a) (h₂ : ↑D₂ (Sum.inr a) = Sum.inl i) :
        ↑(composeDiagram D₁ D₂) (Sum.inr j) = Sum.inl i

        A through strand of the composite, read from its top endpoint.

        source
        theorem TauCeti.composeDiagram_val_inl_eq_inl_of_cap_upper {k : ℕ} (D₁ D₂ : BrauerDiagram k) {i a a' i' : Fin k} (h₂ : ↑D₂ (Sum.inl i) = Sum.inr a) (h₁ : ↑D₁ (Sum.inl a) = Sum.inl a') (h₂' : ↑D₂ (Sum.inr a') = Sum.inl i') :
        ↑(composeDiagram D₁ D₂) (Sum.inl i) = Sum.inl i'

        A cap of the upper diagram, reached by two through strands of the lower one, is a cap of the composite.

        source
        theorem TauCeti.composeDiagram_val_inr_eq_inr_of_cup_lower {k : ℕ} (D₁ D₂ : BrauerDiagram k) {j a a' j' : Fin k} (h₁ : ↑D₁ (Sum.inr j) = Sum.inl a) (h₂ : ↑D₂ (Sum.inr a) = Sum.inr a') (h₁' : ↑D₁ (Sum.inl a') = Sum.inr j') :
        ↑(composeDiagram D₁ D₂) (Sum.inr j) = Sum.inr j'

        A cup of the lower diagram, reached by two through strands of the upper one, is a cup of the composite.

        source
        theorem TauCeti.BrauerDiagram.composeDiagram_val_inl_eq_inr_throughEquiv {k : ℕ} (D₁ D₂ : BrauerDiagram k) (i : { i : Fin k // D₂.IsThrough (Sum.inl i) }) (h : D₁.IsThrough (Sum.inl ↑(D₂.throughEquiv i))) :
        ↑(composeDiagram D₁ D₂) (Sum.inl ↑i) = Sum.inr ↑(D₁.throughEquiv ⟨↑(D₂.throughEquiv i), h⟩)

        A through strand of D₂ continued by a through strand of D₁ is a through strand of the composite: the composite joins the bottom endpoint of a through strand of D₂ to the top endpoint of the through strand of D₁ that continues it.

        source
        theorem TauCeti.BrauerDiagram.composeDiagram_val_inl_eq_inl_capMatching {k : ℕ} (D₁ D₂ : BrauerDiagram k) (i : { i : Fin k // D₂.IsCap (Sum.inl i) }) :
        ↑(composeDiagram D₁ D₂) (Sum.inl ↑i) = Sum.inl ↑(↑D₂.capMatching i)

        The caps of D₂ are caps of the composite: the composite matches a capped bottom point of D₂ with the other end of that cap.

        source
        theorem TauCeti.BrauerDiagram.composeDiagram_val_inr_eq_inr_cupMatching {k : ℕ} (D₁ D₂ : BrauerDiagram k) (j : { j : Fin k // D₁.IsCup (Sum.inr j) }) :
        ↑(composeDiagram D₁ D₂) (Sum.inr ↑j) = Sum.inr ↑(↑D₁.cupMatching j)

        The cups of D₁ are cups of the composite: the composite matches a cupped top point of D₁ with the other end of that cup.

        source
        theorem TauCeti.BrauerDiagram.bottomCap_subset_bottomCap_composeDiagram {k : ℕ} (D₁ D₂ : BrauerDiagram k) :
        D₂.bottomCap ⊆ (composeDiagram D₁ D₂).bottomCap

        Every capped bottom point of D₂ is a capped bottom point of the composite.

        source
        theorem TauCeti.BrauerDiagram.topCup_subset_topCup_composeDiagram {k : ℕ} (D₁ D₂ : BrauerDiagram k) :
        D₁.topCup ⊆ (composeDiagram D₁ D₂).topCup

        Every cupped top point of D₁ is a cupped top point of the composite.

        source
        theorem TauCeti.BrauerDiagram.bottomThrough_composeDiagram_subset {k : ℕ} (D₁ D₂ : BrauerDiagram k) :
        (composeDiagram D₁ D₂).bottomThrough ⊆ D₂.bottomThrough

        A bottom endpoint of a through strand of the composite is a bottom endpoint of a through strand of D₂.

        source
        theorem TauCeti.BrauerDiagram.topThrough_composeDiagram_subset {k : ℕ} (D₁ D₂ : BrauerDiagram k) :
        (composeDiagram D₁ D₂).topThrough ⊆ D₁.topThrough

        A top endpoint of a through strand of the composite is a top endpoint of a through strand of D₁.

        Stacking with a permutation diagram #

        source
        @[simp]
        theorem TauCeti.composeDiagram_permToBrauer_left {k : ℕ} (D : BrauerDiagram k) (σ : Equiv.Perm (Fin k)) :
        composeDiagram (permToBrauer σ) D = D.relabel 1 σ

        Stacking a permutation diagram on top relabels the top boundary. No strand of D is extended past the middle boundary, because the permutation diagram has no cap: a through strand of D ending at the middle point a is continued by the single strand of permToBrauer σ above it, which leaves at the top point σ a.

        source
        @[simp]
        theorem TauCeti.composeDiagram_permToBrauer_right {k : ℕ} (D : BrauerDiagram k) (τ : Equiv.Perm (Fin k)) :
        composeDiagram D (permToBrauer τ) = D.relabel τ⁻¹ 1

        Stacking a permutation diagram underneath relabels the bottom boundary. No strand of D is extended past the middle boundary, because the permutation diagram has no cup: the strand of permToBrauer τ starting at the bottom point i reaches the middle point τ i, where the arc of D takes over.

        source
        theorem TauCeti.composeDiagram_permToBrauer {k : ℕ} (σ τ : Equiv.Perm (Fin k)) :
        composeDiagram (permToBrauer σ) (permToBrauer τ) = permToBrauer (σ * τ)

        Stacking permutation diagrams multiplies the permutations. So the inclusion of the symmetric group into the Brauer diagrams turns the group law into vertical stacking; no loop closes up in the middle, since a permutation diagram has neither a cap nor a cup.

        This and the two identity laws below are not simp lemmas: they are the special cases of TauCeti.composeDiagram_permToBrauer_left and TauCeti.composeDiagram_permToBrauer_right in which the relabelling is one that simp already carries out, so simp proves them and tagging them would leave them out of simp-normal form.

        source
        theorem TauCeti.composeDiagram_permToBrauer_one_left {k : ℕ} (D : BrauerDiagram k) :
        composeDiagram (permToBrauer 1) D = D

        The identity diagram is a left identity for stacking.

        source
        theorem TauCeti.composeDiagram_permToBrauer_one_right {k : ℕ} (D : BrauerDiagram k) :
        composeDiagram D (permToBrauer 1) = D

        The identity diagram is a right identity for stacking.