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 : Submonoid ℂ

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

@[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 : { x // x ∈ circle }) : ↑Complex.abs ↑z = 1

theorem mem_circle_iff_normSq {z : ℂ} : z ∈ circle ↔ ↑Complex.normSq z = 1

@[simp]

theorem normSq_eq_of_mem_circle (z : { x // x ∈ circle }) : ↑Complex.normSq ↑z = 1

theorem ne_zero_of_mem_circle (z : { x // x ∈ circle }) : ↑z ≠ 0

instance commGroup : CommGroup { x // x ∈ circle }

@[simp]

theorem coe_inv_circle (z : { x // x ∈ circle }) : ↑z⁻¹ = (↑z)⁻¹

theorem coe_inv_circle_eq_conj (z : { x // x ∈ circle }) : ↑z⁻¹ = ↑(starRingEnd ℂ) ↑z

@[simp]

theorem coe_div_circle (z : { x // x ∈ circle }) (w : { x // x ∈ circle }) : ↑(z / w) = ↑z / ↑w

def circle.toUnits : { x // x ∈ circle } →* ℂˣ

The elements of the circle embed into the units.

@[simp]

theorem circle.toUnits_apply (z : { x // x ∈ circle }) : ↑circle.toUnits z = Units.mk0 ↑z (_ : ↑z ≠ 0)

instance instCompactSpaceSubtypeComplexMemSubmonoidToMulOneClassToMulZeroOneClassToNonAssocSemiringInstSemiringComplexInstMembershipInstSetLikeSubmonoidCircleInstTopologicalSpaceSubtypeToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingInstNormedFieldComplex : CompactSpace { x // x ∈ circle }

instance instTopologicalGroupSubtypeComplexMemSubmonoidToMulOneClassToMulZeroOneClassToNonAssocSemiringInstSemiringComplexInstMembershipInstSetLikeSubmonoidCircleInstTopologicalSpaceSubtypeToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingInstNormedFieldComplexToGroupCommGroup : TopologicalGroup { x // x ∈ circle }

@[simp]

theorem circle.ofConjDivSelf_coe (z : ℂ) (hz : z ≠ 0) : ↑(circle.ofConjDivSelf z hz) = ↑(starRingEnd ℂ) z / z

def circle.ofConjDivSelf (z : ℂ) (hz : z ≠ 0) : { x // x ∈ circle }

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

def expMapCircle : C(ℝ, { x // x ∈ circle })

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

@[simp]

theorem expMapCircle_apply (t : ℝ) : ↑(↑expMapCircle t) = Complex.exp (↑t * Complex.I)

@[simp]

theorem expMapCircle_zero : ↑expMapCircle 0 = 1

@[simp]

theorem expMapCircle_add (x : ℝ) (y : ℝ) : ↑expMapCircle (x + y) = ↑expMapCircle x * ↑expMapCircle y

@[simp]

theorem expMapCircleHom_apply : ∀ (a : ℝ), ↑expMapCircleHom a = (↑Additive.ofMul ∘ ↑expMapCircle) a

def expMapCircleHom : ℝ →+ Additive { x // x ∈ circle }

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

@[simp]

theorem expMapCircle_sub (x : ℝ) (y : ℝ) : ↑expMapCircle (x - y) = ↑expMapCircle x / ↑expMapCircle y

@[simp]

theorem expMapCircle_neg (x : ℝ) : ↑expMapCircle (-x) = (↑expMapCircle x)⁻¹