Partial closure of a tensor

partialClose z (X' ⊗ z') glues z's ends onto the z-block of the tensor — which is exactly z''s boundary. The result is X' sitting untouched next to the full closure of z against z':

partialClose z (X' ⊗ z') ≃ X' ⊔ pairClose z z'.

This is the engine of the trace multiplicativity (Lemma 3.5(b)): with X' := strandBundle a, z' := strandBundle b and strandBundleTensor, the trace of a tensor splits.

This file: the three-summand shuffle, the ground computation (the z-gluing pairs localize to the z, z' summands), and the inner-pair identification.

def RS.sumShuffleEquiv (α β γ : Type) : β ⊕ α ⊕ γ ≃ α ⊕ β ⊕ γ

The three-summand shuffle: pull the middle summand out front.

Equations

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

noncomputable def RS.disjUnionShuffle {α β γ : Type} (W₁ : Fragment α) (W₂ : Fragment β) (W₃ : Fragment γ) : (W₁.disjUnion (W₂.disjUnion W₃)).Equiv ((W₂.disjUnion (W₁.disjUnion W₃)).relabel (sumShuffleEquiv α β γ))

The disjoint union shuffles: the middle factor pulls out front, up to the shuffle relabelling.

Equations

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

The localized inner pairs

def RS.innerClosePairs (u v : ℕ) : List ((Fin (u + v) ⊕ Fin (u + v)) × (Fin (u + v) ⊕ Fin (u + v)))

The closure pairs of z against z', over the pair of (u + v)-boundaries: high block, then low block.

Equations

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

The ground computation: peeling the interleave

theorem RS.pc_tensor_ground (s t u v : ℕ) : Fragment.mapPairs ((Equiv.refl (Fin (u + v))).sumCongr (interleaveEquiv s t u v)).symm (zClosePairs s t u v) = Fragment.mapPairs (sumShuffleEquiv (Fin (u + v)) (Fin (s + t)) (Fin (u + v))) (Fragment.inrPairs (innerClosePairs u v))

Peeling the interleave from the z-gluing pairs localizes them to the z, z' summands.

The inner closure, normalized

noncomputable def RS.innerCloseLabel (u v : ℕ) : Fin (u + v) ⊕ Fin (u + v) ≃ Fin (0 + (u + v)) ⊕ Fin (u + v + 0)

The closure label of the inner pair: the two closure casts.

Equations

• RS.innerCloseLabel u v = (finCongr ⋯).sumCongr (finCongr ⋯)

theorem RS.inner_ground (u v : ℕ) : Fragment.mapPairs (innerCloseLabel u v).symm (interfacePairs 0 (u + v) 0) = innerClosePairs u v

The transported closure pairs of the inner closure are the inner pairs.

theorem RS.innerClosePairs_wf (u v : ℕ) : Fragment.PairsWF (innerClosePairs u v)

The inner pairs are well-formed.

noncomputable def RS.innerQs (u v : ℕ) : List ((Fin (u + v) ⊕ Fin (u + v)) × (Fin (u + v) ⊕ Fin (u + v)))

The transported inner closure pairs.

Equations

• RS.innerQs u v = RS.Fragment.mapPairs (RS.innerCloseLabel u v).symm (RS.interfacePairs 0 (u + v) 0)

noncomputable def RS.innerLabel (u v : ℕ) : Fragment.FoldSurviving (Fin (u + v) ⊕ Fin (u + v)) (innerClosePairs u v) ≃ Fin (0 + 0)

The composed label identification of the inner closure.

Equations

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

noncomputable def RS.innerNormal {u v : ℕ} (z z' : Fragment (Fin (u + v))) : Fragment.Equiv (pairClose z z') (((z.disjUnion z').glueList (innerClosePairs u v) ⋯).relabel (innerLabel u v))

The inner closure, normalized: the closure of z against z' is iterated gluing of the inner pairs over z ⊔ z'.

Equations

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

The main chain

noncomputable def RS.pcTensorClose (s t : ℕ) : Fin (s + t) ⊕ Fin (0 + 0) ≃ Fin (s + t)

The clean label of the partial closure of a tensor.

Equations

• RS.pcTensorClose s t = ((Equiv.refl (Fin (s + t))).sumCongr (finCongr RS.pcTensorClose._proof_2)).trans (Equiv.sumEmpty (Fin (s + t)) (Fin 0))

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

The interleave peel of the z-gluing ambient.

Equations

• RS.pcTensorPeel s t u v = (Equiv.refl (Fin (u + v))).sumCongr (RS.interleaveEquiv s t u v)

noncomputable def RS.pcTensorQs (s t u v : ℕ) : List ((Fin (u + v) ⊕ Fin (s + t) ⊕ Fin (u + v)) × (Fin (u + v) ⊕ Fin (s + t) ⊕ Fin (u + v)))

The peeled z-gluing pairs.

Equations

• RS.pcTensorQs s t u v = RS.Fragment.mapPairs (RS.pcTensorPeel s t u v).symm (RS.zClosePairs s t u v)

theorem RS.pcTensorPairs_wf (s t u v : ℕ) : Fragment.PairsWF (pcTensorQs s t u v)

The pairs pulled back through the tensor peel are well formed.

noncomputable def RS.pcTensorLabel (s t u v : ℕ) : Fin (s + t) ⊕ Fin (0 + 0) ≃ Fin (s + t)

The composed label identification of the partial closure of a tensor.

Equations

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

noncomputable def RS.pcTensorNormal {s t u v : ℕ} (z : Fragment (Fin (u + v))) (X' : Fragment (Fin (s + t))) (z' : Fragment (Fin (u + v))) : (partialClose z (tensorFragment X' z')).Equiv ((X'.disjUnion (pairClose z z')).relabel (pcTensorLabel s t u v))

The partial closure of a tensor, normalized: X' next to the inner closure, up to the composed label.

Equations

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

The label meet

theorem RS.pcSurvEquiv_val_low (s t u v : ℕ) (b : Fin (s + u + (t + v))) (hsurv : ∀ p ∈ zClosePairs s t u v, Sum.inr b ≠ p.1 ∧ Sum.inr b ≠ p.2) (hb : ↑b < s) : (pcSurvEquiv s t u v) ⟨Sum.inr b, hsurv⟩ = ⟨↑b, ⋯⟩

The forward survivor identification on low labels.

theorem RS.pcSurvEquiv_val_high (s t u v : ℕ) (b : Fin (s + u + (t + v))) (hsurv : ∀ p ∈ zClosePairs s t u v, Sum.inr b ≠ p.1 ∧ Sum.inr b ≠ p.2) (hb : ¬↑b < s) (h1 : s + u ≤ ↑b) (h2 : ↑b < s + u + t) : (pcSurvEquiv s t u v) ⟨Sum.inr b, hsurv⟩ = ⟨s + (↑b - (s + u)), ⋯⟩

The forward survivor identification on high labels.

theorem RS.pcTensorLabel_eq (s t u v : ℕ) : pcTensorLabel s t u v = pcTensorClose s t

The composed label is the clean label: the live value chase on the surviving x-labels.

noncomputable def RS.partialCloseTensor {s t u v : ℕ} (z : Fragment (Fin (u + v))) (X' : Fragment (Fin (s + t))) (z' : Fragment (Fin (u + v))) : (partialClose z (tensorFragment X' z')).Equiv ((X'.disjUnion (pairClose z z')).relabel (pcTensorClose s t))

The partial closure of a tensor: X' unscathed next to the full closure of z against z'.

Equations

• RS.partialCloseTensor z X' z' = (RS.pcTensorNormal z X' z').trans (RS.Fragment.Equiv.relabelEq (X'.disjUnion (RS.pairClose z z')) ⋯)