Documentation

Mathlib.Analysis.Complex.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:

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 :

The unit circle in ℂ.

Equations

Circle = ↥(Submonoid.unitSphere ℂ)

Instances For

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

theorem Circle.norm_coe (z : Circle) :

‖↑z‖ = 1

@[deprecated Circle.norm_coe (since := "2025-02-16")]

theorem Circle.abs_coe (z : Circle) :

‖↑z‖ = 1

Alias of Circle.norm_coe.

@[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 }

Instances For

@[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 ℂ

Instances For

@[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) :

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

Equations

Circle.ofConjDivSelf z hz = ⟨(starRingEnd ℂ) z / z, ⋯⟩

Instances For

@[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 }

Instances For

@[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 }

Instances For

@[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 ℂ α] :

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‖