The interchange law on Hom classes #
Tensoring two composites is composing the two tensors, descended to the Hom spaces: the fragment-level interchange at the singles, extended by the four-fold bilinear induction.
theorem
RS.mem_ker_interchange
{R : ℕ}
(f : EdgeRankParameter R)
{s₁ t₁ u₁ s₂ t₂ u₂ : ℕ}
(x₁ : Fragment (Fin (s₁ + t₁)) →₀ ℂ)
(y₁ : Fragment (Fin (t₁ + u₁)) →₀ ℂ)
(x₂ : Fragment (Fin (s₂ + t₂)) →₀ ℂ)
(y₂ : Fragment (Fin (t₂ + u₂)) →₀ ℂ)
:
((tensorFinsupp s₁ u₁ s₂ u₂) (((composeFinsupp s₁ t₁ u₁) x₁) y₁)) (((composeFinsupp s₂ t₂ u₂) x₂) y₂) - ((composeFinsupp (s₁ + s₂) (t₁ + t₂) (u₁ + u₂)) (((tensorFinsupp s₁ t₁ s₂ t₂) x₁) x₂))
(((tensorFinsupp t₁ u₁ t₂ u₂) y₁) y₂) ∈ (connectionMap f.val (s₁ + s₂ + (u₁ + u₂))).ker
The interchange difference lies in the kernel.