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

@[deprecated]

def circle :

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

Please use Circle when referring to the circle as a type.

Equations

circle = Submonoid.unitSphere ℂ

Instances For

@[deprecated]

theorem mem_circle_iff_abs {z : ℂ} :

z ∈ circle ↔ Complex.abs z = 1

@[deprecated]

theorem mem_circle_iff_normSq {z : ℂ} :

z ∈ circle ↔ Complex.normSq z = 1

def Circle :

The unit circle in ℂ.

Equations

Circle = ↥(Submonoid.unitSphere ℂ)

Instances For

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_iff {x : Circle} {y : Circle} :

x = y ↔ ↑x = ↑y

theorem Circle.ext {x : Circle} {y : Circle} :

↑x = ↑y → x = y

theorem Circle.coe_injective :

Function.Injective Subtype.val

theorem Circle.coe_inj {x : Circle} {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 : Circle) (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 : Circle) (w : Circle) :

↑(z / w) = ↑z / ↑w

@[simp]

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

Circle.coeHom self = ↑self

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

@[deprecated Circle.abs_coe]

theorem abs_coe_circle (z : Circle) :

Complex.abs ↑z = 1

Alias of Circle.abs_coe.

@[deprecated Circle.normSq_coe]

theorem normSq_eq_of_mem_circle (z : Circle) :

Complex.normSq ↑z = 1

Alias of Circle.normSq_coe.

@[deprecated Circle.coe_ne_zero]

theorem ne_zero_of_mem_circle (z : Circle) :

↑z ≠ 0

Alias of Circle.coe_ne_zero.

@[deprecated Circle.coe_inv]

theorem coe_inv_circle (z : Circle) :

↑z⁻¹ = (↑z)⁻¹

Alias of Circle.coe_inv.

@[deprecated Circle.coe_inv_eq_conj]

theorem coe_inv_circle_eq_conj (z : Circle) :

↑z⁻¹ = (starRingEnd ℂ) ↑z

Alias of Circle.coe_inv_eq_conj.

@[deprecated Circle.coe_div]

theorem coe_div_circle (z : Circle) (w : Circle) :

↑(z / w) = ↑z / ↑w

Alias of Circle.coe_div.

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

Circle.toUnits z = Units.mk0 ↑z ⋯

instance Circle.instCompactSpace :

CompactSpace Circle

Equations

Circle.instCompactSpace = ⋯

instance Circle.instTopologicalGroup :

TopologicalGroup Circle

Equations

Circle.instTopologicalGroup = ⋯

instance Circle.instUniformSpace :

UniformSpace Circle

Equations

Circle.instUniformSpace = instUniformSpaceSubtype

instance Circle.instUniformGroup :

UniformGroup Circle

Equations

Circle.instUniformGroup = ⋯

@[simp]

theorem Circle.ofConjDivSelf_coe (z : ℂ) (hz : z ≠ 0) :

↑(Circle.ofConjDivSelf z hz) = (starRingEnd ℂ) z / z

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

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 : ℝ) :

↑(Circle.exp t) = Complex.exp (↑t * Complex.I)

@[simp]

theorem Circle.exp_zero :

Circle.exp 0 = 1

@[simp]

theorem Circle.exp_add (x : ℝ) (y : ℝ) :

Circle.exp (x + y) = Circle.exp x * Circle.exp y

@[simp]

theorem Circle.expHom_apply :

∀ (a : ℝ), Circle.expHom a = (⇑Additive.ofMul ∘ ⇑Circle.exp) a

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.exp_sub (x : ℝ) (y : ℝ) :

Circle.exp (x - y) = Circle.exp x / Circle.exp y

@[simp]

theorem Circle.exp_neg (x : ℝ) :

Circle.exp (-x) = (Circle.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 α β

Equations

⋯ = ⋯

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

SMulCommClass α Circle β

Equations

⋯ = ⋯

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

IsScalarTower Circle α β

Equations

⋯ = ⋯

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 α

Equations

⋯ = ⋯

@[simp]

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

‖u • v‖ = ‖v‖

@[deprecated Circle.exp]

def expMapCircle :

C(ℝ , Circle )

Alias of Circle.exp.

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

Equations

expMapCircle = Circle.exp

Instances For

@[deprecated Circle.coe_exp]

theorem expMapCircle_apply (t : ℝ) :

↑(Circle.exp t) = Complex.exp (↑t * Complex.I)

Alias of Circle.coe_exp.

@[deprecated Circle.exp_zero]

theorem expMapCircle_zero :

Circle.exp 0 = 1

Alias of Circle.exp_zero.

@[deprecated Circle.exp_sub]

theorem expMapCircle_sub (x : ℝ) (y : ℝ) :

Circle.exp (x - y) = Circle.exp x / Circle.exp y

Alias of Circle.exp_sub.

@[deprecated Circle.norm_smul]

theorem norm_circle_smul {E : Type u_4} [SeminormedAddCommGroup E] [NormedSpace ℂ E] (u : Circle) (v : E) :

‖u • v‖ = ‖v‖

Alias of Circle.norm_smul.