Documentation

LeanPool.HopfProblem.TorusHomology.PeriodTorusHigherHomology4

Hopf problem: torus homology · period torus higher homology 4 #

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

source
def Mathoverflow1973.PeriodTorusHigherHomology.formalEdgeCrossProduct {V : Type u_1} {W : Type u_2} (q : ℕ) :
SingularMayerVietoris.FormalChains V 2 →ₗ[ℤ] SingularMayerVietoris.FormalChains W (q + 1) →ₗ[ℤ] SingularMayerVietoris.FormalChains (V × W) (q + 2)

The formal chain-level cross product with an oriented edge.

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