# Documentation

Mathlib.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 expMapCircle to be the natural map fun 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 : ℂ | normSq z = 1}, which is the kernel of the homomorphism Complex.normSq from ℂ to ℝ.

def circle :

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

Instances For
@[simp]
theorem mem_circle_iff_abs {z : } :
= 1
theorem circle_def :
= {z | = 1}
@[simp]
theorem abs_coe_circle (z : { x // }) :
Complex.abs z = 1
@[simp]
theorem normSq_eq_of_mem_circle (z : { x // }) :
= 1
theorem ne_zero_of_mem_circle (z : { x // }) :
z 0
instance commGroup :
CommGroup { x // }
@[simp]
theorem coe_inv_circle (z : { x // }) :
z⁻¹ = (z)⁻¹
theorem coe_inv_circle_eq_conj (z : { x // }) :
z⁻¹ = ↑() z
@[simp]
theorem coe_div_circle (z : { x // }) (w : { x // }) :
↑(z / w) = z / w
def circle.toUnits :
{ x // } →*

The elements of the circle embed into the units.

Instances For
@[simp]
theorem circle.toUnits_apply (z : { x // }) :
= Units.mk0 z (_ : z 0)
@[simp]
theorem circle.ofConjDivSelf_coe (z : ) (hz : z 0) :
↑() = ↑() z / z
def circle.ofConjDivSelf (z : ) (hz : z 0) :
{ x // }

If z is a nonzero complex number, then conj z / z belongs to the unit circle.

Instances For
def expMapCircle :
C(, { x // })

The map fun t => exp (t * I) from ℝ to the unit circle in ℂ.

Instances For
@[simp]
theorem expMapCircle_apply (t : ) :
↑() = Complex.exp ()
@[simp]
theorem expMapCircle_zero :
= 1
@[simp]
theorem expMapCircle_add (x : ) (y : ) :
expMapCircle (x + y) =
@[simp]
theorem expMapCircleHom_apply :
∀ (a : ),

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

Instances For
@[simp]
theorem expMapCircle_sub (x : ) (y : ) :
expMapCircle (x - y) =
@[simp]
theorem expMapCircle_neg (x : ) :