Peeling the bundle cap

The strand-bundle cap on m + 1 strands factors as the cap on m strands tensored with a single evaluation, composed with the rotation that moves the last strand's two ends to the end of the boundary word. This is the recursion that computes the cap functional in coordinates.

def RS.capPeelFun (m j : ℕ) : ℕ

The peel rotation, on values.

Equations

• RS.capPeelFun m j = if j < m then j else if j = m then m + m else if j ≤ m + m then j - 1 else j

def RS.capPeelInv (m j : ℕ) : ℕ

The inverse peel rotation, on values.

Equations

• RS.capPeelInv m j = if j < m then j else if j = m + m then m else if j < m + m then j + 1 else j

def RS.capPeelRotation (m : ℕ) : Fin (m + 1 + (m + 1)) ≃ Fin (m + m + 2)

The peel rotation: move the last strand's ends to the end.

Equations

• RS.capPeelRotation m = { toFun := fun (i : Fin (m + 1 + (m + 1))) => ⟨RS.capPeelFun m ↑i, ⋯⟩, invFun := fun (j : Fin (m + m + 2)) => ⟨RS.capPeelInv m ↑j, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem RS.capPeel_inTransport_val (m : ℕ) (ℓ : Fin (m + m + 2 + 0)) : ↑((finSumFinEquiv.symm.trans (((capPeelRotation m).symm.sumCongr (Equiv.refl (Fin 0))).trans finSumFinEquiv)) ℓ) = capPeelInv m ↑ℓ

The incoming transport of the peel evaluates by the inverse rotation.

def RS.capPeelFlagFun (m : ℕ) : Fin (m + 1) × Bool → Fin m × Bool ⊕ Fin 2

The peel flag map.

Equations

• RS.capPeelFlagFun m g = if h : ↑g.1 < m then Sum.inl (⟨↑g.1, h⟩, g.2) else Sum.inr (if g.2 = true then 1 else 0)

def RS.capPeelFlagInv (m : ℕ) : Fin m × Bool ⊕ Fin 2 → Fin (m + 1) × Bool

The inverse peel flag map.

Equations

• RS.capPeelFlagInv m (Sum.inl (j, b)) = (⟨↑j, ⋯⟩, b)
• RS.capPeelFlagInv m (Sum.inr t) = (⟨m, ⋯⟩, decide (↑t = 1))

def RS.capPeelFlagEquiv (m : ℕ) : Fin (m + 1) × Bool ≃ Fin m × Bool ⊕ Fin 2

The peel flag equivalence.

Equations

• RS.capPeelFlagEquiv m = { toFun := RS.capPeelFlagFun m, invFun := RS.capPeelFlagInv m, left_inv := ⋯, right_inv := ⋯ }

theorem RS.capPeel_interleave_left_val (m X : ℕ) (h : X < m + m + 0) : ↑((interleaveEquiv (m + m) 0 2 0) (Sum.inl ⟨X, h⟩)) = X

Interleave value on the cap side.

theorem RS.capPeel_interleave_right_val (m X : ℕ) (h : X < 2 + 0) : ↑((interleaveEquiv (m + m) 0 2 0) (Sum.inr ⟨X, h⟩)) = m + m + X

Interleave value on the evaluation side.

noncomputable def RS.capPeelEquiv (m : ℕ) : ((strandBundle (m + 1)).relabel (finCongr ⋯)).Equiv ((tensorFragment ((strandBundle m).relabel (finCongr ⋯)) (Fragment.strand.relabel (finCongr capPeelEquiv._proof_3))).relabel (finSumFinEquiv.symm.trans (((capPeelRotation m).symm.sumCongr (Equiv.refl (Fin 0))).trans finSumFinEquiv)))

The cap peel equivalence: the padded bundle cap on m + 1 strands is the tensor of the cap on m strands with one evaluation, relabelled along the peel rotation.

Equations

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

theorem RS.bundleCapClass_peel {R : ℕ} (f : EdgeRankParameter R) (m : ℕ) : bundleCapClass f (m + 1) = ((HomSpace.comp f (m + 1 + (m + 1)) (m + m + 2) 0) (bundleMapClass f (capPeelRotation m))) (((HomSpace.tensor f (m + m) 0 2 0) (bundleCapClass f m)) (evClass f))

The cap peel: the bundle cap on m + 1 strands is the peel rotation composed with the cap on m strands tensored with one evaluation.