Closure against a fragment with a closed attachment

A closed component riding along the test fragment falls out of the closure as a disjoint union:

pairClose F ((H ⊔ C) · clean) ≃ (pairClose F H) ∪ C.

Combined with partialCloseTensor, strandBundleTensor and the multiplicativity of the parameter (Lemma 3.2), this yields the trace multiplicativity (Lemma 3.5(b)).

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

The peel of the union closure: the closure casts against the clean label.

Equations

• RS.unionPeel s t = (finCongr ⋯).sumCongr ((RS.pcTensorClose s t).trans (finCongr ⋯))

noncomputable def RS.unionQs (s t : ℕ) : List ((Fin (s + t) ⊕ Fin (s + t) ⊕ Fin (0 + 0)) × (Fin (s + t) ⊕ Fin (s + t) ⊕ Fin (0 + 0)))

The peeled union-closure pairs.

Equations

• RS.unionQs s t = RS.Fragment.mapPairs (RS.unionPeel s t).symm (RS.interfacePairs 0 (s + t) 0)

theorem RS.union_ground (s t : ℕ) : Fragment.mapPairs (unionPeel s t).symm (interfacePairs 0 (s + t) 0) = Fragment.mapPairs (Equiv.sumAssoc (Fin (s + t)) (Fin (s + t)) (Fin (0 + 0))).symm.symm (Fragment.inlPairs (innerClosePairs s t))

The peeled union-closure pairs are the associated embedding of the inner closure pairs.

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

The composed label identification of the union closure.

Equations

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

noncomputable def RS.unionNormal {s t : ℕ} (F H : Fragment (Fin (s + t))) (C : ClosedFragment) : Fragment.Equiv (pairClose F ((H.disjUnion C).relabel (pcTensorClose s t))) ((Fragment.disjUnion (pairClose F H) C).relabel (unionLabel s t))

The union closure, normalized.

Equations

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

noncomputable def RS.pairCloseUnionRight {s t : ℕ} (F H : Fragment (Fin (s + t))) (C : ClosedFragment) : Fragment.Equiv (pairClose F ((H.disjUnion C).relabel (pcTensorClose s t))) ((pairClose F H).union C)

The union closure (closed components fall out): closing against a test fragment with a closed attachment is the union of the closure with the attachment.

Equations

• RS.pairCloseUnionRight F H C = (RS.unionNormal F H C).trans (RS.Fragment.Equiv.relabelEq (RS.Fragment.disjUnion (RS.pairClose F H) C) ⋯)

theorem RS.fragTrace_tensor {R : ℕ} (f : EdgeRankParameter R) {a b : ℕ} (F₁ : Fragment (Fin (a + a))) (F₂ : Fragment (Fin (b + b))) : fragTrace f.val (tensorFragment F₁ F₂) = fragTrace f.val F₁ * fragTrace f.val F₂

Trace multiplicativity (accompanying paper, Lemma 3.5(b)): the trace of a tensor is the product of the traces.