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 .

def circle  :

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

Equations
@[simp]
theorem mem_circle_iff_abs (z : ) :
theorem circle_def  :
@[simp]
@[instance]
Equations
@[simp]
theorem coe_div_circle (z w : circle) :
@[instance]

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
@[instance]

The unit circle in is a Lie group.

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

Equations

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

Equations

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