mathlibdocumentation

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:

• a submonoid of ℂ
• a group
• a topological group

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 ℝ.

def circle  :

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

Equations
@[simp]
theorem mem_circle_iff_abs {z : } :
= 1
theorem circle_def  :
circle = {z : | = 1}
@[simp]
theorem abs_coe_circle (z : circle) :
@[simp]
@[protected, instance]
Equations
@[simp]
theorem coe_inv_circle (z : circle) :
@[simp]
theorem coe_div_circle (z w : circle) :
(z / w) = z / w
noncomputable def circle.to_units  :

The elements of the circle embed into the units.

Equations
@[simp]
theorem circle.to_units_apply (x : circle) :
@[protected, instance]
@[protected, instance]
noncomputable def exp_map_circle  :

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

Equations
@[simp]
@[simp]
theorem exp_map_circle_zero  :
@[simp]
theorem exp_map_circle_add (x y : ) :
@[simp]
theorem exp_map_circle_hom_apply (ᾰ : ) :
noncomputable def exp_map_circle_hom  :

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

Equations
@[simp]
theorem exp_map_circle_sub (x y : ) :