The absorption of a tensor factor into the test fragment

The accompanying paper's Lemma 3.3(b), the geometric core: closing a tensor x ⊗ z against a test fragment G is closing x against the partial closure G_z = partialClose z G. Both sides normalize to iterated gluing over the common ambient (x ⊔ z) ⊔ G: the closure pairs split into the z-blocks and the x-blocks, the z-blocks glue first (glueListAppend), localize to z ⊔ G (disjUnionAssoc + glueListDisjUnionRight), and what remains is the closure of x against the survivors — the defining gluing of partialClose.

The four closure blocks over the common ambient

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

The v-block: z's high labels against the last block of G.

Equations

• RS.zvBlock s t u v = List.map (fun (l : Fin v) => (Sum.inl (Sum.inr ⟨u + ↑l, ⋯⟩), Sum.inr ⟨s + u + (t + ↑l), ⋯⟩)) (List.finRange v).reverse

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

The t-block: x's high labels against the third block of G.

Equations

• RS.xtBlock s t u v = List.map (fun (k : Fin t) => (Sum.inl (Sum.inl ⟨s + ↑k, ⋯⟩), Sum.inr ⟨s + u + ↑k, ⋯⟩)) (List.finRange t).reverse

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

The u-block: z's low labels against the second block of G.

Equations

• RS.zuBlock s t u v = List.map (fun (j : Fin u) => (Sum.inl (Sum.inr ⟨↑j, ⋯⟩), Sum.inr ⟨s + ↑j, ⋯⟩)) (List.finRange u).reverse

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

The s-block: x's low labels against the first block of G.

Equations

• RS.xsBlock s t u v = List.map (fun (i : Fin s) => (Sum.inl (Sum.inl ⟨↑i, ⋯⟩), Sum.inr ⟨↑i, ⋯⟩)) (List.finRange s).reverse

The four-way split of the closure interface

theorem RS.ipHigh_split (s t u v : ℕ) : ipHigh (s + u) (t + v) = List.map (fun (l : Fin v) => (Sum.inl ⟨s + u + (t + ↑l), ⋯⟩, Sum.inr ⟨s + u + (t + ↑l), ⋯⟩)) (List.finRange v).reverse ++ List.map (fun (k : Fin t) => (Sum.inl ⟨s + u + ↑k, ⋯⟩, Sum.inr ⟨s + u + ↑k, ⋯⟩)) (List.finRange t).reverse

The high closure half splits at t.

theorem RS.ipLow_split (s t u v : ℕ) : ipLow (s + u) (t + v) = List.map (fun (j : Fin u) => (Sum.inl ⟨s + ↑j, ⋯⟩, Sum.inr ⟨s + ↑j, ⋯⟩)) (List.finRange u).reverse ++ List.map (fun (i : Fin s) => (Sum.inl ⟨↑i, ⋯⟩, Sum.inr ⟨↑i, ⋯⟩)) (List.finRange s).reverse

The low closure half splits at s.

The transported closure label

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

The label equivalence of the left side: interleave the tensor factors, then the closure casts.

Equations

• RS.tensorCloseLabel s t u v = ((RS.interleaveEquiv s t u v).trans (finCongr ⋯)).sumCongr (finCongr ⋯)

The ground computation: transported pairs blockwise

theorem RS.tensor_ground_pairs (s t u v : ℕ) : Fragment.mapPairs (tensorCloseLabel s t u v).symm (interfacePairs 0 (s + u + (t + v)) 0) = zvBlock s t u v ++ xtBlock s t u v ++ (zuBlock s t u v ++ xsBlock s t u v)

The transported closure pairs of the tensor side: the four blocks, in ground order.

theorem RS.perm_append_exchange {α : Type} (A B C D : List α) : (A ++ B ++ (C ++ D)).Perm (A ++ C ++ (B ++ D))

Exchanging the middle blocks of a double append.

theorem RS.tensor_pairs_perm (s t u v : ℕ) : (Fragment.mapPairs (tensorCloseLabel s t u v).symm (interfacePairs 0 (s + u + (t + v)) 0)).Perm (zvBlock s t u v ++ zuBlock s t u v ++ (xtBlock s t u v ++ xsBlock s t u v))

The tensor-side closure pairs, reordered: z-blocks first.

theorem RS.tensorPairsL_wf (s t u v : ℕ) : Fragment.PairsWF (zvBlock s t u v ++ zuBlock s t u v ++ (xtBlock s t u v ++ xsBlock s t u v))

The reordered tensor-side pairs are well-formed.

The associated ambient: pairs localize

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

The cross pairs: x's labels against the surviving x-block labels of G, inside the associated ambient.

Equations

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

theorem RS.tensor_pairs_assoc (s t u v : ℕ) : Fragment.mapPairs (Equiv.sumAssoc (Fin (s + t)) (Fin (u + v)) (Fin (s + u + (t + v)))) (zvBlock s t u v ++ zuBlock s t u v ++ (xtBlock s t u v ++ xsBlock s t u v)) = Fragment.inrPairs (zClosePairs s t u v) ++ xCrossPairs s t u v

Under the sum association, the reordered tensor pairs are the embedded z-gluing pairs followed by the cross pairs.

theorem RS.tensorPairsA_wf (s t u v : ℕ) : Fragment.PairsWF (Fragment.inrPairs (zClosePairs s t u v) ++ xCrossPairs s t u v)

The associated pair list is well-formed.

The lifted cross pairs

theorem RS.xtSurv (s t u v : ℕ) (k : Fin t) (p : (Fin (u + v) ⊕ Fin (s + u + (t + v))) × (Fin (u + v) ⊕ Fin (s + u + (t + v)))) : p ∈ zClosePairs s t u v → Sum.inr ⟨s + u + ↑k, ⋯⟩ ≠ p.1 ∧ Sum.inr ⟨s + u + ↑k, ⋯⟩ ≠ p.2

A high x-block label of G survives the z-gluing.

theorem RS.xsSurv (s t u v : ℕ) (i : Fin s) (p : (Fin (u + v) ⊕ Fin (s + u + (t + v))) × (Fin (u + v) ⊕ Fin (s + u + (t + v)))) : p ∈ zClosePairs s t u v → Sum.inr ⟨↑i, ⋯⟩ ≠ p.1 ∧ Sum.inr ⟨↑i, ⋯⟩ ≠ p.2

A low x-block label of G survives the z-gluing.

noncomputable def RS.xLiftedPairs (s t u v : ℕ) : List ((Fin (s + t) ⊕ Fragment.FoldSurviving (Fin (u + v) ⊕ Fin (s + u + (t + v))) (zClosePairs s t u v)) × (Fin (s + t) ⊕ Fragment.FoldSurviving (Fin (u + v) ⊕ Fin (s + u + (t + v))) (zClosePairs s t u v)))

The canonical cross pairs after the z-gluing: x's labels against the surviving x-block labels of G.

Equations

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

theorem RS.lift_pull (s t u v : ℕ) (h : Fragment.PairsSepAll (Fragment.inrPairs (zClosePairs s t u v)) (xCrossPairs s t u v)) : Fragment.mapPairs (Fragment.inrFoldEquiv (zClosePairs s t u v)) (Fragment.liftPairs (Fragment.inrPairs (zClosePairs s t u v)) (xCrossPairs s t u v) h) = xLiftedPairs s t u v

Pulling the lifted cross pairs through the right-embedding survivor equivalence gives the canonical cross pairs.

The right side's transported closure label

noncomputable def RS.pcCloseLabel (s t u v : ℕ) : Fin (s + t) ⊕ Fragment.FoldSurviving (Fin (u + v) ⊕ Fin (s + u + (t + v))) (zClosePairs s t u v) ≃ Fin (0 + (s + t)) ⊕ Fin (s + t + 0)

The label equivalence of the right side: the partial-closure survivor identification, then the closure casts.

Equations

• RS.pcCloseLabel s t u v = (finCongr ⋯).sumCongr ((RS.pcSurvEquiv s t u v).trans (finCongr ⋯))

theorem RS.pcSurvEquiv_symm_high_val (s t u v : ℕ) (k : Fin t) (h : s + ↑k < s + t) : ↑((pcSurvEquiv s t u v).symm ⟨s + ↑k, h⟩) = Sum.inr ⟨s + u + ↑k, ⋯⟩

The inverse survivor identification on high labels.

theorem RS.pcSurvEquiv_symm_low_val (s t u v : ℕ) (i : Fin s) (h : ↑i < s + t) : ↑((pcSurvEquiv s t u v).symm ⟨↑i, h⟩) = Sum.inr ⟨↑i, ⋯⟩

The inverse survivor identification on low labels.

The right side's ground computation

theorem RS.rhs_ground_pairs (s t u v : ℕ) : Fragment.mapPairs (pcCloseLabel s t u v).symm (interfacePairs 0 (s + t) 0) = xLiftedPairs s t u v

The right side's closure pairs are the canonical cross pairs.

noncomputable def RS.absQsR (s t u v : ℕ) : List ((Fin (s + t) ⊕ Fragment.FoldSurviving (Fin (u + v) ⊕ Fin (s + u + (t + v))) (zClosePairs s t u v)) × (Fin (s + t) ⊕ Fragment.FoldSurviving (Fin (u + v) ⊕ Fin (s + u + (t + v))) (zClosePairs s t u v)))

The right side's transported closure pairs.

Equations

• RS.absQsR s t u v = RS.Fragment.mapPairs (RS.pcCloseLabel s t u v).symm (RS.interfacePairs 0 (s + t) 0)

theorem RS.xLiftedPairs_wf (s t u v : ℕ) : Fragment.PairsWF (xLiftedPairs s t u v)

The canonical cross pairs are well-formed.

The right side, normalized

noncomputable def RS.absLabelR (s t u v : ℕ) : Fragment.FoldSurviving (Fin (s + t) ⊕ Fragment.FoldSurviving (Fin (u + v) ⊕ Fin (s + u + (t + v))) (zClosePairs s t u v)) (xLiftedPairs s t u v) ≃ Fin (0 + 0)

The composed label identification of the right side.

Equations

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

noncomputable def RS.absNormalRight {s t u v : ℕ} (X : Fragment (Fin (s + t))) (z : Fragment (Fin (u + v))) (G : Fragment (Fin (s + u + (t + v)))) : Fragment.Equiv (pairClose X (partialClose z G)) (((X.disjUnion ((z.disjUnion G).glueList (zClosePairs s t u v) ⋯)).glueList (xLiftedPairs s t u v) ⋯).relabel (absLabelR s t u v))

The right side, normalized: the closure of x against the partial closure is iterated gluing of the canonical cross pairs over x ⊔ (glued z ⊔ G).

Equations

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

The left side's derived pair lists

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

The left side's transported closure pairs.

Equations

• RS.absQsL s t u v = RS.Fragment.mapPairs (RS.tensorCloseLabel s t u v).symm (RS.interfacePairs 0 (s + u + (t + v)) 0)

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

The reordered pairs, pulled back through the association.

Equations

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

theorem RS.abs_assoc' (s t u v : ℕ) : absPs1 s t u v = Fragment.inrPairs (zClosePairs s t u v) ++ xCrossPairs s t u v

The pulled-back pairs are the localized pairs.

noncomputable def RS.absQsLift (s t u v : ℕ) : List (Fragment.FoldSurviving (Fin (s + t) ⊕ Fin (u + v) ⊕ Fin (s + u + (t + v))) (Fragment.inrPairs (zClosePairs s t u v)) × Fragment.FoldSurviving (Fin (s + t) ⊕ Fin (u + v) ⊕ Fin (s + u + (t + v))) (Fragment.inrPairs (zClosePairs s t u v)))

The lifted cross pairs of the two-stage fold.

Equations

• RS.absQsLift s t u v = RS.Fragment.liftPairs (RS.Fragment.inrPairs (RS.zClosePairs s t u v)) (RS.xCrossPairs s t u v) ⋯

noncomputable def RS.absPs0 (s t u v : ℕ) : List ((Fin (s + t) ⊕ Fragment.FoldSurviving (Fin (u + v) ⊕ Fin (s + u + (t + v))) (zClosePairs s t u v)) × (Fin (s + t) ⊕ Fragment.FoldSurviving (Fin (u + v) ⊕ Fin (s + u + (t + v))) (zClosePairs s t u v)))

The lifted cross pairs, pulled back through the embedding survivor equivalence.

Equations

• RS.absPs0 s t u v = RS.Fragment.mapPairs (RS.Fragment.inrFoldEquiv (RS.zClosePairs s t u v)).symm.symm (RS.absQsLift s t u v)

theorem RS.abs_lift_pull (s t u v : ℕ) : absPs0 s t u v = xLiftedPairs s t u v

The pulled-back lifted pairs are the canonical cross pairs.

The left side, normalized

noncomputable def RS.absLabelL (s t u v : ℕ) : Fragment.FoldSurviving (Fin (s + t) ⊕ Fragment.FoldSurviving (Fin (u + v) ⊕ Fin (s + u + (t + v))) (zClosePairs s t u v)) (xLiftedPairs s t u v) ≃ Fin (0 + 0)

The composed label identification of the left side.

Equations

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

theorem RS.absorptionPairs_wf (s t u v : ℕ) : Fragment.PairsWF (absPs0 s t u v)

The pulled-back absorption pairs form a well-formed gluing list.

noncomputable def RS.absNormalLeft {s t u v : ℕ} (X : Fragment (Fin (s + t))) (z : Fragment (Fin (u + v))) (G : Fragment (Fin (s + u + (t + v)))) : Fragment.Equiv (pairClose (tensorFragment X z) G) (((X.disjUnion ((z.disjUnion G).glueList (zClosePairs s t u v) ⋯)).glueList (xLiftedPairs s t u v) ⋯).relabel (absLabelL s t u v))

The left side, normalized: the closure of the tensor against G is iterated gluing of the canonical cross pairs over x ⊔ (glued z ⊔ G).

Equations

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

The meet: no label survives a full closure

theorem RS.absSurv_empty (s t u v : ℕ) (x : Fragment.FoldSurviving (Fin (s + t) ⊕ Fragment.FoldSurviving (Fin (u + v) ⊕ Fin (s + u + (t + v))) (zClosePairs s t u v)) (xLiftedPairs s t u v)) : False

The canonical cross pairs glue every label: no survivor.

noncomputable def RS.pairCloseTensorAbsorb {s t u v : ℕ} (X : Fragment (Fin (s + t))) (z : Fragment (Fin (u + v))) (G : Fragment (Fin (s + u + (t + v)))) : Fragment.Equiv (pairClose (tensorFragment X z) G) (pairClose X (partialClose z G))

The absorption (accompanying paper, Lemma 3.3(b), geometric core): closing a tensor against a test fragment is closing the first factor against the partial closure of the second.

Equations

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

The monoidal ideal (accompanying paper, Lemma 3.3(b))

theorem RS.connectionPairing_tensor (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 (s + t) X (partialClose z G)

The connection row of a tensor is a connection row of the first factor at the partially closed test fragment.

noncomputable def RS.tensorFinsupp (s t u v : ℕ) : (Fragment (Fin (s + t)) →₀ ℂ) →ₗ[ℂ] (Fragment (Fin (u + v)) →₀ ℂ) →ₗ[ℂ] Fragment (Fin (s + u + (t + v))) →₀ ℂ

Bilinear tensor on the free modules of fragments.

Equations

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

theorem RS.tensorFinsupp_single (s t u v : ℕ) (F : Fragment (Fin (s + t))) (c : ℂ) (z : Fragment (Fin (u + v))) (d : ℂ) : ((tensorFinsupp s t u v) (Finsupp.single F c)) (Finsupp.single z d) = Finsupp.single (tensorFragment F z) (c * d)

Tensor of weighted single fragments.

theorem RS.connectionMap_tensor_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)) →₀ ℂ) (z : Fragment (Fin (u + v))) (K : Fragment (Fin (s + u + (t + v)))) : (connectionMap f (s + u + (t + v))) (((tensorFinsupp s t u v) x) (Finsupp.single z 1)) K = (connectionMap f (s + t)) x (partialClose z K)

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

theorem RS.tensorFinsupp_single_ker (f : ClosedFragment → ℂ) (hf : ∀ (W₁ W₂ : ClosedFragment) (a : Fragment.Equiv W₁ W₂), f W₁ = f W₂) {s t u v : ℕ} {x : Fragment (Fin (s + t)) →₀ ℂ} (hx : x ∈ (connectionMap f (s + t)).ker) (z : Fragment (Fin (u + v))) : ((tensorFinsupp s t u v) x) (Finsupp.single z 1) ∈ (connectionMap f (s + u + (t + v))).ker

A kernel element tensored with a single fragment stays in the kernel.

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

The monoidal ideal (accompanying paper, Lemma 3.3(b)): a kernel element tensored with anything stays in the kernel.