Hopf problem: torus homology · period torus higher homology 9

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

def Mathoverflow1973.PeriodTorusHigherHomology.rightTranslation {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (a : G) : C(G, G)

Right translation by a fixed element as a continuous map.

Equations

• Mathoverflow1973.PeriodTorusHigherHomology.rightTranslation a = { toFun := fun (x : G) => x + a, continuous_toFun := ⋯ }

@[simp]

theorem Mathoverflow1973.PeriodTorusHigherHomology.rightTranslation_apply {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (a x : G) : (rightTranslation a) x = x + a