The disjoint union: canonical migration #
Migrating canonical data between a union and its components.
The canonical-value migration #
The corrected (canonical) constrained value pins a path-canonical orientation and weights it by the Pfaffian chord-diagram sign. The factorization migrates: the product of two path-canonical component orientations is path-canonical for the union (chains stay componentwise), and cross-component chords never interleave under any order placing every left label below every right label, so the crossing count — hence the path sign — is additive.
Boundary membership over the union #
theorem
RS.inl_mem_boundary
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{g : W₁.Flag}
:
Being a boundary flag is componentwise on the left.
theorem
RS.inr_mem_boundary
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{g : W₂.Flag}
:
And on the right.
The path match of the product system is componentwise #
theorem
RS.pathMatch_prodRel_inl
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
(κ₁ : (leftSub F).RelTransitionSystem)
(κ₂ : (rightSub F).RelTransitionSystem)
{g : W₁.Flag}
(hb : Sum.inl g ∈ F.boundaryFlags)
(hb' : g ∈ (leftSub F).boundaryFlags)
:
A left boundary flag's chain stays left, so the product system's path matching is the left component's.
theorem
RS.pathMatch_prodRel_inr
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
(κ₁ : (leftSub F).RelTransitionSystem)
(κ₂ : (rightSub F).RelTransitionSystem)
{g : W₂.Flag}
(hb : Sum.inr g ∈ F.boundaryFlags)
(hb' : g ∈ (rightSub F).boundaryFlags)
:
And likewise on the right.