Hopf problem: torus homology · period torus higher homology 6

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

@[reducible, inline]

abbrev Mathoverflow1973.PeriodTorusHigherHomology.ProductTorus (n : ℕ) : Type

The product of n unit circles.

Equations

• Mathoverflow1973.PeriodTorusHigherHomology.ProductTorus n = (Fin n → AddCircle 1)

def Mathoverflow1973.PeriodTorusHigherHomology.coordinateProjection (n : ℕ) : (Fin n → ℝ) →+ ProductTorus n

The additive quotient map from real coordinates to the product torus.

Equations

• Mathoverflow1973.PeriodTorusHigherHomology.coordinateProjection n = { toFun := fun (x : Fin n → ℝ) (i : Fin n) => ↑(x i), map_zero' := ⋯, map_add' := ⋯ }

def Mathoverflow1973.PeriodTorusHigherHomology.CirclePaths.positiveLoop : Path 0 0

The positively oriented standard loop around the unit circle.

Equations

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