The quotient map from d → ℝ onto the unit torus

The unit torus UnitAddTorus d = (ℝ / ℤ)^d is the image of d → ℝ under the map x ↦ fun i ↦ (x i : UnitAddCircle) reducing each coordinate modulo one. This file records that this map is a surjective open quotient map whose fibres are the cosets of the integer vectors, so that functions on the torus are the same as ℤ^d-periodic functions on d → ℝ, and continuous functions on the torus are the same as continuous ℤ^d-periodic functions on d → ℝ.

Main results

• TauCeti.UnitAddTorus.surjective_coe: every point of the torus comes from a point of d → ℝ.
• TauCeti.UnitAddTorus.isOpenQuotientMap_coe: the map d → ℝ → UnitAddTorus d is an open quotient map.
• TauCeti.UnitAddTorus.coe_eq_coe_iff: two points have the same image exactly when they differ by an integer vector.
• TauCeti.UnitAddTorus.periodic_comp_coe: the lift of a function on the torus is ℤ^d-periodic.
• TauCeti.UnitAddTorus.exists_continuous_comp_coe_eq: a continuous ℤ^d-periodic function on d → ℝ descends to a continuous function on the torus.

theorem TauCeti.UnitAddTorus.surjective_coe {d : Type u_1} : Function.Surjective fun (x : d → ℝ) (i : d) => ↑(x i)

Every point of the torus is the image of a point of d → ℝ.

theorem TauCeti.UnitAddTorus.isOpenQuotientMap_coe {d : Type u_1} : IsOpenQuotientMap fun (x : d → ℝ) (i : d) => ↑(x i)

Reducing each coordinate modulo one is an open quotient map from d → ℝ onto the torus.

theorem TauCeti.UnitAddTorus.coe_eq_coe_iff {d : Type u_1} {x y : d → ℝ} : ((fun (i : d) => ↑(x i)) = fun (i : d) => ↑(y i)) ↔ ∃ (m : d → ℤ), y = x + fun (i : d) => ↑(m i)

Two points of d → ℝ have the same image on the torus exactly when they differ by an integer vector.

theorem TauCeti.UnitAddTorus.periodic_comp_coe {d : Type u_1} {X : Type u_2} (f : UnitAddTorus d → X) (m : d → ℤ) : Function.Periodic (fun (x : d → ℝ) => f fun (i : d) => ↑(x i)) fun (i : d) => ↑(m i)

The lift x ↦ f (fun i ↦ (x i : UnitAddCircle)) of a function on the torus is periodic with every integer vector as a period.

theorem TauCeti.UnitAddTorus.exists_continuous_comp_coe_eq {d : Type u_1} {X : Type u_2} [TopologicalSpace X] {G : (d → ℝ) → X} (hG : Continuous G) (hper : ∀ (m : d → ℤ), Function.Periodic G fun (i : d) => ↑(m i)) : ∃ (g : UnitAddTorus d → X), Continuous g ∧ ∀ (x : d → ℝ), (g fun (i : d) => ↑(x i)) = G x

A continuous function on d → ℝ with every integer vector as a period descends to a continuous function on the torus.