The gluing action on chord diagrams

Gluing the cut {i, j} acts on label chord diagrams: the chord (i, j) closes into a loop; otherwise the chords at i and at j concatenate into one chord joining their far ends; chords avoiding the cut pass through. This is the combinatorial (Temperley–Lieb) composition over which the pairing-resolved gluing decomposition lives.

noncomputable def RS.cutPartner {α : Type} [LinearOrder α] (P : Finset (α × α)) (x : α) : Option α

The far end of the chord at x, when one exists.

Equations

• RS.cutPartner P x = if h : ∃ (y : α), (min x y, max x y) ∈ P then some (Classical.choose h) else none

noncomputable def RS.glueChords {α : Type} [LinearOrder α] (i j : α) (P : Finset (α × α)) : Finset (α × α)

The glued diagram.

Equations

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

theorem RS.cutPartner_eq_some {α : Type} [LinearOrder α] {P : Finset (α × α)} (hP : IsChordDiagram P) {x y : α} (h : (min x y, max x y) ∈ P) : cutPartner P x = some y

In a well-formed diagram a chord end determines its far end.

theorem RS.IsChordDiagram.mono {α : Type} [LinearOrder α] {P Q : Finset (α × α)} (hQP : Q ⊆ P) (hP : IsChordDiagram P) : IsChordDiagram Q

Well-formedness is inherited by subdiagrams.

theorem RS.glueChords_cross {α : Type} [LinearOrder α] {P : Finset (α × α)} (hP : IsChordDiagram P) {i j x y : α} (hxj : x ≠ j) (hi : (min i x, max i x) ∈ P) (hj : (min j y, max j y) ∈ P) : glueChords i j P = (P.erase (min i x, max i x)).erase (min j y, max j y) ∪ {(min x y, max x y)}

The glued diagram of a crossing cut: the chords at the two cut labels concatenate.