Commutation of disjoint single-pair glues

Two single-pair glues at disjoint label pairs commute up to fragment equivalence: gluing {i, j} then {k, l} yields an equivalent fragment to gluing {k, l} then {i, j}, provided the four labels are pairwise distinct. This is the engine of associativity for the skein category.

The proof proceeds by classifying the involution structure of W.pairing on the four boundary flags: whether the pairs {i, j} and {k, l} are edges determines the open/closed status of each glue and thus the circle count and rewiring behaviour.

Label plumbing

def RS.Fragment.swapLabelEquiv {α : Type} {i j k l : α} (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) : SurvivingLabel (SurvivingLabel α i j) ⟨k, ⋯⟩ ⟨l, ⋯⟩ ≃ SurvivingLabel (SurvivingLabel α k l) ⟨i, ⋯⟩ ⟨j, ⋯⟩

The swap equivalence between nested surviving-label subtypes: removing {i, j} then {k, l} is the same as removing {k, l} then {i, j}.

Equations

• One or more equations did not get rendered due to their size.

What the two orders share

Neither the surviving flags nor the attachment map of a double glue depends on the order the two pairs are glued in: either order leaves the flags of W that are none of the four glued boundary flags, and either order reads attachment off W.attach. Only the pairing and the circle count tell the configurations below apart, so the pairing is all each of them has to compute.

def RS.Fragment.doubleSurvivingSwap {α : Type} (W : Fragment α) {i j k l : α} (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) : { f : W.SurvivingFlag i j // f ≠ W.glueBoundaryFlag i j ⟨k, ⋯⟩ ∧ f ≠ W.glueBoundaryFlag i j ⟨l, ⋯⟩ } ≃ { f : W.SurvivingFlag k l // f ≠ W.glueBoundaryFlag k l ⟨i, ⋯⟩ ∧ f ≠ W.glueBoundaryFlag k l ⟨j, ⋯⟩ }

The flags surviving both glues, read in either order: removing {i, j} and then {k, l} nests the four exclusions one way, and removing {k, l} first nests them the other way. The swap is the identity on the underlying flag of W.

Equations

• One or more equations did not get rendered due to their size.

Configuration (4): both pairs are edges (closed-closed)

def RS.Fragment.closedClosedEquiv {α : Type} (W : Fragment α) {i j k l : α} (_hij : i ≠ j) (_hkl : k ≠ l) (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) (hclosed_ij : W.pairing (W.boundaryFlag i) = W.boundaryFlag j) (hclosed_kl : W.pairing (W.boundaryFlag k) = W.boundaryFlag l) : ((W.gluePairClosed i j hclosed_ij).gluePairClosed ⟨k, ⋯⟩ ⟨l, ⋯⟩ ⋯).Equiv (((W.gluePairClosed k l hclosed_kl).gluePairClosed ⟨i, ⋯⟩ ⟨j, ⋯⟩ ⋯).relabel (swapLabelEquiv hik hil hjk hjl).symm)

Configuration (4): commutativity when both {i, j} and {k, l} are edges of W. Both glues are closed in both orders, giving circles W.circles + 2 with the pairing restricted.

Equations

• One or more equations did not get rendered due to their size.

Configuration (0): both pairs are open and disjoint (open-open)

def RS.Fragment.openOpenDisjointEquiv {α : Type} (W : Fragment α) {i j k l : α} (hij : i ≠ j) (hkl : k ≠ l) (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) (hopen_ij : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (hopen_kl : W.pairing (W.boundaryFlag k) ≠ W.boundaryFlag l) (hfar_ik : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag k) (hfar_il : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag l) (hfar_jk : W.pairing (W.boundaryFlag j) ≠ W.boundaryFlag k) (hfar_jl : W.pairing (W.boundaryFlag j) ≠ W.boundaryFlag l) : ((W.gluePairOpen i j hij hopen_ij).gluePairOpen ⟨k, ⋯⟩ ⟨l, ⋯⟩ ⋯ ⋯).Equiv (((W.gluePairOpen k l hkl hopen_kl).gluePairOpen ⟨i, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯).relabel (swapLabelEquiv hik hil hjk hjl).symm)

Configuration (0): commutativity when both {i, j} and {k, l} are open (not edges) and disjoint (no cross-edges between the two pairs). Both glues are open in both orders, giving circles W.circles with a double-rewire that commutes.

Equations

• One or more equations did not get rendered due to their size.

Configuration (1): {i,j} closed, {k,l} open (closed-open mixed)

def RS.Fragment.closedOpenEquiv {α : Type} (W : Fragment α) {i j k l : α} (_hij : i ≠ j) (hkl : k ≠ l) (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) (hclosed_ij : W.pairing (W.boundaryFlag i) = W.boundaryFlag j) (hopen_kl : W.pairing (W.boundaryFlag k) ≠ W.boundaryFlag l) : ((W.gluePairClosed i j hclosed_ij).gluePairOpen ⟨k, ⋯⟩ ⟨l, ⋯⟩ ⋯ ⋯).Equiv (((W.gluePairOpen k l hkl hopen_kl).gluePairClosed ⟨i, ⋯⟩ ⟨j, ⋯⟩ ⋯).relabel (swapLabelEquiv hik hil hjk hjl).symm)

Configuration (1): commutativity when {i, j} is an edge and {k, l} is not. The ij-first order is closed then open; the kl-first order is open then closed; both give circles W.circles + 1.

Equations

• One or more equations did not get rendered due to their size.

Configuration (1'): {k,l} closed, {i,j} open (open-closed mixed)

def RS.Fragment.openClosedEquiv {α : Type} (W : Fragment α) {i j k l : α} (hij : i ≠ j) (_hkl : k ≠ l) (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) (hopen_ij : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (hclosed_kl : W.pairing (W.boundaryFlag k) = W.boundaryFlag l) : ((W.gluePairOpen i j hij hopen_ij).gluePairClosed ⟨k, ⋯⟩ ⟨l, ⋯⟩ ⋯).Equiv (((W.gluePairClosed k l hclosed_kl).gluePairOpen ⟨i, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯).relabel (swapLabelEquiv hik hil hjk hjl).symm)

Configuration (1'): commutativity when {k, l} is an edge and {i, j} is not. The ij-first order is open then closed; the kl-first order is closed then open; both give circles W.circles + 1.

Equations

• One or more equations did not get rendered due to their size.

Configuration (2): one cross-edge, variant {ik}

def RS.Fragment.oneCrossIkEquiv {α : Type} (W : Fragment α) {i j k l : α} (hij : i ≠ j) (hkl : k ≠ l) (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) (hopen_ij : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (hopen_kl : W.pairing (W.boundaryFlag k) ≠ W.boundaryFlag l) (hcross : W.pairing (W.boundaryFlag i) = W.boundaryFlag k) (hfar_jl : W.pairing (W.boundaryFlag j) ≠ W.boundaryFlag l) : ((W.gluePairOpen i j hij hopen_ij).gluePairOpen ⟨k, ⋯⟩ ⟨l, ⋯⟩ ⋯ ⋯).Equiv (((W.gluePairOpen k l hkl hopen_kl).gluePairOpen ⟨i, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯).relabel (swapLabelEquiv hik hil hjk hjl).symm)

Configuration (2), variant {ik}: one cross-edge W.pairing(bFi) = bFk. Both glues are open in both orders; circles = W.circles.

Equations

• One or more equations did not get rendered due to their size.

Configuration (2): one cross-edge, variant {il}

def RS.Fragment.oneCrossIlEquiv {α : Type} (W : Fragment α) {i j k l : α} (hij : i ≠ j) (hkl : k ≠ l) (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) (hopen_ij : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (hopen_kl : W.pairing (W.boundaryFlag k) ≠ W.boundaryFlag l) (hcross : W.pairing (W.boundaryFlag i) = W.boundaryFlag l) (hfar_jk : W.pairing (W.boundaryFlag j) ≠ W.boundaryFlag k) : ((W.gluePairOpen i j hij hopen_ij).gluePairOpen ⟨k, ⋯⟩ ⟨l, ⋯⟩ ⋯ ⋯).Equiv (((W.gluePairOpen k l hkl hopen_kl).gluePairOpen ⟨i, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯).relabel (swapLabelEquiv hik hil hjk hjl).symm)

Configuration (2), variant {il}: one cross-edge W.pairing(bFi) = bFl. Both glues are open in both orders; circles = W.circles.

Equations

• One or more equations did not get rendered due to their size.

Configuration (2): one cross-edge, variant {jk}

def RS.Fragment.oneCrossJkEquiv {α : Type} (W : Fragment α) {i j k l : α} (hij : i ≠ j) (hkl : k ≠ l) (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) (hopen_ij : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (hopen_kl : W.pairing (W.boundaryFlag k) ≠ W.boundaryFlag l) (hcross : W.pairing (W.boundaryFlag j) = W.boundaryFlag k) (hfar_il : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag l) : ((W.gluePairOpen i j hij hopen_ij).gluePairOpen ⟨k, ⋯⟩ ⟨l, ⋯⟩ ⋯ ⋯).Equiv (((W.gluePairOpen k l hkl hopen_kl).gluePairOpen ⟨i, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯).relabel (swapLabelEquiv hik hil hjk hjl).symm)

Configuration (2), variant {jk}: one cross-edge W.pairing(bFj) = bFk. Both glues are open in both orders; circles = W.circles.

Equations

• One or more equations did not get rendered due to their size.

Configuration (2): one cross-edge, variant {jl}

def RS.Fragment.oneCrossJlEquiv {α : Type} (W : Fragment α) {i j k l : α} (hij : i ≠ j) (hkl : k ≠ l) (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) (hopen_ij : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (hopen_kl : W.pairing (W.boundaryFlag k) ≠ W.boundaryFlag l) (hcross : W.pairing (W.boundaryFlag j) = W.boundaryFlag l) (hfar_ik : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag k) : ((W.gluePairOpen i j hij hopen_ij).gluePairOpen ⟨k, ⋯⟩ ⟨l, ⋯⟩ ⋯ ⋯).Equiv (((W.gluePairOpen k l hkl hopen_kl).gluePairOpen ⟨i, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯).relabel (swapLabelEquiv hik hil hjk hjl).symm)

Configuration (2), variant {jl}: one cross-edge W.pairing(bFj) = bFl. Both glues are open in both orders; circles = W.circles.

Equations

• One or more equations did not get rendered due to their size.

Configuration (3): two cross-edges (open then closed)

def RS.Fragment.twoCrossIkjlEquiv {α : Type} (W : Fragment α) {i j k l : α} (hij : i ≠ j) (hkl : k ≠ l) (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) (hopen_ij : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (hopen_kl : W.pairing (W.boundaryFlag k) ≠ W.boundaryFlag l) (hcross_ik : W.pairing (W.boundaryFlag i) = W.boundaryFlag k) (hcross_jl : W.pairing (W.boundaryFlag j) = W.boundaryFlag l) : ((W.gluePairOpen i j hij hopen_ij).gluePairClosed ⟨k, ⋯⟩ ⟨l, ⋯⟩ ⋯).Equiv (((W.gluePairOpen k l hkl hopen_kl).gluePairClosed ⟨i, ⋯⟩ ⟨j, ⋯⟩ ⋯).relabel (swapLabelEquiv hik hil hjk hjl).symm)

Configuration (3), variant {ik,jl}: two cross-edges. First glue is open, second is closed; circles = W.circles + 1.

Equations

• One or more equations did not get rendered due to their size.

def RS.Fragment.twoCrossIljkEquiv {α : Type} (W : Fragment α) {i j k l : α} (hij : i ≠ j) (hkl : k ≠ l) (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) (hopen_ij : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (hopen_kl : W.pairing (W.boundaryFlag k) ≠ W.boundaryFlag l) (hcross_il : W.pairing (W.boundaryFlag i) = W.boundaryFlag l) (hcross_jk : W.pairing (W.boundaryFlag j) = W.boundaryFlag k) : ((W.gluePairOpen i j hij hopen_ij).gluePairClosed ⟨k, ⋯⟩ ⟨l, ⋯⟩ ⋯).Equiv (((W.gluePairOpen k l hkl hopen_kl).gluePairClosed ⟨i, ⋯⟩ ⟨j, ⋯⟩ ⋯).relabel (swapLabelEquiv hik hil hjk hjl).symm)

Configuration (3), variant {il,jk}: two cross-edges. First glue is open, second is closed; circles = W.circles + 1.

Equations

• One or more equations did not get rendered due to their size.

Main dispatch: gluePairComm

def RS.Fragment.gluePairComm {α : Type} (W : Fragment α) {i j k l : α} (hij : i ≠ j) (hkl : k ≠ l) (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) : ((W.gluePair i j hij).gluePair ⟨k, ⋯⟩ ⟨l, ⋯⟩ ⋯).Equiv (((W.gluePair k l hkl).gluePair ⟨i, ⋯⟩ ⟨j, ⋯⟩ ⋯).relabel (swapLabelEquiv hik hil hjk hjl).symm)

Two single-pair glues at disjoint label pairs commute up to fragment equivalence.

Equations

• One or more equations did not get rendered due to their size.