Hopf problem: homology theory · first hurewicz 3

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

noncomputable def Mathoverflow1973.FirstHurewicz.loopCycle {X : Type} [TopologicalSpace X] {x : X} (p : Path x x) : ↥(Cycles1 X)

The singular one-cycle represented by a based loop.

Equations

• Mathoverflow1973.FirstHurewicz.loopCycle p = Mathoverflow1973.FirstHurewicz.mkCycle1✝ X (Mathoverflow1973.FirstHurewicz.pathChain✝ p) ⋯

noncomputable def Mathoverflow1973.FirstHurewicz.loopHomologyClass {X : Type} [TopologicalSpace X] {x : X} (p : Path x x) : ↑(SingularH1 X)

The first singular-homology class represented by a based loop.

Equations

• Mathoverflow1973.FirstHurewicz.loopHomologyClass p = (Mathoverflow1973.FirstHurewicz.cycleClass X) (Mathoverflow1973.FirstHurewicz.loopCycle p)