mathlib3 documentation

analysis.complex.circle

The circle #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

noncomputable def circle :

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

Equations

circle = submonoid.unit_sphere ℂ

Instances for ↥circle

@[simp]

theorem mem_circle_iff_abs {z : ℂ} :

z ∈ circle ↔ ⇑complex.abs z = 1

theorem circle_def :

↑circle = {z : ℂ | ⇑complex.abs z = 1}

@[simp]

theorem abs_coe_circle (z : ↥circle) :

⇑complex.abs ↑z = 1

theorem mem_circle_iff_norm_sq {z : ℂ} :

z ∈ circle ↔ ⇑complex.norm_sq z = 1

@[simp]

theorem norm_sq_eq_of_mem_circle (z : ↥circle) :

⇑complex.norm_sq ↑z = 1

theorem ne_zero_of_mem_circle (z : ↥circle) :

@[protected, instance]

noncomputable def circle.comm_group :

comm_group ↥circle

Equations

circle.comm_group = metric.sphere.comm_group

@[simp]

theorem coe_inv_circle (z : ↥circle) :

↑z⁻¹ = (↑z)⁻¹

theorem coe_inv_circle_eq_conj (z : ↥circle) :

↑z⁻¹ = ⇑(star_ring_end ℂ) ↑z

@[simp]

theorem coe_div_circle (z w : ↥circle) :

↑(z / w) = ↑z / ↑w

noncomputable def circle.to_units :

↥circle →* ℂ ˣ

The elements of the circle embed into the units.

Equations

circle.to_units = unit_sphere_to_units ℂ

@[simp]

theorem circle.to_units_apply (z : ↥circle) :

⇑circle.to_units z = units.mk0 ↑z _

@[protected, instance]

def circle.compact_space :

compact_space ↥circle

@[protected, instance]

def circle.topological_group :

topological_group ↥circle

@[simp]

theorem circle.of_conj_div_self_coe (z : ℂ) (hz : z ≠ 0) :

↑(circle.of_conj_div_self z hz) = ⇑(star_ring_end ℂ) z / z

noncomputable def circle.of_conj_div_self (z : ℂ) (hz : z ≠ 0) :

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

Equations

circle.of_conj_div_self z hz = ⟨⇑(star_ring_end ℂ) z / z, _⟩

noncomputable def exp_map_circle :

C(ℝ , ↥circle )

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

Equations

exp_map_circle = {to_fun := λ (t : ℝ), ⟨cexp (↑t * complex.I), _⟩, continuous_to_fun := exp_map_circle._proof_2}

@[simp]

theorem exp_map_circle_apply (t : ℝ) :

↑(⇑exp_map_circle t) = cexp (↑t * complex.I)

@[simp]

theorem exp_map_circle_zero :

⇑exp_map_circle 0 = 1

@[simp]

theorem exp_map_circle_add (x y : ℝ) :

⇑exp_map_circle (x + y) = ⇑exp_map_circle x * ⇑exp_map_circle y

@[simp]

theorem exp_map_circle_hom_apply (ᾰ : ℝ) :

⇑exp_map_circle_hom ᾰ = (⇑additive.of_mul ∘ ⇑exp_map_circle) ᾰ

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

exp_map_circle_hom = {to_fun := ⇑additive.of_mul ∘ ⇑exp_map_circle, map_zero' := exp_map_circle_zero, map_add' := exp_map_circle_add}

@[simp]

theorem exp_map_circle_sub (x y : ℝ) :

⇑exp_map_circle (x - y) = ⇑exp_map_circle x / ⇑exp_map_circle y

@[simp]

theorem exp_map_circle_neg (x : ℝ) :

⇑exp_map_circle (-x) = (⇑exp_map_circle x)⁻¹