mathlib documentation

analysis.complex.circle

The circle #

This file defines circle to be the metric sphere (metric.sphere) in ℂ centred at 0 of radius 1. We equip it with the following structure:

We furthermore define exp_map_circle to be the natural map λ t, exp (t * I) from ℝ to circle, and show that this map is a group homomorphism.

Implementation notes #

Because later (in geometry.manifold.instances.sphere) one wants to equip the circle with a smooth manifold structure borrowed from metric.sphere, the underlying set is {z : ℂ | abs (z - 0) = 1}. This prevents certain algebraic facts from working definitionally -- for example, the circle is not defeq to {z : ℂ | abs z = 1}, which is the kernel of complex.abs considered as a homomorphism from ℂ to ℝ, nor is it defeq to {z : ℂ | norm_sq z = 1}, which is the kernel of the homomorphism complex.norm_sq from ℂ to ℝ.

source
def circle  :
submonoid ℂ

The unit circle in ℂ, here given the structure of a submonoid of ℂ.

Equations
source
@[simp]
theorem mem_circle_iff_abs {z : ℂ} :
z ∈ circle ↔ complex.abs z = 1
source
theorem circle_def  :
↑circle = {z : ℂ | complex.abs z = 1}
source
@[simp]
theorem abs_coe_circle (z : ↥circle) :
complex.abs ↑z = 1
source
theorem mem_circle_iff_norm_sq {z : ℂ} :
z ∈ circle ↔ ⇑complex.norm_sq z = 1
source
@[simp]
theorem norm_sq_eq_of_mem_circle (z : ↥circle) :
⇑complex.norm_sq ↑z = 1
source
theorem ne_zero_of_mem_circle (z : ↥circle) :
↑z ≠ 0
source
@[protected, instance]
def circle.comm_group  :
comm_group ↥circle
Equations
source
theorem coe_inv_circle_eq_conj (z : ↥circle) :
↑z⁻¹ = ⇑conj ↑z
source
@[simp]
theorem coe_inv_circle (z : ↥circle) :
↑z⁻¹ = (↑z)⁻¹
source
@[simp]
theorem coe_div_circle (z w : ↥circle) :
↑(z / w) = ↑z / ↑w
source
noncomputable def circle.to_units  :
↥circle →* ℂˣ

The elements of the circle embed into the units.

Equations
source
@[simp]
theorem circle.to_units_apply (x : ↥circle) :
⇑circle.to_units x = units.mk0 ↑x _
source
@[protected, instance]
def circle.compact_space  :
compact_space ↥circle
source
@[protected, instance]
def circle.topological_group  :
topological_group ↥circle
source
noncomputable def exp_map_circle  :
C(ℝ, ↥circle)

The map λ t, exp (t * I) from ℝ to the unit circle in ℂ.

Equations
source
@[simp]
theorem exp_map_circle_apply (t : ℝ) :
↑(⇑exp_map_circle t) = complex.exp ((↑t) * complex.I)
source
@[simp]
theorem exp_map_circle_zero  :
⇑exp_map_circle 0 = 1
source
@[simp]
theorem exp_map_circle_add (x y : ℝ) :
⇑exp_map_circle (x + y) = (⇑exp_map_circle x) * ⇑exp_map_circle y
source
@[simp]
theorem exp_map_circle_hom_apply (ᾰ : ℝ) :
⇑exp_map_circle_hom ᾰ = (⇑additive.of_mul ∘ ⇑exp_map_circle) ᾰ
source
noncomputable def exp_map_circle_hom  :
ℝ →+ additive ↥circle

The map λ t, exp (t * I) from ℝ to the unit circle in ℂ, considered as a homomorphism of groups.

Equations
source
@[simp]
theorem exp_map_circle_sub (x y : ℝ) :
⇑exp_map_circle (x - y) = ⇑exp_map_circle x / ⇑exp_map_circle y
source
@[simp]
theorem exp_map_circle_neg (x : ℝ) :
⇑exp_map_circle (-x) = (⇑exp_map_circle x)⁻¹