Hopf problem: torus homology · period torus higher homology 5

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

theorem Mathoverflow1973.PeriodTorusHigherHomology.formalEdgeCrossProduct_mem_supported {V : Type u_1} {W : Type u_2} {S : Set V} {T : Set W} (q : ℕ) {c : SingularMayerVietoris.FormalChains V 2} {d : SingularMayerVietoris.FormalChains W (q + 1)} : c ∈ SingularMayerVietoris.formalChainsSupported S 2 → d ∈ SingularMayerVietoris.formalChainsSupported T (q + 1) → ((formalEdgeCrossProduct q) c) d ∈ SingularMayerVietoris.formalChainsSupported (S ×ˢ T) (q + 2)