Interchange law of the skein category

The interchange law holds at the fragment level: tensoring two composites is equivalent to composing the two tensors. This file constructs the Fragment.Equiv witnessing

(F₁ . G₁) ⊗ (F₂ . G₂) ≃ (F₁ ⊗ F₂) . (G₁ ⊗ G₂)

by normalizing both sides to iterated gluing over the common ambient (F₁ ⊔ G₁) ⊔ (F₂ ⊔ G₂) and meeting the label chains.

noncomputable def RS.Fragment.disjUnionExchange {α β γ δ : Type} (W₁ : Fragment α) (W₂ : Fragment β) (W₃ : Fragment γ) (W₄ : Fragment δ) : ((W₁.disjUnion W₂).disjUnion (W₃.disjUnion W₄)).Equiv (((W₁.disjUnion W₃).disjUnion (W₂.disjUnion W₄)).relabel (Equiv.sumSumSumComm α γ β δ))

Four-summand exchange: (W₁ ⊔ W₂) ⊔ (W₃ ⊔ W₄) reshuffles to (W₁ ⊔ W₃) ⊔ (W₂ ⊔ W₄) up to the sumSumSumComm relabelling.

Equations

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

Interface pair splitting and ground computation

theorem RS.interchange_ground (s₁ t₁ u₁ s₂ t₂ u₂ : ℕ) : Fragment.mapPairs (((interleaveEquiv s₁ t₁ s₂ t₂).sumCongr (interleaveEquiv t₁ u₁ t₂ u₂)).symm.trans (Equiv.sumSumSumComm (Fin (s₁ + t₁)) (Fin (s₂ + t₂)) (Fin (t₁ + u₁)) (Fin (t₂ + u₂)))) (interfacePairs (s₁ + s₂) (t₁ + t₂) (u₁ + u₂)) = Fragment.inrPairs (interfacePairs s₂ t₂ u₂) ++ Fragment.inlPairs (interfacePairs s₁ t₁ u₁)

Ground computation: transporting the composition interface pairs through the interchange shuffle yields the right-block interface pairs followed by the left-block interface pairs.

theorem RS.interchangePairs_wf (s₁ t₁ u₁ s₂ t₂ u₂ : ℕ) : Fragment.PairsWF (Fragment.inlPairs (interfacePairs s₁ t₁ u₁) ++ Fragment.inrPairs (interfacePairs s₂ t₂ u₂))

The combined interface pairs of the interchange are well-formed: the inlPairs block is all Sum.inl and the inrPairs block is all Sum.inr, so they are disjoint.

LHS normalization

noncomputable def RS.Fragment.interchangeNormalLeft {s₁ t₁ u₁ s₂ t₂ u₂ : ℕ} (F₁ : Fragment (Fin (s₁ + t₁))) (G₁ : Fragment (Fin (t₁ + u₁))) (F₂ : Fragment (Fin (s₂ + t₂))) (G₂ : Fragment (Fin (t₂ + u₂))) : (tensorFragment (F₁.compose G₁) (F₂.compose G₂)).Equiv ((((F₁.disjUnion G₁).glueList (interfacePairs s₁ t₁ u₁) ⋯).disjUnion ((F₂.disjUnion G₂).glueList (interfacePairs s₂ t₂ u₂) ⋯)).relabel ((((interfaceSurvEquiv s₁ t₁ u₁).trans finSumFinEquiv).sumCongr ((interfaceSurvEquiv s₂ t₂ u₂).trans finSumFinEquiv)).trans (interleaveEquiv s₁ u₁ s₂ u₂)))

LHS chain: (F₁ . G₁) ⊗ (F₂ . G₂) normalizes to (GL₁ ⊔ GL₂).relabel L_lhs where GL_i is the glueing of the i-th factor.

Equations

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

Helper: liftPairs of inlPairs/inrPairs

RHS normalization

noncomputable def RS.Fragment.interchangeNormalRight {s₁ t₁ u₁ s₂ t₂ u₂ : ℕ} (F₁ : Fragment (Fin (s₁ + t₁))) (G₁ : Fragment (Fin (t₁ + u₁))) (F₂ : Fragment (Fin (s₂ + t₂))) (G₂ : Fragment (Fin (t₂ + u₂))) : ((tensorFragment F₁ F₂).compose (tensorFragment G₁ G₂)).Equiv ((((F₁.disjUnion G₁).glueList (interfacePairs s₁ t₁ u₁) ⋯).disjUnion ((F₂.disjUnion G₂).glueList (interfacePairs s₂ t₂ u₂) ⋯)).relabel ((((interfaceSurvEquiv s₁ t₁ u₁).trans finSumFinEquiv).sumCongr ((interfaceSurvEquiv s₂ t₂ u₂).trans finSumFinEquiv)).trans (interleaveEquiv s₁ u₁ s₂ u₂)))

RHS chain: (F₁ ⊗ F₂) . (G₁ ⊗ G₂) normalizes to (GL₁ ⊔ GL₂).relabel L_rhs.

The chain goes through composeNormal, ambient peel (exchange + relabel_disjUnion), relabel peel (glueListRelabel + mapPairs_symm_cancel), ground computation (interchange_ground), pair permutation (glueListPerm), append split (glueListAppend), and two-sided localization (glueListDisjUnionLeft + glueListDisjUnionRight).

Equations

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

Final assembly

noncomputable def RS.Fragment.tensorComposeInterchange {s₁ t₁ u₁ s₂ t₂ u₂ : ℕ} (F₁ : Fragment (Fin (s₁ + t₁))) (G₁ : Fragment (Fin (t₁ + u₁))) (F₂ : Fragment (Fin (s₂ + t₂))) (G₂ : Fragment (Fin (t₂ + u₂))) : (tensorFragment (F₁.compose G₁) (F₂.compose G₂)).Equiv ((tensorFragment F₁ F₂).compose (tensorFragment G₁ G₂))

Interchange law: tensoring two composites is equivalent to composing the two tensors.

Equations

• F₁.tensorComposeInterchange G₁ F₂ G₂ = (F₁.interchangeNormalLeft G₁ F₂ G₂).trans (F₁.interchangeNormalRight G₁ F₂ G₂).symm