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