The bundle-map calculus

The strand bundle implementing an arbitrary label equivalence e : Fin n ≃ Fin m: strand k runs from input k to output e k. These fragments and their Hom classes provide all the structural morphisms of the monoidal skein category — associators and unitors (e a cast) and the braiding (e a block transpose) — and satisfy a single composition law: composing the bundle maps of e₁ and e₂ is the bundle map of e₁.trans e₂. The proof forces the arities equal (a Fin-equivalence fixes the cardinality), after which everything is permutation-fragment algebra. Every coherence diagram of the monoidal assembly collapses through this law into an equality of label equivalences.

def RS.outMapEquiv {n m : ℕ} (e : Fin n ≃ Fin m) : Fin (n + n) ≃ Fin (n + m)

The outgoing label map of a bundle: fix the inputs, apply e to the outputs.

Equations

• RS.outMapEquiv e = finSumFinEquiv.symm.trans (((Equiv.refl (Fin n)).sumCongr e).trans finSumFinEquiv)

noncomputable def RS.bundleMap {n m : ℕ} (e : Fin n ≃ Fin m) : Fragment (Fin (n + m))

The bundle map of a label equivalence: strand k joins input k to output e k.

Equations

• RS.bundleMap e = (RS.strandBundle n).relabel (RS.outMapEquiv e)

noncomputable def RS.bundleMapRefl (n : ℕ) : (bundleMap (Equiv.refl (Fin n))).Equiv (strandBundle n)

The bundle map of the identity is the strand bundle.

Equations

• RS.bundleMapRefl n = (RS.Fragment.Equiv.relabelEq (RS.strandBundle n) ⋯).trans (RS.Fragment.Equiv.relabelRefl (RS.strandBundle n))

noncomputable def RS.bundleMapComp {n m p : ℕ} (e₁ : Fin n ≃ Fin m) (e₂ : Fin m ≃ Fin p) : ((bundleMap e₁).compose (bundleMap e₂)).Equiv (bundleMap (e₁.trans e₂))

The composition law of bundle maps.

Equations

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

noncomputable def RS.tensorFragmentRelabel {s t u v s' t' u' v' : ℕ} (X : Fragment (Fin (s + t))) (z : Fragment (Fin (u + v))) (r₁ : Fin (s + t) ≃ Fin (s' + t')) (r₂ : Fin (u + v) ≃ Fin (u' + v')) : (tensorFragment (X.relabel r₁) (z.relabel r₂)).Equiv ((tensorFragment X z).relabel ((interleaveEquiv s t u v).symm.trans ((r₁.sumCongr r₂).trans (interleaveEquiv s' t' u' v'))))

Tensoring relabelled fragments is relabelling the tensor by the interleave-conjugated sum.

Equations

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

theorem RS.outMapEquiv_castAdd {n m : ℕ} (e : Fin n ≃ Fin m) (i : Fin n) : (outMapEquiv e) (Fin.castAdd n i) = Fin.castAdd m i

The outgoing map fixes input slots.

theorem RS.outMapEquiv_natAdd {n m : ℕ} (e : Fin n ≃ Fin m) (k : Fin n) : (outMapEquiv e) (Fin.natAdd n k) = Fin.natAdd n (e k)

The outgoing map acts on output slots.

def RS.tensorMapEquiv {n₁ m₁ n₂ m₂ : ℕ} (e₁ : Fin n₁ ≃ Fin m₁) (e₂ : Fin n₂ ≃ Fin m₂) : Fin (n₁ + n₂) ≃ Fin (m₁ + m₂)

The sum of two label equivalences, on concatenated blocks.

Equations

• RS.tensorMapEquiv e₁ e₂ = finSumFinEquiv.symm.trans ((e₁.sumCongr e₂).trans finSumFinEquiv)

theorem RS.tensorMapEquiv_castAdd {n₁ m₁ n₂ m₂ : ℕ} (e₁ : Fin n₁ ≃ Fin m₁) (e₂ : Fin n₂ ≃ Fin m₂) (i : Fin n₁) : (tensorMapEquiv e₁ e₂) (Fin.castAdd n₂ i) = Fin.castAdd m₂ (e₁ i)

The tensor of two label equivalences on a left label.

theorem RS.tensorMapEquiv_natAdd {n₁ m₁ n₂ m₂ : ℕ} (e₁ : Fin n₁ ≃ Fin m₁) (e₂ : Fin n₂ ≃ Fin m₂) (j : Fin n₂) : (tensorMapEquiv e₁ e₂) (Fin.natAdd n₁ j) = Fin.natAdd m₁ (e₂ j)

And on a right label.

noncomputable def RS.bundleMapTensor {n₁ m₁ n₂ m₂ : ℕ} (e₁ : Fin n₁ ≃ Fin m₁) (e₂ : Fin n₂ ≃ Fin m₂) : (tensorFragment (bundleMap e₁) (bundleMap e₂)).Equiv (bundleMap (tensorMapEquiv e₁ e₂))

The tensor law of bundle maps: the tensor of two bundle maps is the bundle map of the block sum.

Equations

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

noncomputable def RS.composeBundleMap {s n m : ℕ} (e : Fin n ≃ Fin m) (F : Fragment (Fin (s + n))) : (F.compose (bundleMap e)).Equiv (F.relabel (finSumFinEquiv.symm.trans (((Equiv.refl (Fin s)).sumCongr e).trans finSumFinEquiv)))

Composing with a bundle map on the right relabels the outgoing boundary.

Equations

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

noncomputable def RS.bundleMapCompose {n m u : ℕ} (e : Fin n ≃ Fin m) (F : Fragment (Fin (m + u))) : ((bundleMap e).compose F).Equiv (F.relabel (finSumFinEquiv.symm.trans ((e.symm.sumCongr (Equiv.refl (Fin u))).trans finSumFinEquiv)))

Composing with a bundle map on the left relabels the incoming boundary by the inverse.

Equations

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

theorem RS.outTransport_finCongr {s n m : ℕ} (h : n = m) : finSumFinEquiv.symm.trans (((Equiv.refl (Fin s)).sumCongr (finCongr h)).trans finSumFinEquiv) = finCongr ⋯

The outgoing transport of a cast is a cast.

theorem RS.inTransport_finCongr {n m u : ℕ} (h : n = m) : finSumFinEquiv.symm.trans (((finCongr h).sumCongr (Equiv.refl (Fin u))).trans finSumFinEquiv) = finCongr ⋯

The incoming transport of a cast is a cast.

noncomputable def RS.bundleMapClass {R : ℕ} (f : EdgeRankParameter R) {n m : ℕ} (e : Fin n ≃ Fin m) : HomSpace f.val (n + m)

The bundle-map class.

Equations

• RS.bundleMapClass f e = RS.HomSpace.ofFragment f.val (RS.bundleMap e)

theorem RS.bundleMapClass_refl {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) : bundleMapClass f (Equiv.refl (Fin n)) = HomSpace.ofFragment f.val (strandBundle n)

The class of the identity bundle map is the identity class.

theorem RS.bundleMapClass_comp {R : ℕ} (f : EdgeRankParameter R) {n m p : ℕ} (e₁ : Fin n ≃ Fin m) (e₂ : Fin m ≃ Fin p) : ((HomSpace.comp f n m p) (bundleMapClass f e₁)) (bundleMapClass f e₂) = bundleMapClass f (e₁.trans e₂)

Composition of bundle-map classes.

theorem RS.bundleMapClass_congr {R : ℕ} (f : EdgeRankParameter R) {n m : ℕ} {e₁ e₂ : Fin n ≃ Fin m} (h : e₁ = e₂) : bundleMapClass f e₁ = bundleMapClass f e₂

Congruent label equivalences give equal classes.