Hopf problem: homology of x · small chain biprod

Supporting definitions and proofs for this stage of the six-sphere construction.

theorem Mathoverflow1973.SmallChainBiprod.square_f {K L J T : ChainComplex (ModuleCat ℤ) ℕ} (a : J ⟶ K) (b : J ⟶ L) (u : K ⟶ T) (v : L ⟶ T) (w : CategoryTheory.CategoryStruct.comp a u = CategoryTheory.CategoryStruct.comp b v) (n : ℕ) : CategoryTheory.CategoryStruct.comp (a.f n) (u.f n) = CategoryTheory.CategoryStruct.comp (b.f n) (v.f n)