Cyclicity of the trace

The trace of a composition is independent of the order (fragTrace_comm, accompanying paper, Lemma 3.5(a)): closing F ∘ G by the strand bundle and closing G ∘ F by the strand bundle produce isomorphic closed fragments. Both reduce, by the rotation (pairCloseComposeRotate) and the identity law (composeStrandBundleLeft), to the closure of F against a transposed copy of G; the two reductions are matched by the commutativity of the closure and the closure-relabel exchange (pairCloseRelabel), itself derived from interfaceShift at s = 0, where the outgoing block is the entire boundary.

theorem RS.transposeEquiv_symm (n p : ℕ) : (transposeEquiv n p).symm = transposeEquiv p n

The inverse of the transpose is the reverse transpose.

noncomputable def RS.pairCloseCongr {t : ℕ} {F₁ F₂ G₁ G₂ : Fragment (Fin t)} (hF : F₁.Equiv F₂) (hG : G₁.Equiv G₂) : Fragment.Equiv (pairClose F₁ G₁) (pairClose F₂ G₂)

The closure respects fragment equivalence in both slots.

Equations

• RS.pairCloseCongr hF hG = RS.Fragment.composeCongr (hF.relabelCongr (finCongr ⋯)) (hG.relabelCongr (finCongr ⋯))

theorem RS.cast_trans_outPerm {t : ℕ} (e : Equiv.Perm (Fin t)) : Equiv.trans e (finCongr ⋯) = (finCongr ⋯).trans (outPermEquiv 0 e)

Label algebra: post-composing a boundary permutation with the low cast is pre-composing the cast with the outgoing permutation at s = 0.

theorem RS.cast_trans_inPerm {t : ℕ} (e : Equiv.Perm (Fin t)) : (Equiv.symm e).trans (finCongr ⋯) = (finCongr ⋯).trans (inPermEquiv (Equiv.symm e) 0)

Label algebra: post-composing the inverse boundary permutation with the high cast is pre-composing the cast with the incoming permutation at u = 0.

noncomputable def RS.pairCloseRelabelPerm {t : ℕ} (e : Equiv.Perm (Fin t)) (X Y : Fragment (Fin t)) : Fragment.Equiv (pairClose (X.relabel e) Y) (pairClose X (Y.relabel (Equiv.symm e)))

The closure-relabel exchange for boundary permutations: relabelling the first factor of a closure by a permutation is relabelling the second by the inverse. Instance of interfaceShift at s = 0, where the outgoing block is the whole boundary.

Equations

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

noncomputable def RS.pairCloseCast {a b : ℕ} (h : a = b) (X : Fragment (Fin a)) (Y : Fragment (Fin b)) : Fragment.Equiv (pairClose (X.relabel (finCongr h)) Y) (pairClose X (Y.relabel (finCongr ⋯)))

The closure-relabel exchange across a pure cast.

Equations

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

noncomputable def RS.pairCloseRelabel {a b : ℕ} (e : Fin a ≃ Fin b) (X : Fragment (Fin a)) (Y : Fragment (Fin b)) : Fragment.Equiv (pairClose (X.relabel e) Y) (pairClose X (Y.relabel e.symm))

The closure-relabel exchange: relabelling the first factor of a closure is relabelling the second factor by the inverse label equivalence.

Equations

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

theorem RS.fragTrace_comm (f : ClosedFragment → ℂ) (hf : ∀ (W₁ W₂ : ClosedFragment) (a : Fragment.Equiv W₁ W₂), f W₁ = f W₂) {t u : ℕ} (F : Fragment (Fin (t + u))) (G : Fragment (Fin (u + t))) : fragTrace f (F.compose G) = fragTrace f (G.compose F)

Cyclicity of the trace (accompanying paper, Lemma 3.5(a)): for an isomorphism-invariant parameter, the trace of a composition does not depend on the order of the factors.