Gluing in an ambient union

The two normalization equivalences behind associativity of composition: disjoint union of fragments is associative up to equivalence (with the label re-bracketing), and a single-pair glue commutes with extending the ambient fragment by a disjoint union.

Glue-in-ambient equivalence

def RS.Fragment.ambientLabelEquiv {α β : Type} (i j : α) : SurvivingLabel (α ⊕ β) (Sum.inl i) (Sum.inl j) ≃ SurvivingLabel α i j ⊕ β

The label equivalence for gluing inside an ambient union: surviving labels of the sum at an inl-pair decompose as the surviving labels of the left factor plus the right labels.

Equations

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

def RS.Fragment.ambientFlagEquiv {α β : Type} (W : Fragment α) (V : Fragment β) (i j : α) : W.SurvivingFlag i j ⊕ V.Flag ≃ (W.disjUnion V).SurvivingFlag (Sum.inl i) (Sum.inl j)

The flag equivalence for gluing inside an ambient union: surviving flags of the union at the inl-pair are the surviving flags of the left factor plus the right flags.

Equations

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

noncomputable def RS.Fragment.gluePairClosedDisjUnion {α β : Type} (W : Fragment α) (V : Fragment β) {i j : α} (hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j) : ((W.gluePairClosed i j hclosed).disjUnion V).Equiv (((W.disjUnion V).gluePairClosed (Sum.inl i) (Sum.inl j) ⋯).relabel (ambientLabelEquiv i j))

The closed case of glue-in-ambient: when the two boundary flags bound a common edge in W, the LHS and RHS produce equivalent fragments.

Equations

• W.gluePairClosedDisjUnion V hclosed = { flagEquiv := W.ambientFlagEquiv V i j, vertexEquiv := Equiv.refl (W.Vertex ⊕ V.Vertex), attach_comm := ⋯, pairing_comm := ⋯, circles_eq := ⋯ }

noncomputable def RS.Fragment.gluePairOpenDisjUnion {α β : Type} (W : Fragment α) (V : Fragment β) {i j : α} (hij : i ≠ j) (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) : ((W.gluePairOpen i j hij hopen).disjUnion V).Equiv (((W.disjUnion V).gluePairOpen (Sum.inl i) (Sum.inl j) ⋯ ⋯).relabel (ambientLabelEquiv i j))

The open case of glue-in-ambient: when the two boundary flags bound distinct edges in W, the LHS and RHS produce equivalent fragments.

Equations

• W.gluePairOpenDisjUnion V hij hopen = { flagEquiv := W.ambientFlagEquiv V i j, vertexEquiv := Equiv.refl (W.Vertex ⊕ V.Vertex), attach_comm := ⋯, pairing_comm := ⋯, circles_eq := ⋯ }

noncomputable def RS.Fragment.gluePairDisjUnion {α β : Type} (W : Fragment α) (V : Fragment β) {i j : α} (hij : i ≠ j) : ((W.gluePair i j hij).disjUnion V).Equiv (((W.disjUnion V).gluePair (Sum.inl i) (Sum.inl j) ⋯).relabel (ambientLabelEquiv i j))

A single-pair glue commutes with extending the ambient fragment by a disjoint union: gluing {i, j} in W and then forming the union with V is equivalent to forming the union first and gluing the inl-wrapped pair.

Equations

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

noncomputable def RS.Fragment.gluePairRelabel {α β : Type} (W : Fragment α) (e : α ≃ β) {i j : β} (hij : i ≠ j) : ((W.relabel e).gluePair i j hij).Equiv ((W.gluePair (e.symm i) (e.symm j) ⋯).relabel (e.subtypeEquiv ⋯))

Gluing commutes with relabelling: gluing two labels of a relabelled fragment is the relabelled gluing of their preimages.

Equations

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

Component swap of a single glue

def RS.Fragment.survLabelSwapEquiv (α : Type) (i j : α) : SurvivingLabel α j i ≃ SurvivingLabel α i j

Swapping the two removed labels.

Equations

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

noncomputable def RS.Fragment.gluePairSwap {α : Type} (W : Fragment α) {i j : α} (hij : i ≠ j) : (W.gluePair i j hij).Equiv ((W.gluePair j i ⋯).relabel (survLabelSwapEquiv α i j))

Gluing a pair is symmetric in its two labels, up to the swap relabelling.

Equations

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

noncomputable def RS.Fragment.disjUnionComm {α β : Type} (W₁ : Fragment α) (W₂ : Fragment β) : (W₁.disjUnion W₂).Equiv ((W₂.disjUnion W₁).relabel (Equiv.sumComm β α))

Disjoint union is commutative, up to the sum-swap relabelling.

Equations

• W₁.disjUnionComm W₂ = { flagEquiv := Equiv.sumComm W₁.Flag W₂.Flag, vertexEquiv := Equiv.sumComm W₁.Vertex W₂.Vertex, attach_comm := ⋯, pairing_comm := ⋯, circles_eq := ⋯ }