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 : Type

The unit circle in ℂ.

Equations

• Circle = ↥(Submonoid.unitSphere ℂ)

instance instCircleTopologicalSpace : TopologicalSpace Circle

Equations

• instCircleTopologicalSpace = instTopologicalSpaceSubtype

instance Circle.instCoeOut : CoeOut Circle ℂ

Equations

• Circle.instCoeOut = subtypeCoe

instance Circle.instCommGroup : CommGroup Circle

Equations

• Circle.instCommGroup = Metric.sphere.commGroup

instance Circle.instMetricSpace : MetricSpace Circle

Equations

• Circle.instMetricSpace = Subtype.metricSpace

theorem Circle.ext {x y : Circle} : ↑x = ↑y → x = y

theorem Circle.coe_injective : Function.Injective Subtype.val

theorem Circle.coe_inj {x y : Circle} : ↑x = ↑y ↔ x = y

@[simp]

theorem Circle.abs_coe (z : Circle) : Complex.abs ↑z = 1

@[simp]

theorem Circle.normSq_coe (z : Circle) : Complex.normSq ↑z = 1

@[simp]

theorem Circle.coe_ne_zero (z : Circle) : ↑z ≠ 0

@[simp]

theorem Circle.coe_one : ↑1 = 1

theorem Circle.coe_eq_one {x : Circle} : ↑x = 1 ↔ x = 1

@[simp]

theorem Circle.coe_mul (z w : Circle) : ↑(z * w) = ↑z * ↑w

@[simp]

theorem Circle.coe_inv (z : Circle) : ↑z⁻¹ = (↑z)⁻¹

theorem Circle.coe_inv_eq_conj (z : Circle) : ↑z⁻¹ = (starRingEnd ℂ) ↑z

@[simp]

theorem Circle.coe_div (z w : Circle) : ↑(z / w) = ↑z / ↑w

def Circle.coeHom : Circle →* ℂ

The coercion Circle → ℂ as a monoid homomorphism.

Equations

• Circle.coeHom = { toFun := Subtype.val, map_one' := Circle.coe_one, map_mul' := Circle.coe_mul }

@[simp]

theorem Circle.coeHom_apply (self : ↥(Submonoid.unitSphere ℂ)) : coeHom self = ↑self

def Circle.toUnits : Circle →* ℂˣ

The elements of the circle embed into the units.

Equations

• Circle.toUnits = unitSphereToUnits ℂ

@[simp]

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

instance Circle.instCompactSpace : CompactSpace Circle

instance Circle.instIsTopologicalGroup : IsTopologicalGroup Circle

instance Circle.instUniformSpace : UniformSpace Circle

Equations

• Circle.instUniformSpace = instUniformSpaceSubtype

instance Circle.instUniformGroup : UniformGroup Circle

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 = ⟨(starRingEnd ℂ) z / z, ⋯⟩

@[simp]

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

def Circle.exp : C(ℝ, Circle)

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

Equations

• Circle.exp = { toFun := fun (t : ℝ) => ⟨Complex.exp (↑t * Complex.I), ⋯⟩, continuous_toFun := Circle.exp.proof_2 }

@[simp]

theorem Circle.coe_exp (t : ℝ) : ↑(exp t) = Complex.exp (↑t * Complex.I)

@[simp]

theorem Circle.exp_zero : exp 0 = 1

@[simp]

theorem Circle.exp_add (x y : ℝ) : exp (x + y) = exp x * exp y

def Circle.expHom : ℝ →+ Additive Circle

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

Equations

• Circle.expHom = { toFun := ⇑Additive.ofMul ∘ ⇑Circle.exp, map_zero' := Circle.exp_zero, map_add' := Circle.exp_add }

@[simp]

theorem Circle.expHom_apply (a✝ : ℝ) : expHom a✝ = (⇑Additive.ofMul ∘ ⇑exp) a✝

@[simp]

theorem Circle.exp_sub (x y : ℝ) : exp (x - y) = exp x / exp y

@[simp]

theorem Circle.exp_neg (x : ℝ) : exp (-x) = (exp x)⁻¹

instance Circle.instSMul {α : Type u_1} [SMul ℂ α] : SMul Circle α

Equations

• Circle.instSMul = (Submonoid.unitSphere ℂ).smul

instance Circle.instSMulCommClass_left {α : Type u_1} {β : Type u_2} [SMul ℂ β] [SMul α β] [SMulCommClass ℂ α β] : SMulCommClass Circle α β

instance Circle.instSMulCommClass_right {α : Type u_1} {β : Type u_2} [SMul ℂ β] [SMul α β] [SMulCommClass α ℂ β] : SMulCommClass α Circle β

instance Circle.instIsScalarTower {α : Type u_1} {β : Type u_2} [SMul ℂ α] [SMul ℂ β] [SMul α β] [IsScalarTower ℂ α β] : IsScalarTower Circle α β

instance Circle.instMulAction {α : Type u_1} [MulAction ℂ α] : MulAction Circle α

Equations

• Circle.instMulAction = (Submonoid.unitSphere ℂ).mulAction

instance Circle.instDistribMulAction {M : Type u_3} [AddMonoid M] [DistribMulAction ℂ M] : DistribMulAction Circle M

Equations

• Circle.instDistribMulAction = (Submonoid.unitSphere ℂ).distribMulAction

theorem Circle.smul_def {α : Type u_1} [SMul ℂ α] (z : Circle) (a : α) : z • a = ↑z • a

instance Circle.instContinuousSMul {α : Type u_1} [TopologicalSpace α] [MulAction ℂ α] [ContinuousSMul ℂ α] : ContinuousSMul Circle α

@[simp]

theorem Circle.norm_smul {E : Type u_4} [SeminormedAddCommGroup E] [NormedSpace ℂ E] (u : Circle) (v : E) : ‖u • v‖ = ‖v‖