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

Equations

• circle = Submonoid.unitSphere ℂ

@[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_normSq {z : ℂ} : z ∈ circle ↔ Complex.normSq z = 1

@[simp]

theorem normSq_eq_of_mem_circle (z : ↥circle) : Complex.normSq ↑z = 1

theorem ne_zero_of_mem_circle (z : ↥circle) : ↑z ≠ 0

instance commGroup : CommGroup ↥circle

Equations

• commGroup = Metric.sphere.commGroup

@[simp]

theorem coe_inv_circle (z : ↥circle) : ↑z⁻¹ = (↑z)⁻¹

theorem coe_inv_circle_eq_conj (z : ↥circle) : ↑z⁻¹ = (starRingEnd ℂ) ↑z

@[simp]

theorem coe_div_circle (z : ↥circle) (w : ↥circle) : ↑(z / w) = ↑z / ↑w

def circle.toUnits : ↥circle →* ℂˣ

The elements of the circle embed into the units.

Equations

• circle.toUnits = unitSphereToUnits ℂ

@[simp]

theorem circle.toUnits_apply (z : ↥circle) : circle.toUnits z = Units.mk0 ↑z ⋯

instance instCompactSpaceSubtypeComplexMemSubmonoidToMulOneClassToMulZeroOneClassToNonAssocSemiringInstSemiringComplexInstMembershipInstSetLikeSubmonoidCircleInstTopologicalSpaceSubtypeToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingInstNormedFieldComplex : CompactSpace ↥circle

Equations

• One or more equations did not get rendered due to their size.

instance instTopologicalGroupSubtypeComplexMemSubmonoidToMulOneClassToMulZeroOneClassToNonAssocSemiringInstSemiringComplexInstMembershipInstSetLikeSubmonoidCircleInstTopologicalSpaceSubtypeToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingInstNormedFieldComplexToGroupCommGroup : TopologicalGroup ↥circle

Equations

• One or more equations did not get rendered due to their size.

instance instUniformGroupSubtypeComplexMemSubmonoidToMulOneClassToMulZeroOneClassToNonAssocSemiringInstSemiringComplexInstMembershipInstSetLikeSubmonoidCircleInstUniformSpaceSubtypeToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingInstNormedFieldComplexToGroupCommGroup : UniformGroup ↥circle

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

def circle.ofConjDivSelf (z : ℂ) (hz : z ≠ 0) : ↥circle

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

Equations

• circle.ofConjDivSelf z hz = { val := (starRingEnd ℂ) z / z, property := ⋯ }

def expMapCircle : C(ℝ, ↥circle)

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

Equations

• expMapCircle = { toFun := fun (t : ℝ) => { val := Complex.exp (↑t * Complex.I), property := ⋯ }, continuous_toFun := expMapCircle.proof_2 }

@[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 ↥circle

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

Equations

• expMapCircleHom = { toZeroHom := { toFun := ⇑Additive.ofMul ∘ ⇑expMapCircle, map_zero' := expMapCircle_zero }, map_add' := expMapCircle_add }

@[simp]

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

@[simp]

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

@[simp]

theorem norm_circle_smul {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℂ E] (u : ↥circle) (v : E) : ‖u • v‖ = ‖v‖