Documentation

TauCeti.Combinatorics.Brauer.Labelling

Labellings of Brauer diagrams that are constant on arcs #

Label the boundary points of a Brauer diagram D on k strands by elements of a type ι: a bottom labelling u : Fin k → ι and a top labelling v : Fin k → ι, assembled into Sum.elim u v. The labelling is constant on arcs (TauCeti.BrauerDiagram.IsConstantOnArcs) when the two endpoints of every arc carry the same label. These are the matrix entries of the action of the Brauer algebra on the tensor power of V = ι → R with its standard symmetric form: the coefficient of the output basis tensor v in the image of the input basis tensor u under D is 1 when Sum.elim u v is constant on the arcs of D, and 0 otherwise. A cap of D contracts two input slots through the form, which pairs equal coordinates; a cup expands two output slots through the copairing ∑ c, e_c ⊗ e_c; and a through strand copies a coordinate.

The point of this file is that these entries multiply according to the loop rule of the Brauer algebra. Stack D₁ above D₂, with bottom labels u and top labels v, and count the labellings m of the middle boundary for which both Sum.elim m v is constant on the arcs of D₁ and Sum.elim u m on the arcs of D₂. There is such a middle labelling only if Sum.elim u v is constant on the arcs of the composite TauCeti.composeDiagram D₁ D₂, since a label is carried unchanged along each strand of the stack (TauCeti.BrauerDiagram.IsConstantOnArcs.composeDiagram). Conversely, when it is, the middle labels on the strands are forced while the label on each closed middle loop is free, so there are exactly |ι| ^ c of them with c = TauCeti.middleLoopCount D₁ D₂ (TauCeti.BrauerDiagram.natCard_middleLabelling). That is the identity M(D₁) * M(D₂) = |ι| ^ c • M(D₁ ∘ D₂) for the matrices of the action, which makes it an action of the Brauer algebra B_k(|ι|).

Main definitions #

Main results #

Implementation notes #

The count is proved by restricting a middle labelling to the least points of the closed middle loops, the points counted by TauCeti.middleLoopCount. That restriction is injective because every middle point off the loops is joined in the middle graph to a point carrying a through strand of one of the two diagrams, whose label is the label of an outer point. It is surjective because those forced labels are consistent: the middle points joined to the through strand at an outer point y all lie on the strand of the stack that starts at y, so the outer points whose labels they are forced to carry are y and the far end of that strand, which carry the same label once the outer labelling is constant on the arcs of the composite. The strand is followed with TauCeti.stackStart and TauCeti.stackStep, the walk through which TauCeti.composeDiagram_val_eq_iff describes the composite.

References #

source
def TauCeti.BrauerDiagram.IsConstantOnArcs {k : ℕ} {ι : Type u_1} (D : BrauerDiagram k) (ℓ : Fin k ⊕ Fin k → ι) :
Prop

A labelling ℓ of the boundary points of the Brauer diagram D is constant on arcs when the two endpoints of every arc of D carry the same label.

Instances For
    source
    theorem TauCeti.BrauerDiagram.isConstantOnArcs_def {k : ℕ} {ι : Type u_1} (D : BrauerDiagram k) (ℓ : Fin k ⊕ Fin k → ι) :
    D.IsConstantOnArcs ℓ ↔ ∀ (x : Fin k ⊕ Fin k), ℓ (↑D x) = ℓ x

    A labelling is constant on arcs when it takes the same value at the two endpoints of every arc.

    source
    @[instance_reducible]
    instance TauCeti.BrauerDiagram.instDecidableIsConstantOnArcsOfDecidableEq {k : ℕ} {ι : Type u_1} [DecidableEq ι] (D : BrauerDiagram k) (ℓ : Fin k ⊕ Fin k → ι) :
    Decidable (D.IsConstantOnArcs ℓ)
    source
    theorem TauCeti.BrauerDiagram.isConstantOnArcs_permToBrauer_iff {k : ℕ} {ι : Type u_1} (σ : Equiv.Perm (Fin k)) (u v : Fin k → ι) :
    (permToBrauer σ).IsConstantOnArcs (Sum.elim u v) ↔ ∀ (i : Fin k), v (σ i) = u i

    Labellings of a permutation diagram. A labelling is constant on the arcs of the diagram of σ exactly when the top point σ i carries the label of the bottom point i.

    source
    theorem TauCeti.BrauerDiagram.isConstantOnArcs_capCup_iff {k : ℕ} {ι : Type u_1} {a b : Fin k} (hab : a ≠ b) (u v : Fin k → ι) :
    (capCup a b).IsConstantOnArcs (Sum.elim u v) ↔ u a = u b ∧ v a = v b ∧ ∀ (i : Fin k), i ≠ a → i ≠ b → v i = u i

    Labellings of a cap-cup diagram. A labelling is constant on the arcs of capCup a b exactly when the two capped bottom points carry the same label, the two cupped top points carry the same label, and every other top point carries the label of the bottom point below it.

    One label per arc #

    source
    def TauCeti.BrauerDiagram.isConstantOnArcsEquiv {k : ℕ} {ι : Type u_1} (D : BrauerDiagram k) :
    { m : Fin k ⊕ Fin k → ι // D.IsConstantOnArcs m } ≃ ({ x : Fin k ⊕ Fin k // D.IsLowerEnd x } → ι)

    A labelling constant on the arcs of D is the same as a free choice of a label at each lower end.

    Instances For
      source
      @[simp]
      theorem TauCeti.BrauerDiagram.isConstantOnArcsEquiv_apply {k : ℕ} {ι : Type u_1} (D : BrauerDiagram k) (m : { m : Fin k ⊕ Fin k → ι // D.IsConstantOnArcs m }) (x : { x : Fin k ⊕ Fin k // D.IsLowerEnd x }) :
      D.isConstantOnArcsEquiv m x = ↑m ↑x
      source
      theorem TauCeti.BrauerDiagram.isConstantOnArcsEquiv_symm_apply {k : ℕ} {ι : Type u_1} (D : BrauerDiagram k) (g : { x : Fin k ⊕ Fin k // D.IsLowerEnd x } → ι) (x : Fin k ⊕ Fin k) :
      ↑(D.isConstantOnArcsEquiv.symm g) x = if h : D.IsLowerEnd x then g ⟨x, h⟩ else g ⟨↑D x, ⋯⟩

      The labelling with prescribed labels at the lower ends carries, at every boundary point, the label of the lower end of its arc.

      source
      theorem TauCeti.BrauerDiagram.exists_forall_isConstantOnArcs_iff_eq {k : ℕ} {ι : Type u_1} [Fintype ι] (hk : k ≤ Fintype.card ι) (D : BrauerDiagram k) :
      ∃ (ℓ : Fin k ⊕ Fin k → ι), ∀ (D' : BrauerDiagram k), D'.IsConstantOnArcs ℓ ↔ D' = D

      A labelling that singles out a diagram. With at least k labels, some labelling of the boundary points, one that gives the k arcs of D pairwise distinct labels, is constant on the arcs of D and of no other Brauer diagram.

      source
      @[simp]
      theorem TauCeti.BrauerDiagram.isConstantOnArcs_flip_iff {k : ℕ} {ι : Type u_1} (D : BrauerDiagram k) (ℓ : Fin k ⊕ Fin k → ι) :
      D.flip.IsConstantOnArcs ℓ ↔ D.IsConstantOnArcs (ℓ ∘ Sum.swap)

      Reflecting a diagram exchanges the bottom and top labels: a labelling is constant on the arcs of D.flip exactly when, read with its bottom and top points exchanged, it is constant on the arcs of D.

      Labels are carried along the strands of a stack #

      source
      theorem TauCeti.BrauerDiagram.IsConstantOnArcs.composeDiagram {k : ℕ} {ι : Type u_1} {D₁ D₂ : BrauerDiagram k} {u v m : Fin k → ι} (h₁ : D₁.IsConstantOnArcs (Sum.elim m v)) (h₂ : D₂.IsConstantOnArcs (Sum.elim u m)) :
      (TauCeti.composeDiagram D₁ D₂).IsConstantOnArcs (Sum.elim u v)

      Labels are carried along strands. If a labelling of the stack of D₁ above D₂ is constant on the arcs of both diagrams, its restriction to the outer boundary is constant on the arcs of the composite TauCeti.composeDiagram D₁ D₂: each strand carries one label from end to end.

      Middle points with a through strand #

      The count #

      source
      theorem TauCeti.BrauerDiagram.natCard_middleLabelling {k : ℕ} {ι : Type u_1} {D₁ D₂ : BrauerDiagram k} {u v : Fin k → ι} (hC : (composeDiagram D₁ D₂).IsConstantOnArcs (Sum.elim u v)) :
      Nat.card { m : Fin k → ι // D₁.IsConstantOnArcs (Sum.elim m v) ∧ D₂.IsConstantOnArcs (Sum.elim u m) } = Nat.card ι ^ middleLoopCount D₁ D₂

      The loop rule for labellings. Stack D₁ above D₂ and label the outer boundary by Sum.elim u v, constant on the arcs of the composite TauCeti.composeDiagram D₁ D₂. Its extensions by a labelling m of the middle boundary, constant on the arcs of both diagrams, number |ι| ^ c with c = TauCeti.middleLoopCount D₁ D₂: the labels on the strands are forced, and the label of each closed middle loop is free. No finiteness of ι is needed: for an infinite ι both sides are 1 when there is no loop and 0 (the value of Nat.card on infinite types) when there is one.