Tensor commutativity and the right-slot ideal

The tensor of fragments commutes up to the block-swap relabel, so the closure rows of x ⊗ z are closure rows of z — the right-slot half of the monoidal ideal follows from the left-slot machinery through the swap.

noncomputable def RS.tensorSwapEquiv (s t u v : ℕ) : Fin (u + s + (v + t)) ≃ Fin (s + u + (t + v))

The block swap of interleaved boundaries.

Equations

• RS.tensorSwapEquiv s t u v = (RS.interleaveEquiv u v s t).symm.trans ((Equiv.sumComm (Fin (u + v)) (Fin (s + t))).trans (RS.interleaveEquiv s t u v))

noncomputable def RS.tensorFragmentComm {s t u v : ℕ} (X : Fragment (Fin (s + t))) (z : Fragment (Fin (u + v))) : (tensorFragment X z).Equiv ((tensorFragment z X).relabel (tensorSwapEquiv s t u v))

Tensor commutativity: the tensor is the swapped tensor, relabelled by the block swap.

Equations

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

theorem RS.connectionPairing_tensor_right (f : ClosedFragment → ℂ) (hf : ∀ (W₁ W₂ : ClosedFragment) (a : Fragment.Equiv W₁ W₂), f W₁ = f W₂) {s t u v : ℕ} (X : Fragment (Fin (s + t))) (z : Fragment (Fin (u + v))) (G : Fragment (Fin (s + u + (t + v)))) : connectionPairing f (s + u + (t + v)) (tensorFragment X z) G = connectionPairing f (u + v) z (partialClose X (G.relabel (tensorSwapEquiv s t u v).symm))

The closure rows of a tensor are closure rows of the second factor.

theorem RS.connectionMap_tensor_right_single (f : ClosedFragment → ℂ) (hf : ∀ (W₁ W₂ : ClosedFragment) (a : Fragment.Equiv W₁ W₂), f W₁ = f W₂) {s t u v : ℕ} (X : Fragment (Fin (s + t))) (y : Fragment (Fin (u + v)) →₀ ℂ) (K : Fragment (Fin (s + u + (t + v)))) : (connectionMap f (s + u + (t + v))) (((tensorFinsupp s t u v) (Finsupp.single X 1)) y) K = (connectionMap f (u + v)) y (partialClose X (K.relabel (tensorSwapEquiv s t u v).symm))

The connection row of a single-fragment tensor, linearized in the second slot.

theorem RS.tensorFinsupp_ker_right (f : ClosedFragment → ℂ) (hf : ∀ (W₁ W₂ : ClosedFragment) (a : Fragment.Equiv W₁ W₂), f W₁ = f W₂) {s t u v : ℕ} (x : Fragment (Fin (s + t)) →₀ ℂ) {y : Fragment (Fin (u + v)) →₀ ℂ} (hy : y ∈ (connectionMap f (u + v)).ker) : ((tensorFinsupp s t u v) x) y ∈ (connectionMap f (s + u + (t + v))).ker

The right-slot monoidal ideal: anything tensored with a kernel element stays in the kernel.