The unit circle: the unit sphere of ℂ, the exponential and the coordinate function

Mathlib's unit circle Circle is a type synonym for the unit sphere sphere (0 : ℂ) 1, carrying its group structure. This file records the identification as a homeomorphism, so that results stated for unit spheres of real normed spaces (such as their CW structures) apply to Circle without unfolding the synonym.

It also packages the exponential t ↦ exp (i t) as a continuous homomorphism from the real line, and records that the coordinate function z ↦ z is a unitary element of C(S¹, ℂ).

Main declarations

• Circle.homeomorphSphere: Circle ≃ₜ sphere (0 : ℂ) 1, the identity on underlying complex numbers.
• Circle.expContinuousMonoidHom: t ↦ exp (i t) as a continuous homomorphism Multiplicative ℝ →ₜ* Circle.
• Circle.coordinate: the coordinate function z ↦ z in C(S¹, ℂ), and Circle.coordinate_mem_unitary.
• Circle.re_sq_add_im_sq and Circle.coe_add_inv_coe: Re z ^ 2 + Im z ^ 2 = 1 and z + z⁻¹ = 2 Re z on the circle, and Complex.re_sq_add_im_sq_of_mem_sphere, the first identity for a point of sphere (0 : ℂ) 1.
• Circle.exp_pow_eq_neg_one and Circle.mixed_power_rotation_factor: power identities for complex exponentials on the circle.
• Circle.exists_pow_nat_eq: every point of the circle has an n-th root on the circle.
• Circle.differentiableAt_coe_inv: the pointwise inverse of a differentiable circle-valued map is differentiable.

noncomputable def Circle.homeomorphSphere : Circle ≃ₜ ↑(Metric.sphere 0 1)

The unit circle Circle is homeomorphic to the unit sphere sphere (0 : ℂ) 1, by the identity on underlying complex numbers.

@[simp]

theorem Circle.coe_homeomorphSphere_apply (z : Circle) : ↑(homeomorphSphere z) = ↑z

@[simp]

theorem Circle.coe_homeomorphSphere_symm_apply (z : ↑(Metric.sphere 0 1)) : ↑(homeomorphSphere.symm z) = ↑z

theorem Circle.re_sq_add_im_sq (z : Circle) : (↑z).re ^ 2 + (↑z).im ^ 2 = 1

The real and imaginary parts of a point of the circle satisfy Re z ^ 2 + Im z ^ 2 = 1.

theorem Complex.re_sq_add_im_sq_of_mem_sphere {z : ℂ} (hz : z ∈ Metric.sphere 0 1) : z.re ^ 2 + z.im ^ 2 = 1

The real and imaginary parts of a point of the unit sphere of ℂ satisfy Re z ^ 2 + Im z ^ 2 = 1.

theorem Circle.coe_add_inv_coe (z : Circle) : ↑z + (↑z)⁻¹ = 2 * ↑(↑z).re

For a point of the circle, z + z⁻¹ = 2 Re z.

theorem Circle.exp_pow_eq_neg_one (d : ℕ) (hd : d ≠ 0) : ↑(exp (Real.pi / ↑d)) ^ d = -1

Raising exp (π * I / d) to a nonzero natural power d gives -1.

theorem Circle.mixed_power_rotation_factor {p q : ℕ} (hpq : p ≠ q) : ↑(exp (Real.pi / ↑(if p < q then q - p else p - q))) ^ p * (starRingEnd ℂ) ↑(exp (Real.pi / ↑(if p < q then q - p else p - q))) ^ q = -1

For distinct natural powers, rotation by exp (π * I / |p - q|) negates their mixed power.

theorem Circle.exists_pow_nat_eq (z : Circle) {n : ℕ} (hn : n ≠ 0) : ∃ (y : Circle), y ^ n = z

Every point of the circle has an n-th root on the circle, for n ≠ 0: exp (i arg z / n).

theorem Circle.differentiableAt_coe_inv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {u : E → Circle} {z : E} (hu : DifferentiableAt ℝ (fun (w : E) => ↑(u w)) z) : DifferentiableAt ℝ (fun (w : E) => ↑(u⁻¹ w)) z

The pointwise inverse of a circle-valued map that is differentiable at z, as a map into ℂ, is differentiable at z.

noncomputable def Circle.expContinuousMonoidHom : Multiplicative ℝ →ₜ* Circle

The map t ↦ exp (i t) from the real line to the circle, as a continuous homomorphism from Multiplicative ℝ.

@[simp]

theorem Circle.expContinuousMonoidHom_apply (t : Multiplicative ℝ) : expContinuousMonoidHom t = exp (Multiplicative.toAdd t)

def Circle.coordinate : C(Circle, ℂ)

The coordinate function z ↦ z on the circle.

@[simp]

theorem Circle.coordinate_apply (z : Circle) : coordinate z = ↑z

@[simp]

theorem Circle.star_coordinate_mul : star coordinate * coordinate = 1

@[simp]

theorem Circle.coordinate_mul_star : coordinate * star coordinate = 1

theorem Circle.coordinate_mem_unitary : coordinate ∈ unitary C(Circle, ℂ)

The coordinate function is a unitary element of C(S¹, ℂ).