Free-side relabels pass through composition

Relabelling the free (non-interface) boundary of a factor relabels the composite: permuting the outgoing boundary of the right factor commutes with compose (composeRelabelOut), because the interface pairs are untouched. That is the naturality law of the boundary identifications, and the engine that lets a permutation fragment be absorbed into a relabel (composePermFragment, permFragmentComposeLeft).

The outgoing relabel's own inverse law (outPermEquiv_symm, with its two halves outPermEquiv_symm_low and outPermEquiv_symm_high) lives here too, since it is what lets the absorption run in either direction.

theorem RS.outPermEquiv_symm_low (s : ℕ) {t : ℕ} (σ : Equiv.Perm (Fin t)) (a : Fin s) : (outPermEquiv s σ).symm (Fin.castAdd t a) = Fin.castAdd t a

The inverse outgoing permutation fixes low labels.

The interface pairs are untouched

theorem RS.outPermEquiv_symm (s : ℕ) {t : ℕ} (σ : Equiv.Perm (Fin t)) : (outPermEquiv s σ).symm = outPermEquiv s (Equiv.symm σ)

The inverse of an outgoing permutation is the outgoing inverse permutation.

theorem RS.out_ground (s t u : ℕ) (σ : Equiv.Perm (Fin u)) : Fragment.mapPairs ((Equiv.refl (Fin (s + t))).sumCongr (outPermEquiv t σ)).symm (interfacePairs s t u) = interfacePairs s t u

Peeling an outgoing permutation of the right factor leaves the interface pairs untouched.

The outgoing relabel

noncomputable def RS.outQs (s t u : ℕ) (σ : Equiv.Perm (Fin u)) : List ((Fin (s + t) ⊕ Fin (t + u)) × (Fin (s + t) ⊕ Fin (t + u)))

The peeled pairs of the outgoing relabel.

Equations

• RS.outQs s t u σ = RS.Fragment.mapPairs ((Equiv.refl (Fin (s + t))).sumCongr (RS.outPermEquiv t σ)).symm (RS.interfacePairs s t u)

theorem RS.out_label_meet (s t u : ℕ) (σ : Equiv.Perm (Fin u)) : (Fragment.foldSurvivingPermEquiv ⋯).symm.trans ((Fragment.foldSurvivingMapEquiv ((Equiv.refl (Fin (s + t))).sumCongr (outPermEquiv t σ)) (outQs s t u σ)).trans ((Fragment.foldSurvivingPermEquiv ⋯).symm.trans ((interfaceSurvEquiv s t u).trans finSumFinEquiv))) = ((interfaceSurvEquiv s t u).trans finSumFinEquiv).trans (outPermEquiv s σ)

The label meet of the outgoing relabel: the survivor chase.

noncomputable def RS.composeRelabelOut {s t u : ℕ} (σ : Equiv.Perm (Fin u)) (F : Fragment (Fin (s + t))) (G : Fragment (Fin (t + u))) : (F.compose (G.relabel (outPermEquiv t σ))).Equiv ((F.compose G).relabel (outPermEquiv s σ))

Outgoing relabels pass through composition: permuting the outgoing boundary of the right factor permutes the outgoing boundary of the composite.

Equations

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

Permutation fragments absorb into relabels

noncomputable def RS.composePermFragment {s t : ℕ} (σ : Equiv.Perm (Fin t)) (F : Fragment (Fin (s + t))) : (F.compose (permFragment σ)).Equiv (F.relabel (outPermEquiv s σ))

Composing with a permutation fragment on the right relabels the outgoing boundary.

Equations

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

noncomputable def RS.permFragmentComposeLeft {t u : ℕ} (σ : Equiv.Perm (Fin t)) (F : Fragment (Fin (t + u))) : ((permFragment σ).compose F).Equiv (F.relabel (inPermEquiv (Equiv.symm σ) u))

Composing with a permutation fragment on the left relabels the incoming boundary by the inverse.

Equations

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