Associativity of composition

Both associations of a triple composition normalize to iterated gluing of the two interface pair lists over the common ambient disjoint union (F ⊔ G) ⊔ H, so composition of fragments is associative up to fragment equivalence (composeAssoc).

This file builds the associativity infrastructure in stages: the associativity equivalence of disjoint unions, the embedding of relabellings into disjoint unions, the normalization of each association, and the final meet in the middle via two-stage folding and reordering.

noncomputable def RS.Fragment.disjUnionAssoc {α β γ : Type} (W₁ : Fragment α) (W₂ : Fragment β) (W₃ : Fragment γ) : ((W₁.disjUnion W₂).disjUnion W₃).Equiv ((W₁.disjUnion (W₂.disjUnion W₃)).relabel (Equiv.sumAssoc α β γ).symm)

Disjoint union is associative, up to the sum-associativity relabelling.

Equations

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

noncomputable def RS.Fragment.relabelDisjUnionLeft {α β α' : Type} (W : Fragment α) (W' : Fragment β) (e : α ≃ α') : ((W.relabel e).disjUnion W').Equiv ((W.disjUnion W').relabel (e.sumCongr (_root_.Equiv.refl β)))

Relabelling the left factor of a disjoint union equals relabelling the whole union by a sum congruence.

Equations

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

noncomputable def RS.Fragment.relabelDisjUnionRight {α β β' : Type} (W : Fragment α) (W' : Fragment β) (e : β ≃ β') : (W.disjUnion (W'.relabel e)).Equiv ((W.disjUnion W').relabel ((_root_.Equiv.refl α).sumCongr e))

Relabelling the right factor of a disjoint union equals relabelling the whole union by a sum congruence.

Equations

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

noncomputable def RS.Fragment.Equiv.relabelFlip {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {e : β ≃ α} (E : W₁.Equiv (W₂.relabel e)) : W₂.Equiv (W₁.relabel e.symm)

Flip a relabelled equivalence to the other side.

Equations

• E.relabelFlip = ((⋯ ▸ RS.Fragment.Equiv.relabelTrans W₂ e e.symm).trans (RS.Fragment.Equiv.relabelRefl W₂)).symm.trans (E.symm.relabelCongr e.symm)

noncomputable def RS.Fragment.Equiv.relabelEq {α β : Type} (W : Fragment α) {e e' : α ≃ β} (h : e = e') : (W.relabel e).Equiv (W.relabel e')

Relabelling by equal equivalences.

Equations

• RS.Fragment.Equiv.relabelEq W h = h ▸ RS.Fragment.Equiv.refl (W.relabel e)

The interface pair lists in the common ambient

def RS.uPairsAssoc (s t u v : ℕ) : List (((Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (u + v)) × ((Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (u + v)))

The u-interface pairs in the common ambient (F ⊔ G) ⊔ H: the high labels of G against the low labels of H, top pair first.

Equations

• RS.uPairsAssoc s t u v = List.map (fun (k : Fin u) => (Sum.inl (Sum.inr ⟨t + ↑k, ⋯⟩), Sum.inr ⟨↑k, ⋯⟩)) (List.finRange u).reverse

theorem RS.uPairsAssoc_wf (s t u v : ℕ) : Fragment.PairsWF (uPairsAssoc s t u v)

The u-interface pairs are well-formed.

theorem RS.mem_uPairsAssoc (s t u v : ℕ) (p : ((Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (u + v)) × ((Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (u + v))) : p ∈ uPairsAssoc s t u v ↔ ∃ (k : Fin u), p = (Sum.inl (Sum.inr ⟨t + ↑k, ⋯⟩), Sum.inr ⟨↑k, ⋯⟩)

Membership in the u-interface pairs.

def RS.tPairsAssoc (s t u v : ℕ) : List (((Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (u + v)) × ((Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (u + v)))

The t-interface pairs in the common ambient, as a direct index map.

Equations

• RS.tPairsAssoc s t u v = List.map (fun (k : Fin t) => (Sum.inl (Sum.inl ⟨s + ↑k, ⋯⟩), Sum.inl (Sum.inr ⟨↑k, ⋯⟩))) (List.finRange t).reverse

theorem RS.tPairsAssoc_eq (s t u v : ℕ) : tPairsAssoc s t u v = Fragment.inlPairs (interfacePairs s t u)

The direct t-interface pairs are the embedded interface pairs.

theorem RS.mem_tPairsAssoc' (s t u v : ℕ) (p : ((Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (u + v)) × ((Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (u + v))) : p ∈ tPairsAssoc s t u v ↔ ∃ (k : Fin t), p = (Sum.inl (Sum.inl ⟨s + ↑k, ⋯⟩), Sum.inl (Sum.inr ⟨↑k, ⋯⟩))

Membership in the direct t-interface pairs.

theorem RS.mem_tPairsAssoc (s t u v : ℕ) (p : ((Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (u + v)) × ((Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (u + v))) : p ∈ Fragment.inlPairs (interfacePairs s t u) ↔ ∃ (k : Fin t), p = (Sum.inl (Sum.inl ⟨s + ↑k, ⋯⟩), Sum.inl (Sum.inr ⟨↑k, ⋯⟩))

Membership in the embedded t-interface pairs.

theorem RS.mem_interfacePairs (s t u : ℕ) (p : (Fin (s + t) ⊕ Fin (t + u)) × (Fin (s + t) ⊕ Fin (t + u))) : p ∈ interfacePairs s t u ↔ ∃ (k : Fin t), p = (Sum.inl ⟨s + ↑k, ⋯⟩, Sum.inr ⟨↑k, ⋯⟩)

Membership in the interface pairs.

theorem RS.mapPairs_mapPairs {α β γ : Type} (e : α ≃ β) (e' : β ≃ γ) (ps : List (α × α)) : Fragment.mapPairs e' (Fragment.mapPairs e ps) = Fragment.mapPairs (e.trans e') ps

mapPairs composes.

theorem RS.highG_surv (s t u : ℕ) (b : Fin (t + u)) (hb : t ≤ ↑b) (p : (Fin (s + t) ⊕ Fin (t + u)) × (Fin (s + t) ⊕ Fin (t + u))) : p ∈ interfacePairs s t u → Sum.inr b ≠ p.1 ∧ Sum.inr b ≠ p.2

High G-labels survive the t-interface gluing.

theorem RS.lowF_surv (s t u : ℕ) (a : Fin (s + t)) (ha : ↑a < s) (p : (Fin (s + t) ⊕ Fin (t + u)) × (Fin (s + t) ⊕ Fin (t + u))) : p ∈ interfacePairs s t u → Sum.inl a ≠ p.1 ∧ Sum.inl a ≠ p.2

Low F-labels survive the t-interface gluing.

theorem RS.interfaceEquiv_symm_high (s t u k : ℕ) (_hk : k < u) (h1 : s + k < s + u) (h2 : t + k < t + u) : ↑(((interfaceSurvEquiv s t u).trans finSumFinEquiv).symm ⟨s + k, h1⟩) = Sum.inr ⟨t + k, h2⟩

The inverse boundary identification sends high output labels to high G-labels.

theorem RS.interfaceEquiv_symm_low (s t u k : ℕ) (hk : k < s) (h1 : k < s + u) (h2 : k < s + t) : ↑(((interfaceSurvEquiv s t u).trans finSumFinEquiv).symm ⟨k, h1⟩) = Sum.inl ⟨k, h2⟩

The inverse boundary identification sends low output labels to low F-labels.

theorem RS.Fragment.inlFoldEquiv_symm_inl_val {α β : Type} (ps : List (α × α)) (x : FoldSurviving α ps) : ↑((inlFoldEquiv ps).symm (Sum.inl x)) = Sum.inl ↑x

Value of the left-embedding fold equivalence's inverse on an embedded survivor.

theorem RS.Fragment.inlFoldEquiv_symm_inr_val {α β : Type} (ps : List (α × α)) (b : β) : ↑((inlFoldEquiv ps).symm (Sum.inr b)) = Sum.inr b

Value of the left-embedding fold equivalence's inverse on a right label.

theorem RS.Fragment.inrFoldEquiv_symm_inr_val {α β : Type} (qs : List (β × β)) (x : FoldSurviving β qs) : ↑((inrFoldEquiv qs).symm (Sum.inr x)) = Sum.inr ↑x

Value of the right-embedding fold equivalence's inverse on an embedded survivor.

theorem RS.Fragment.inrFoldEquiv_symm_inl_val {α β : Type} (qs : List (β × β)) (a : α) : ↑((inrFoldEquiv qs).symm (Sum.inl a)) = Sum.inl a

Value of the right-embedding fold equivalence's inverse on a left label.

theorem RS.lhs_pairs_eq (s t u v : ℕ) (hsep : Fragment.PairsSepAll (Fragment.inlPairs (interfacePairs s t u)) (uPairsAssoc s t u v)) : Fragment.mapPairs (Fragment.inlFoldEquiv (interfacePairs s t u)).symm (Fragment.mapPairs (((interfaceSurvEquiv s t u).trans finSumFinEquiv).sumCongr (Equiv.refl (Fin (u + v)))).symm (interfacePairs s u v)) = Fragment.liftPairs (Fragment.inlPairs (interfacePairs s t u)) (uPairsAssoc s t u v) hsep

The mapped-back outer interface pairs of the left association are the lifted u-interface pairs.

theorem RS.assocPairs_wf (s t u v : ℕ) : Fragment.PairsWF (Fragment.inlPairs (interfacePairs s t u) ++ uPairsAssoc s t u v)

The combined pair list is well-formed.

noncomputable def RS.Fragment.Equiv.relabelFlip' {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {e : α ≃ β} (E : (W₁.relabel e).Equiv W₂) : W₁.Equiv (W₂.relabel e.symm)

Flip a relabelled equivalence to the other side, relabelled form on the left.

Equations

• E.relabelFlip' = E.symm.relabelFlip

noncomputable def RS.Fragment.glueListProofIrrel {α : Type} (W : Fragment α) (ps : List (α × α)) (h1 h2 : PairsWF ps) : (W.glueList ps h1).Equiv (W.glueList ps h2)

Iterated gluing does not depend on the well-formedness proof.

Equations

• W.glueListProofIrrel ps h1 h2 = RS.Fragment.Equiv.refl (W.glueList ps h1)

noncomputable def RS.glueListPullRelabelTrans {α β γ : Type} (W : Fragment α) (σ : α ≃ β) (ps : List (β × β)) (hp : Fragment.PairsWF ps) {V : Fragment γ} {τ : γ ≃ Fragment.FoldSurviving α (Fragment.mapPairs σ.symm ps)} (e : (W.glueList (Fragment.mapPairs σ.symm ps) ⋯).Equiv (V.relabel τ)) : ((W.relabel σ).glueList ps hp).Equiv (V.relabel ((τ.trans (Fragment.foldSurvivingMapEquiv σ (Fragment.mapPairs σ.symm ps))).trans (Fragment.foldSurvivingPermEquiv ⋯).symm))

Pull gluing pairs through a relabelling and compose a normalized inner fold.

Equations

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

noncomputable def RS.pairCloseAmbientEquiv {n : ℕ} (F G : Fragment (Fin n)) {α : Type} {N : Fragment α} {e : α ≃ Fin n} (E : G.Equiv (N.relabel e)) : ((F.relabel (finCongr ⋯)).disjUnion (G.relabel (finCongr ⋯))).Equiv ((F.disjUnion N).relabel (((Equiv.refl (Fin n)).sumCongr e).trans (((Equiv.refl (Fin n)).sumCongr (finCongr ⋯)).trans ((finCongr ⋯).sumCongr (Equiv.refl (Fin (n + 0)))))))

Transport the two closure casts across a normalized right-hand fragment.

Equations

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

The left association, normalized

noncomputable def RS.lhsLabelEquiv (s t u v : ℕ) : Fragment.FoldSurviving ((Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (u + v)) (Fragment.inlPairs (interfacePairs s t u) ++ uPairsAssoc s t u v) ≃ Fin (s + v)

The composed label identification of the left association: flatten the two-stage survivors, pass through the embedded and relabelled fold equivalences, and read off the outer boundary identification.

Equations

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

theorem RS.assocPairsR_wf (s t u v : ℕ) : Fragment.PairsWF (uPairsAssoc s t u v ++ tPairsAssoc s t u v)

The swapped combined pair list is well-formed.

theorem RS.rhs_ground_eq (s t u v : ℕ) : Fragment.mapPairs (Equiv.sumAssoc (Fin (s + t)) (Fin (t + u)) (Fin (u + v))).symm.symm.symm (Fragment.inrPairs (interfacePairs t u v)) = uPairsAssoc s t u v

The associativity-transported right-embedded u-interface pairs are the ambient u-interface pairs.

noncomputable def RS.rhsBridgeEquiv (s t u v : ℕ) : Fragment.FoldSurviving ((Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (u + v)) (uPairsAssoc s t u v) ≃ Fragment.FoldSurviving (Fin (s + t) ⊕ Fin (t + u) ⊕ Fin (u + v)) (Fragment.inrPairs (interfacePairs t u v))

The associativity bridge: survivors of the ambient u-interface pairs are survivors of the right-embedded pairs in the right-associated ambient.

Equations

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

theorem RS.rhs_pairs_eq (s t u v : ℕ) (hsep : Fragment.PairsSepAll (uPairsAssoc s t u v) (tPairsAssoc s t u v)) : Fragment.mapPairs (rhsBridgeEquiv s t u v).symm (Fragment.mapPairs (Fragment.inrFoldEquiv (interfacePairs t u v)).symm (Fragment.mapPairs ((Equiv.refl (Fin (s + t))).sumCongr ((interfaceSurvEquiv t u v).trans finSumFinEquiv)).symm (interfacePairs s t v))) = Fragment.liftPairs (uPairsAssoc s t u v) (tPairsAssoc s t u v) hsep

The mapped-back outer interface pairs of the right association are the lifted t-interface pairs.

noncomputable def RS.assocNormalLeft {s t u v : ℕ} (F : Fragment (Fin (s + t))) (G : Fragment (Fin (t + u))) (H : Fragment (Fin (u + v))) : ((F.compose G).compose H).Equiv ((((F.disjUnion G).disjUnion H).glueList (Fragment.inlPairs (interfacePairs s t u) ++ uPairsAssoc s t u v) ⋯).relabel (lhsLabelEquiv s t u v))

The left association, normalized: composing F with G and then with H is iterated gluing of the embedded t-interface pairs followed by the u-interface pairs over the common ambient (F ⊔ G) ⊔ H.

Equations

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

The right association, normalized

noncomputable def RS.rhsQs1 (s t u v : ℕ) : List ((Fin (s + t) ⊕ Fragment.FoldSurviving (Fin (t + u) ⊕ Fin (u + v)) (interfacePairs t u v)) × (Fin (s + t) ⊕ Fragment.FoldSurviving (Fin (t + u) ⊕ Fin (u + v)) (interfacePairs t u v)))

The outer interface pairs of the right association, pulled back to the boundary of the inner composition.

Equations

• RS.rhsQs1 s t u v = RS.Fragment.mapPairs ((Equiv.refl (Fin (s + t))).sumCongr ((RS.interfaceSurvEquiv t u v).trans finSumFinEquiv)).symm (RS.interfacePairs s t v)

noncomputable def RS.rhsQs2 (s t u v : ℕ) : List (Fragment.FoldSurviving (Fin (s + t) ⊕ Fin (t + u) ⊕ Fin (u + v)) (Fragment.inrPairs (interfacePairs t u v)) × Fragment.FoldSurviving (Fin (s + t) ⊕ Fin (t + u) ⊕ Fin (u + v)) (Fragment.inrPairs (interfacePairs t u v)))

The outer interface pairs, pulled into the right-embedded fold survivors.

Equations

• RS.rhsQs2 s t u v = RS.Fragment.mapPairs (RS.Fragment.inrFoldEquiv (RS.interfacePairs t u v)).symm (RS.rhsQs1 s t u v)

noncomputable def RS.rhsQs3 (s t u v : ℕ) : List (Fragment.FoldSurviving ((Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (u + v)) (uPairsAssoc s t u v) × Fragment.FoldSurviving ((Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (u + v)) (uPairsAssoc s t u v))

The outer interface pairs, pulled across the associativity bridge.

Equations

• RS.rhsQs3 s t u v = RS.Fragment.mapPairs (RS.rhsBridgeEquiv s t u v).symm (RS.rhsQs2 s t u v)

noncomputable def RS.rhsLabelEquiv (s t u v : ℕ) : Fragment.FoldSurviving ((Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (u + v)) (Fragment.inlPairs (interfacePairs s t u) ++ uPairsAssoc s t u v) ≃ Fin (s + v)

The composed label identification of the right association.

Equations

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

noncomputable def RS.assocNormalRight {s t u v : ℕ} (F : Fragment (Fin (s + t))) (G : Fragment (Fin (t + u))) (H : Fragment (Fin (u + v))) : (F.compose (G.compose H)).Equiv ((((F.disjUnion G).disjUnion H).glueList (Fragment.inlPairs (interfacePairs s t u) ++ uPairsAssoc s t u v) ⋯).relabel (rhsLabelEquiv s t u v))

The right association, normalized: composing F with the composition of G and H is the same iterated gluing over the common ambient, through the associativity bridge.

Equations

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

The meet

theorem RS.label_equiv_meet (s t u v : ℕ) : lhsLabelEquiv s t u v = rhsLabelEquiv s t u v

The two label identifications agree: every survivor of the combined gluing is a low F-label or a high H-label, and both composites read off the same boundary position.

noncomputable def RS.composeAssoc {s t u v : ℕ} (F : Fragment (Fin (s + t))) (G : Fragment (Fin (t + u))) (H : Fragment (Fin (u + v))) : ((F.compose G).compose H).Equiv (F.compose (G.compose H))

Associativity of composition: the two associations of a triple composition are equivalent fragments.

Equations

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