The right identity law: stage equivalences

Mirror of RS.Novel.Skein.IdentityLaw (the left identity law). Composing with a strand bundle on the right is the identity up to fragment equivalence. The proof runs by descending induction through glueInterface with the invariant that the stage-t' fragment is equivalent to F.disjUnion (strandBundle t') relabelled along a stage equivalence relocating the not-yet-glued interface labels and the strand labels into the two output blocks.

The transformation: where the left law places the strand bundle in the left factor (its outgoing ends glued to F's leading interface labels), the right law places F in the left factor and the strand bundle in the right (interface pairs (Sum.inl (s + k), Sum.inr k) hit F's trailing labels and the bundle's incoming labels; the bundle's outgoing labels survive and become the output's trailing labels).

The stage equivalence maps Fin (s + u) ⊕ Fin (t' + t') to Fin (s + t') ⊕ Fin (t' + u). Block decomposition: D = Fin s (F's leading/outer labels) C = Fin t' (F's not-yet-glued trailing interface labels) B = Fin (u - t') (F's already-glued trailing labels) A = Fin t' (strand-bundle incoming ends) A' = Fin t' (strand-bundle outgoing ends) The shuffle: ((D ⊕ C) ⊕ B) ⊕ (A ⊕ A') ≃ (D ⊕ C) ⊕ ((A ⊕ A') ⊕ B).

def RS.stageEquivR (s t' u : ℕ) (ht : t' ≤ u) : Fin (s + u) ⊕ Fin (t' + t') ≃ Fin (s + t') ⊕ Fin (t' + u)

The stage relabelling for the right identity law. On the left output, F's outer labels and the not-yet-glued interface labels; on the right output, the strand-bundle labels followed by F's already-glued trailing labels.

Equations

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

Label evaluations

theorem RS.stageEquivR_inl (s t' u : ℕ) (ht : t' ≤ u) (ℓ : Fin (s + u)) : (stageEquivR s t' u ht) (Sum.inl ℓ) = if h : ↑ℓ < s + t' then Sum.inl ⟨↑ℓ, h⟩ else Sum.inr ⟨t' + (↑ℓ - s), ⋯⟩

Evaluation of the right stage equivalence on a left label (F's labels): a label below s + t' stays left; a label at or above s + t' relocates to the right block.

theorem RS.stageEquivR_inr (s t' u : ℕ) (ht : t' ≤ u) (a : Fin (t' + t')) : (stageEquivR s t' u ht) (Sum.inr a) = Sum.inr ⟨↑a, ⋯⟩

Evaluation of the right stage equivalence on a right label (strand-bundle labels): it maps to the right output block at the same index.

The base case

theorem RS.stageEquivR_zero_inl (s u : ℕ) (ℓ : Fin (s + u)) : (stageEquivR s 0 u ⋯) (Sum.inl ℓ) = if h : ↑ℓ < s then Sum.inl ⟨↑ℓ, h⟩ else Sum.inr ⟨↑ℓ - s, ⋯⟩

Evaluation of the stage-zero right equivalence on a left label: a leading label stays left; a trailing label relocates to the right block.

noncomputable def RS.stageZeroEquivR (s u : ℕ) (F : Fragment (Fin (s + u))) : ((glueInterface s 0 u ((F.disjUnion (strandBundle 0)).relabel (stageEquivR s 0 u ⋯))).relabel finSumFinEquiv).Equiv F

The base case of the right identity law: after zero interface gluings, the triply-relabelled F/(strand-0) union is equivalent to F.

Equations

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

The descent step

theorem RS.stageStepR_leftBoundary (s t' u : ℕ) (ht : t' + 1 ≤ u) (F : Fragment (Fin (s + u))) : ((F.disjUnion (strandBundle (t' + 1))).relabel (stageEquivR s (t' + 1) u ht)).boundaryFlag (Sum.inl ⟨s + t', ⋯⟩) = Sum.inl (F.boundaryFlag ⟨s + t', ⋯⟩)

The boundary flag at the left interface label in the relabelled disjoint union: it is F's boundary flag at s + t'.

theorem RS.stageStepR_rightBoundary (s t' u : ℕ) (ht : t' + 1 ≤ u) (F : Fragment (Fin (s + u))) : ((F.disjUnion (strandBundle (t' + 1))).relabel (stageEquivR s (t' + 1) u ht)).boundaryFlag (Sum.inr ⟨t', ⋯⟩) = Sum.inr (⟨t', ⋯⟩, false)

The boundary flag at the right interface label in the relabelled disjoint union: it is the incoming end of strand t'.

theorem RS.stageStepR_hopen (s t' u : ℕ) (ht : t' + 1 ≤ u) (F : Fragment (Fin (s + u))) : ((F.disjUnion (strandBundle (t' + 1))).relabel (stageEquivR s (t' + 1) u ht)).pairing (((F.disjUnion (strandBundle (t' + 1))).relabel (stageEquivR s (t' + 1) u ht)).boundaryFlag (Sum.inl ⟨s + t', ⋯⟩)) ≠ ((F.disjUnion (strandBundle (t' + 1))).relabel (stageEquivR s (t' + 1) u ht)).boundaryFlag (Sum.inr ⟨t', ⋯⟩)

The glue in the descent step is always the open case.

theorem RS.stageStepR_rightPairing (s t' u : ℕ) (ht : t' + 1 ≤ u) (F : Fragment (Fin (s + u))) : ((F.disjUnion (strandBundle (t' + 1))).relabel (stageEquivR s (t' + 1) u ht)).pairing (Sum.inr (⟨t', ⋯⟩, false)) = Sum.inr (⟨t', ⋯⟩, true)

The pairing partner of the right boundary flag in the relabelled fragment: it is (t', true), the outgoing end of strand t'.

noncomputable def RS.stageStepFlagEquivR (s t' u : ℕ) (ht : t' + 1 ≤ u) (F : Fragment (Fin (s + u))) : ((F.disjUnion (strandBundle (t' + 1))).relabel (stageEquivR s (t' + 1) u ht)).SurvivingFlag (Sum.inl ⟨s + t', ⋯⟩) (Sum.inr ⟨t', ⋯⟩) ≃ F.Flag ⊕ Fin t' × Bool

The flag equivalence for the descent step: surviving flags of the open glue at stage t' + 1 correspond to flags of the stage-t' disjoint union F.disjUnion (strandBundle t').

Equations

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

The stage step equivalence

@[reducible, inline]

abbrev RS.baseFragmentR (s t' u : ℕ) (ht : t' + 1 ≤ u) (F : Fragment (Fin (s + u))) : Fragment (Fin (s + (t' + 1)) ⊕ Fin (t' + 1 + u))

The relabelled fragment-strand union before the next right identity glue.

Equations

• RS.baseFragmentR s t' u ht F = (F.disjUnion (RS.strandBundle (t' + 1))).relabel (RS.stageEquivR s (t' + 1) u ht)

@[reducible, inline]

abbrev RS.targetFragmentR (s t' u : ℕ) (ht' : t' ≤ u) (F : Fragment (Fin (s + u))) : Fragment (Fin (s + t') ⊕ Fin (t' + u))

The relabelled fragment-strand union at the target stage of right identity descent.

Equations

• RS.targetFragmentR s t' u ht' F = (F.disjUnion (RS.strandBundle t')).relabel (RS.stageEquivR s t' u ht')

@[reducible, inline]

noncomputable abbrev RS.sourceFragmentR (s t' u : ℕ) (ht : t' + 1 ≤ u) (F : Fragment (Fin (s + u))) : Fragment (Fin (s + t') ⊕ Fin (t' + u))

The source fragment obtained by one open glue in the right identity descent.

Equations

• RS.sourceFragmentR s t' u ht F = ((RS.baseFragmentR s t' u ht F).gluePairOpen (Sum.inl ⟨s + t', ⋯⟩) (Sum.inr ⟨t', ⋯⟩) ⋯ ⋯).relabel (RS.interfaceStepEquiv s t' u)

noncomputable def RS.stageStepEquivR (s t' u : ℕ) (ht : t' + 1 ≤ u) (F : Fragment (Fin (s + u))) : (sourceFragmentR s t' u ht F).Equiv (targetFragmentR s t' u ⋯ F)

The descent step: after one open glue (at the t'-th interface pair), the resulting fragment is equivalent to the stage-t' disjoint union relabelled by the stage-t' equivalence.

Equations

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

Assembly: the right identity law

theorem RS.stageEquivR_self (s u : ℕ) (x : Fin (s + u) ⊕ Fin (u + u)) : (stageEquivR s u u ⋯) x = x

The stage equivalence at t' = u acts as the identity: every element is mapped to itself.

theorem RS.baseFragmentR_gluePair_eq (s t' u : ℕ) (ht : t' + 1 ≤ u) (F : Fragment (Fin (s + u))) : (baseFragmentR s t' u ht F).gluePair (Sum.inl ⟨s + t', ⋯⟩) (Sum.inr ⟨t', ⋯⟩) ⋯ = (baseFragmentR s t' u ht F).gluePairOpen (Sum.inl ⟨s + t', ⋯⟩) (Sum.inr ⟨t', ⋯⟩) ⋯ ⋯

In the base fragment, the glue is always open, so gluePair coincides with gluePairOpen.

@[irreducible]

noncomputable def RS.glueInterfaceStrandBundleDescentRight (s u : ℕ) (F : Fragment (Fin (s + u))) (t' : ℕ) (ht' : t' ≤ u) : (glueInterface s u u (F.disjUnion (strandBundle u))).Equiv (glueInterface s t' u ((F.disjUnion (strandBundle t')).relabel (stageEquivR s t' u ht')))

Descending induction: iterating glueInterface from stage t' down to zero, with the stage-t' fragment, yields a result equivalent to iterating from stage u on the original F/strand union.

Equations

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

noncomputable def RS.composeStrandBundleRight (s u : ℕ) (F : Fragment (Fin (s + u))) : (F.compose (strandBundle u)).Equiv F

The right identity law for fragment composition: composing with the strand bundle on the right yields an equivalent fragment.

Equations

• RS.composeStrandBundleRight s u F = ((RS.glueInterfaceStrandBundleDescentRight s u F 0 ⋯).relabelCongr finSumFinEquiv).trans (RS.stageZeroEquivR s u F)