Loops as maps out of the circle

The standard quotient TauCeti.unitToCircle : C(I, Circle), t ↦ exp (2πit), collapses the endpoints 0 and 1 of the unit interval to 1 ∈ Circle and maps (0, 1) bijectively onto Circle \ {1}. A loop γ : Path x x closes up, so it factors through unitToCircle. The factorization is Path.toCircle γ : C(Circle, X): it sends unitToCircle t = exp (2πit) to γ t, and the point 1 to x.

Maps out of a wedge of circles are assembled from maps out of the circles, so this is how loops in a space give maps out of a wedge of circles.

In the other direction, the (p, q) curve t ↦ (exp (2πipt), exp (2πiqt)) is the standard loop on the torus S¹ × S¹ winding p times around the first circle and q times around the second.

Main definitions

• TauCeti.unitToCircle: the standard quotient C(I, Circle), t ↦ Circle.exp (2 * π * t).
• Path.toCircle: a loop, read as a map from the unit circle.
• TauCeti.torusCurve p q: the (p, q) curve on S¹ × S¹, a loop at (1, 1).
• TauCeti.torusGluing: a torus homeomorphism given by a determinant-one integer matrix.

Main results

• TauCeti.unitToCircle_surjective, TauCeti.unitToCircle_eq_one_iff, TauCeti.eq_or_of_unitToCircle_eq: quotient properties of unitToCircle.
• Path.toCircle_unitToCircle, Path.toCircle_exp: unitToCircle t = exp (2πit) goes to γ t.
• Path.toCircle_one: the point 1 goes to the base point.

noncomputable def TauCeti.unitToCircle : C(↑unitInterval, Circle)

The standard quotient I → Circle, t ↦ exp(2πit), collapsing the endpoints 0 and 1 to 1 ∈ Circle and mapping (0, 1) bijectively onto Circle \ {1}.

theorem TauCeti.unitToCircle_apply (t : ↑unitInterval) : unitToCircle t = Circle.exp (2 * Real.pi * ↑t)

@[simp]

theorem TauCeti.unitToCircle_zero : unitToCircle 0 = 1

@[simp]

theorem TauCeti.unitToCircle_one : unitToCircle 1 = 1

theorem TauCeti.unitToCircle_surjective : Function.Surjective ⇑unitToCircle

unitToCircle is surjective: every z : Circle is exp (angleDiff 1 z) for angleDiff 1 z ∈ [0, 2π).

@[simp]

theorem TauCeti.unitToCircle_eq_one_iff (t : ↑unitInterval) : unitToCircle t = 1 ↔ t = 0 ∨ t = 1

unitToCircle sends exactly the endpoints 0 and 1 to 1 ∈ Circle.

theorem TauCeti.eq_or_of_unitToCircle_eq {s t : ↑unitInterval} (h : unitToCircle s = unitToCircle t) : s = t ∨ s = 0 ∧ t = 1 ∨ s = 1 ∧ t = 0

Two points of I with the same image under unitToCircle are equal or opposite endpoints.

noncomputable def Path.toCircle {X : Type u_1} [TopologicalSpace X] {x : X} (γ : Path x x) : C(Circle, X)

A loop γ at x, read as a map from the unit circle: unitToCircle t = exp (2πit) goes to γ t. It is γ extended to ℝ and descended to AddCircle 1, which is identified with the circle by AddCircle.homeomorphCircle.

@[simp]

theorem Path.toCircle_unitToCircle {X : Type u_1} [TopologicalSpace X] {x : X} (γ : Path x x) (t : ↑unitInterval) : γ.toCircle (TauCeti.unitToCircle t) = γ t

The point unitToCircle t of the circle goes to γ t.

theorem Path.toCircle_exp {X : Type u_1} [TopologicalSpace X] {x : X} (γ : Path x x) (t : ↑unitInterval) : γ.toCircle (Circle.exp (2 * Real.pi * ↑t)) = γ t

The point exp (2πit) of the circle goes to γ t.

@[simp]

theorem Path.toCircle_one {X : Type u_1} [TopologicalSpace X] {x : X} (γ : Path x x) : γ.toCircle 1 = x

The point 1 of the circle goes to the base point of the loop.

noncomputable def TauCeti.torusCurve (p q : ℤ) : Path (1, 1) (1, 1)

The (p, q) curve t ↦ (exp (2πipt), exp (2πiqt)) on the torus S¹ × S¹, a loop at (1, 1) winding p times around the first circle and q times around the second.

@[simp]

theorem TauCeti.torusCurve_apply (p q : ℤ) (t : ↑unitInterval) : (torusCurve p q) t = (Circle.exp (2 * Real.pi * (↑p * ↑t)), Circle.exp (2 * Real.pi * (↑q * ↑t)))

The gluing of the boundary tori

noncomputable def TauCeti.torusGluing (p q s t : ℤ) (h : s * p + t * q = 1) : Circle × Circle ≃ₜ Circle × Circle

The homeomorphism (a, b) ↦ (a ^ p b ^ (-t), a ^ q b ^ s) of the torus S¹ × S¹ given by the matrix [[p, -t], [q, s]] of determinant s p + t q = 1.

@[simp]

theorem TauCeti.torusGluing_apply (p q s t : ℤ) (h : s * p + t * q = 1) (x : Circle × Circle) : (torusGluing p q s t h) x = (x.1 ^ p * x.2 ^ (-t), x.1 ^ q * x.2 ^ s)

The value of the determinant-one torus map.

@[simp]

theorem TauCeti.torusGluing_symm_apply (p q s t : ℤ) (h : s * p + t * q = 1) (x : Circle × Circle) : (torusGluing p q s t h).symm x = (x.1 ^ s * x.2 ^ t, x.1 ^ (-q) * x.2 ^ p)

The inverse of the determinant-one torus map.

theorem TauCeti.torusGluing_torusCurve (p q s t : ℤ) (h : s * p + t * q = 1) (τ : ↑unitInterval) : (torusGluing p q s t h) ((torusCurve 1 0) τ) = (torusCurve p q) τ

The gluing carries the meridian (a, 1) to the (p, q) curve.