Associativity of the fragment tensor

The two associations of a triple tensor carry the same interleaved boundary up to the arithmetic cast: block order is s₁ s₂ s₃ | t₁ t₂ t₃ either way. The label identity (assocLabel_eq) is a six-block value chase through the interleave value lemmas; the associator equivalence follows by pure relabel algebra.

noncomputable def RS.tensorAssocCast (s₁ t₁ s₂ t₂ s₃ t₃ : ℕ) : Fin (s₁ + (s₂ + s₃) + (t₁ + (t₂ + t₃))) ≃ Fin (s₁ + s₂ + s₃ + (t₁ + t₂ + t₃))

The associativity cast of interleaved boundaries.

Equations

• RS.tensorAssocCast s₁ t₁ s₂ t₂ s₃ t₃ = finCongr ⋯

noncomputable def RS.assocLabelL (s₁ t₁ s₂ t₂ s₃ t₃ : ℕ) : Fin (s₁ + t₁) ⊕ Fin (s₂ + t₂) ⊕ Fin (s₃ + t₃) ≃ Fin (s₁ + s₂ + s₃ + (t₁ + t₂ + t₃))

The left-association label composite.

Equations

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

noncomputable def RS.assocLabelR (s₁ t₁ s₂ t₂ s₃ t₃ : ℕ) : Fin (s₁ + t₁) ⊕ Fin (s₂ + t₂) ⊕ Fin (s₃ + t₃) ≃ Fin (s₁ + s₂ + s₃ + (t₁ + t₂ + t₃))

The right-association label composite, cast.

Equations

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

theorem RS.assocLabel_eq (s₁ t₁ s₂ t₂ s₃ t₃ : ℕ) : assocLabelL s₁ t₁ s₂ t₂ s₃ t₃ = assocLabelR s₁ t₁ s₂ t₂ s₃ t₃

The two association composites agree.

noncomputable def RS.tensorFragmentAssoc (s₁ t₁ s₂ t₂ s₃ t₃ : ℕ) (X : Fragment (Fin (s₁ + t₁))) (Y : Fragment (Fin (s₂ + t₂))) (Z : Fragment (Fin (s₃ + t₃))) : (tensorFragment (tensorFragment X Y) Z).Equiv ((tensorFragment X (tensorFragment Y Z)).relabel (tensorAssocCast s₁ t₁ s₂ t₂ s₃ t₃))

Associativity of the fragment tensor: the two associations agree up to the arithmetic cast.

Equations

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