The identity law: stage equivalences

Composing with a strand bundle 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 (strandBundle t').disjUnion F relabelled along a stage equivalence relocating the not-yet-glued interface labels of F into the left label block.

The stage equivalence is assembled from block decompositions: the five blocks are the strand-in labels A, the strand-out labels A', the already-glued interface labels B, the not-yet-glued interface labels C, and the outer labels D; the shuffle (A ⊕ A') ⊕ ((B ⊕ C) ⊕ D) ≃ ((A ⊕ C) ⊕ A') ⊕ (B ⊕ D) is a plain constructor permutation with definitional inverses.

def RS.stageShuffle (A A' B C D : Type) : (A ⊕ A') ⊕ (B ⊕ C) ⊕ D ≃ ((A ⊕ C) ⊕ A') ⊕ B ⊕ D

The five-block shuffle underlying the stage equivalence.

Equations

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

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

The stage relabelling for the identity law: on the left, the t' strand-in labels, then the t - t' not-yet-glued interface labels of F, then the t' strand-out labels; on the right, the t' already-glued interface labels, then the u outer labels.

Equations

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

Label evaluations

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

Evaluation of the stage equivalence on a right label: an already-glued interface label stays right, a not-yet-glued interface label relocates to the left block, and an outer label stays right with an offset.

theorem RS.stageEquiv_inl (t t' u : ℕ) (ht : t' ≤ t) (a : Fin (t' + t')) : (stageEquiv t t' u ht) (Sum.inl a) = if h : ↑a < t' then Sum.inl ⟨↑a, ⋯⟩ else Sum.inl ⟨t + (↑a - t'), ⋯⟩

Evaluation of the stage equivalence on a left (strand) label: a strand-in label stays left with its index, a strand-out label goes left with an offset past the interface block.

The base case

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

Evaluation of the stage-zero equivalence on a right label: an interface label relocates to the left block, an outer label stays right.

instance RS.strandBundleZero_flag_isEmpty : IsEmpty (strandBundle 0).Flag

The empty bundle has no flags.

instance RS.strandBundleZero_vertex_isEmpty : IsEmpty (strandBundle 0).Vertex

Nor any vertices — it is the empty fragment.

noncomputable def RS.stageZeroEquiv (t u : ℕ) (F : Fragment (Fin (t + u))) : ((glueInterface t 0 u (((strandBundle 0).disjUnion F).relabel (stageEquiv t 0 u ⋯))).relabel finSumFinEquiv).Equiv F

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

Equations

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

The descent step

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

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

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

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

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

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

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

The pairing partner of the left boundary flag in the relabelled fragment: it is (t', false), the incoming end of strand t'.

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

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 (strandBundle t').disjUnion F.

Equations

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

interfaceStepEquiv evaluation lemmas

theorem RS.interfaceStepEquiv_eval_inl (s t u j : ℕ) (hj : j < s + t) : (interfaceStepEquiv s t u) ⟨Sum.inl ⟨j, ⋯⟩, ⋯⟩ = Sum.inl ⟨j, hj⟩

Evaluation of interfaceStepEquiv on a left surviving label.

theorem RS.interfaceStepEquiv_eval_inr_below (s t u j : ℕ) (hj : j < t) : (interfaceStepEquiv s t u) ⟨Sum.inr ⟨j, ⋯⟩, ⋯⟩ = Sum.inr ⟨j, ⋯⟩

Evaluation of interfaceStepEquiv on a right surviving label below the cut.

theorem RS.interfaceStepEquiv_eval_inr_above (s t u j : ℕ) (hj : t < j) (hj' : j < t + 1 + u) : (interfaceStepEquiv s t u) ⟨Sum.inr ⟨j, hj'⟩, ⋯⟩ = Sum.inr ⟨j - 1, ⋯⟩

Evaluation of interfaceStepEquiv on a right surviving label above the cut.

The stage step equivalence

@[reducible, inline]

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

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

Equations

• RS.baseFragment t t' u ht F = ((RS.strandBundle (t' + 1)).disjUnion F).relabel (RS.stageEquiv t (t' + 1) u ht)

@[reducible, inline]

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

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

Equations

• RS.targetFragment t t' u ht' F = ((RS.strandBundle t').disjUnion F).relabel (RS.stageEquiv t t' u ht')

@[reducible, inline]

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

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

Equations

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

Assembly: the left identity law

noncomputable def RS.stageStepEquiv (t t' u : ℕ) (ht : t' + 1 ≤ t) (F : Fragment (Fin (t + u))) : (sourceFragment t t' u ht F).Equiv (targetFragment t 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.

theorem RS.stageEquiv_self (t u : ℕ) (x : Fin (t + t) ⊕ Fin (t + u)) : (stageEquiv t t u ⋯) x = x

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

def RS.Fragment.Equiv.relabelPointwiseId {α : Type} (W : Fragment α) (e : α ≃ α) (h : ∀ (x : α), e x = x) : (W.relabel e).Equiv W

Relabelling by a pointwise-identity equivalence yields an equivalent fragment.

Equations

• RS.Fragment.Equiv.relabelPointwiseId W e h = { flagEquiv := Equiv.refl (W.relabel e).Flag, vertexEquiv := Equiv.refl (W.relabel e).Vertex, attach_comm := ⋯, pairing_comm := ⋯, circles_eq := ⋯ }

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

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

@[irreducible]

noncomputable def RS.glueInterfaceStrandBundleDescent (t u : ℕ) (F : Fragment (Fin (t + u))) (t' : ℕ) (ht' : t' ≤ t) : (glueInterface t t u ((strandBundle t).disjUnion F)).Equiv (glueInterface t t' u (((strandBundle t').disjUnion F).relabel (stageEquiv t 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 t on the original strand/F union.

Equations

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

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

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

Equations

• RS.composeStrandBundleLeft t u F = ((RS.glueInterfaceStrandBundleDescent t u F 0 ⋯).relabelCongr finSumFinEquiv).trans (RS.stageZeroEquiv t u F)