Documentation

TauCeti.Combinatorics.Brauer.Flip

Turning a Brauer diagram upside down #

Reflecting a Brauer diagram in a horizontal line exchanges its bottom and its top boundary. On the perfect matching of Fin k ⊕ Fin k that a diagram is, that reflection is conjugation by Sum.swap, and this file builds it as TauCeti.BrauerDiagram.flip, together with its two compatibilities with the vertical stacking of diagrams:

flip (composeDiagram D₁ D₂) = composeDiagram (flip D₂) (flip D₁), middleLoopCount (flip D₂) (flip D₁) = middleLoopCount D₁ D₂.

Reflection therefore reverses the order of a stack and leaves the number of loops that close up in its middle alone, so D ↦ flip D reverses the loop-weighted stacking D₁ * D₂ = δ ^ middleLoopCount D₁ D₂ • composeDiagram D₁ D₂ of diagrams. That is the diagram-level operation an anti-automorphism (x y)* = y* x* of the Brauer algebra B_k(δ) is read off from; the algebra itself is not built here, and nothing below is a map of algebras. Reflection is therefore a symmetry of the relations of that stacking: each relation between diagrams has a mirror, the same stack turned upside down, and reflection carries one to the other. A cap-cup diagram is its own reflection (TauCeti.BrauerDiagram.flip_capCup, stated beside TauCeti.capCup in TauCeti/Combinatorics/Brauer/Generator.lean), so the relations between cap-cup and permutation diagrams in TauCeti/Combinatorics/Brauer/Relations.lean come in mirror pairs.

Reflection is an involution, exchanges caps with cups, inverts a permutation diagram, and on a relabelled diagram exchanges the two renamings.

The two stacking compatibilities #

Reflecting the stack of D₁ above D₂ gives the stack of the reflection of D₂ above the reflection of D₁: a strand of either is a strand of the other read in the reflected labels, so the two stacks match the same pairs of outer points once those are reflected (TauCeti.flip_composeDiagram).

The middle of the stack is unchanged as a graph. Two middle points are joined by an arc of it when a cap of the upper diagram or a cup of the lower one joins them, and reflection exchanges those two kinds of arc without moving the middle point, so the two stacks have literally the same middle graph (TauCeti.middleAdj_flip) with the same interior vertices (TauCeti.isMiddleVertex_flip). Their closed loops, and hence their loop counts, therefore agree (TauCeti.middleLoopCount_flip).

Main definitions #

Main results #

References #

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

The reflection of a Brauer diagram in a horizontal line: the same diagram drawn upside down, its bottom point i becoming its top point i and conversely. On the perfect matching it is conjugation by Sum.swap.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.BrauerDiagram.flip_val_swap {k : ℕ} (D : BrauerDiagram k) (x : Fin k ⊕ Fin k) :
    ↑D.flip x.swap = (↑D x).swap

    The arcs of the reflected diagram are the arcs of the diagram with both endpoints reflected.

    source
    theorem TauCeti.BrauerDiagram.flip_val {k : ℕ} (D : BrauerDiagram k) (x : Fin k ⊕ Fin k) :
    ↑D.flip x = (↑D x.swap).swap

    The arc of the reflected diagram at x is the arc at the reflected point, reflected.

    source
    @[simp]
    theorem TauCeti.BrauerDiagram.flip_val_inl {k : ℕ} (D : BrauerDiagram k) (i : Fin k) :
    ↑D.flip (Sum.inl i) = (↑D (Sum.inr i)).swap

    The arc of the reflected diagram at a bottom point is the arc of the diagram at the corresponding top point.

    source
    @[simp]
    theorem TauCeti.BrauerDiagram.flip_val_inr {k : ℕ} (D : BrauerDiagram k) (j : Fin k) :
    ↑D.flip (Sum.inr j) = (↑D (Sum.inl j)).swap

    The arc of the reflected diagram at a top point is the arc of the diagram at the corresponding bottom point.

    source
    @[simp]
    theorem TauCeti.BrauerDiagram.flip_flip {k : ℕ} (D : BrauerDiagram k) :
    D.flip.flip = D

    Reflection is an involution: reflecting twice restores the diagram.

    source
    theorem TauCeti.BrauerDiagram.flip_injective {k : ℕ} :
    Function.Injective flip

    Reflection is injective, being an involution.

    Reflection exchanges caps and cups #

    source
    @[simp]
    theorem TauCeti.BrauerDiagram.isThrough_flip {k : ℕ} (D : BrauerDiagram k) (x : Fin k ⊕ Fin k) :
    D.flip.IsThrough x ↔ D.IsThrough x.swap

    Reflection carries a through strand to a through strand.

    source
    @[simp]
    theorem TauCeti.BrauerDiagram.isCap_flip {k : ℕ} (D : BrauerDiagram k) (x : Fin k ⊕ Fin k) :
    D.flip.IsCap x ↔ D.IsCup x.swap

    Reflection carries a cap to a cup.

    source
    @[simp]
    theorem TauCeti.BrauerDiagram.isCup_flip {k : ℕ} (D : BrauerDiagram k) (x : Fin k ⊕ Fin k) :
    D.flip.IsCup x ↔ D.IsCap x.swap

    Reflection carries a cup to a cap.

    source
    @[simp]
    theorem TauCeti.BrauerDiagram.bottomThrough_flip {k : ℕ} (D : BrauerDiagram k) :
    D.flip.bottomThrough = D.topThrough

    The bottom endpoints of the through strands of the reflected diagram are the top endpoints of the through strands of the diagram.

    source
    @[simp]
    theorem TauCeti.BrauerDiagram.topThrough_flip {k : ℕ} (D : BrauerDiagram k) :
    D.flip.topThrough = D.bottomThrough

    The top endpoints of the through strands of the reflected diagram are the bottom endpoints of the through strands of the diagram.

    source
    @[simp]
    theorem TauCeti.BrauerDiagram.bottomCap_flip {k : ℕ} (D : BrauerDiagram k) :
    D.flip.bottomCap = D.topCup

    The capped bottom points of the reflected diagram are the cupped top points of the diagram.

    source
    @[simp]
    theorem TauCeti.BrauerDiagram.topCup_flip {k : ℕ} (D : BrauerDiagram k) :
    D.flip.topCup = D.bottomCap

    The cupped top points of the reflected diagram are the capped bottom points of the diagram.

    Reflection on permutation and relabelled diagrams #

    source
    @[simp]
    theorem TauCeti.BrauerDiagram.flip_permToBrauer {k : ℕ} (σ : Equiv.Perm (Fin k)) :
    (permToBrauer σ).flip = permToBrauer σ⁻¹

    Reflection inverts a permutation diagram: read upside down, the strand i ↦ σ i is the strand σ i ↦ i.

    source
    @[simp]
    theorem TauCeti.BrauerDiagram.flip_relabel {k : ℕ} (D : BrauerDiagram k) (σ τ : Equiv.Perm (Fin k)) :
    (D.relabel σ τ).flip = D.flip.relabel τ σ

    Reflection exchanges the two renamings of a relabelling: the renaming of the bottom boundary becomes the renaming of the top boundary and conversely.

    Reflection reverses stacking #

    source
    theorem TauCeti.stackStart_flip {k : ℕ} (D₁ D₂ : BrauerDiagram k) (x : Fin k ⊕ Fin k) :
    stackStart D₂.flip D₁.flip x.swap = Sum.map Sum.swap Sum.swap (stackStart D₁ D₂ x)

    The first arc of a strand of the reflected stack. Reflecting the stack of D₁ above D₂ gives the stack of the reflection of D₂ above the reflection of D₁, and the first arc of its strand at the reflected outer point is the reflection of the first arc of the strand at that outer point: Sum.swap carries the outer boundary and the middle states across together.

    source
    theorem TauCeti.stackStep_flip {k : ℕ} (D₁ D₂ : BrauerDiagram k) (s : Fin k ⊕ Fin k) :
    stackStep D₂.flip D₁.flip s.swap = Sum.map Sum.swap Sum.swap (stackStep D₁ D₂ s)

    A later arc of a strand of the reflected stack, the companion of TauCeti.stackStart_flip. Reflection exchanges the two diagrams a middle state can point at, so it exchanges the two kinds of middle state and leaves the middle point untouched.

    source
    @[simp]
    theorem TauCeti.flip_composeDiagram {k : ℕ} (D₁ D₂ : BrauerDiagram k) :
    (composeDiagram D₁ D₂).flip = composeDiagram D₂.flip D₁.flip

    Reflection reverses stacking: the stack of D₁ above D₂, read upside down, is the stack of the reflection of D₂ above the reflection of D₁. Together with TauCeti.middleLoopCount_flip this says that reflection reverses the loop-weighted stacking of diagrams, the multiplication the Brauer algebra carries on its diagram basis.

    Reflection preserves the middle-loop count #

    source
    @[simp]
    theorem TauCeti.middleAdj_flip {k : ℕ} (D₁ D₂ : BrauerDiagram k) (a b : Fin k) :
    MiddleAdj D₂.flip D₁.flip a b ↔ MiddleAdj D₁ D₂ a b

    The two stacks have the same middle graph: reflection exchanges a cap of the upper diagram with a cup of the lower one, and both join the same two middle points.

    source
    @[simp]
    theorem TauCeti.reflTransGen_middleAdj_flip {k : ℕ} (D₁ D₂ : BrauerDiagram k) (a b : Fin k) :
    Relation.ReflTransGen (MiddleAdj D₂.flip D₁.flip) a b ↔ Relation.ReflTransGen (MiddleAdj D₁ D₂) a b

    Reflection preserves reachability in the middle graph: the two stacks have the same middle graph, so the same middle points are joined by a chain of its arcs.

    source
    @[simp]
    theorem TauCeti.isMiddleVertex_flip {k : ℕ} (D₁ D₂ : BrauerDiagram k) (a : Fin k) :
    IsMiddleVertex D₂.flip D₁.flip a ↔ IsMiddleVertex D₁ D₂ a

    The two stacks have the same interior middle points: keeping both arcs in the middle means being capped above and cupped below, and reflection exchanges the two conditions.

    source
    @[simp]
    theorem TauCeti.onMiddleLoop_flip {k : ℕ} (D₁ D₂ : BrauerDiagram k) (a : Fin k) :
    OnMiddleLoop D₂.flip D₁.flip a ↔ OnMiddleLoop D₁ D₂ a

    Reflection preserves the closed middle loops: a middle point lies on a loop of the reflected stack exactly when it lies on a loop of the stack.

    source
    @[simp]
    theorem TauCeti.isMiddleLoopMin_flip {k : ℕ} (D₁ D₂ : BrauerDiagram k) (a : Fin k) :
    IsMiddleLoopMin D₂.flip D₁.flip a ↔ IsMiddleLoopMin D₁ D₂ a

    Reflection preserves the least point of a closed middle loop, the point the loops are counted by.

    source
    @[simp]
    theorem TauCeti.middleLoopCount_flip {k : ℕ} (D₁ D₂ : BrauerDiagram k) :
    middleLoopCount D₂.flip D₁.flip = middleLoopCount D₁ D₂

    Reflection preserves the middle-loop count: turning a stack of two Brauer diagrams upside down closes up the same loops in the middle. With TauCeti.flip_composeDiagram this says that reflection reverses the loop-weighted stacking D₁ * D₂ = δ ^ middleLoopCount D₁ D₂ • composeDiagram D₁ D₂ of diagrams, the multiplication the Brauer algebra carries on its diagram basis.