mathlib documentation

geometry.manifold.instances.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 and is smooth.

Implementation notes #

To borrow the smooth manifold structure cleanly, the circle needs to be defined using metric.sphere, and therefore 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_eq_of_mem_circle (z : ↥circle) :
complex.abs ↑z = 1
source
@[protected, instance]
def circle.group  :
group ↥circle
Equations
source
@[simp]
theorem coe_inv_circle (z : ↥circle) :
↑z⁻¹ = ⇑complex.conj ↑z
source
@[simp]
theorem coe_div_circle (z w : ↥circle) :
↑(z / w) = (↑z) * ⇑complex.conj ↑w
source
@[protected, instance]
def circle.topological_group  :
topological_group ↥circle
source
@[protected, instance]
def circle.charted_space  :
charted_space (euclidean_space ℝ (fin 1)) ↥circle

The unit circle in ℂ is a charted space modelled on euclidean_space ℝ (fin 1). This follows by definition from the corresponding result for metric.sphere.

Equations
source
@[protected, instance]
def circle.smooth_manifold_with_corners  :
smooth_manifold_with_corners 𝓘(ℝ, euclidean_space ℝ (fin 1)) ↥circle
source
@[protected, instance]
def circle.lie_group  :
lie_group 𝓘(ℝ, euclidean_space ℝ (fin 1)) ↥circle

The unit circle in ℂ is a Lie group.

source
def exp_map_circle (t : ℝ) :
↥circle

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

Equations
source
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
theorem times_cont_mdiff_exp_map_circle  :
times_cont_mdiff 𝓘(ℝ, ℝ) 𝓘(ℝ, euclidean_space ℝ (fin 1)) ⊤ exp_map_circle

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