Commutativity of pair closure

The closed fragment pairClose F G, formed by composing an (0+t)- with a (t+0)-fragment, is invariant (up to Fragment.Equiv) under swapping F and G.

def RS.Fragment.pairCloseSwapFun (t : ℕ) : Fin (0 + t) ⊕ Fin (t + 0) → Fin (0 + t) ⊕ Fin (t + 0)

Swap the two boundary summands in the comparison of opposite pair closures.

Equations

• RS.Fragment.pairCloseSwapFun t = Sum.elim (fun (x : Fin (0 + t)) => Sum.inr ((finCongr ⋯) x)) fun (y : Fin (t + 0)) => Sum.inl ((finCongr ⋯) y)

def RS.Fragment.pairCloseSwap (t : ℕ) : Fin (0 + t) ⊕ Fin (t + 0) ≃ Fin (0 + t) ⊕ Fin (t + 0)

Self-inverse sum-swap equivalence used in the pairClose commutativity proof.

Equations

• RS.Fragment.pairCloseSwap t = { toFun := RS.Fragment.pairCloseSwapFun t, invFun := RS.Fragment.pairCloseSwapFun t, left_inv := ⋯, right_inv := ⋯ }

noncomputable def RS.Fragment.pairCloseAmbient {t : ℕ} (F G : Fragment (Fin t)) : ((F.relabel (finCongr ⋯)).disjUnion (G.relabel (finCongr ⋯))).Equiv (((G.relabel (finCongr ⋯)).disjUnion (F.relabel (finCongr ⋯))).relabel (pairCloseSwap t))

The disjoint-union ambients of pairClose F G and pairClose G F are related by pairCloseSwap.

Equations

• F.pairCloseAmbient G = { flagEquiv := Equiv.sumComm F.Flag G.Flag, vertexEquiv := Equiv.sumComm F.Vertex G.Vertex, attach_comm := ⋯, pairing_comm := ⋯, circles_eq := ⋯ }

theorem RS.Fragment.mapPairs_pairCloseSwap_symm (t : ℕ) : mapPairs (pairCloseSwap t).symm (interfacePairs 0 t 0) = List.map Prod.swap (interfacePairs 0 t 0)

mapPairs through (pairCloseSwap t).symm on the interface pairs yields the swap of each pair.

noncomputable def RS.Fragment.pairCloseComm {t : ℕ} (F G : Fragment (Fin t)) : Equiv (pairClose F G) (pairClose G F)

Composing pairClose F G and pairClose G F yields equivalent closed fragments.

Equations

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