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:

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 .

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

Equations
Instances For
    @[simp]
    theorem circle_def :
    circle = {z : | Complex.abs z = 1}
    @[simp]
    theorem abs_coe_circle (z : circle) :
    Complex.abs z = 1
    @[simp]
    theorem ne_zero_of_mem_circle (z : circle) :
    z 0
    Equations
    @[simp]
    theorem coe_inv_circle (z : circle) :
    z⁻¹ = (z)⁻¹
    @[simp]
    theorem coe_div_circle (z : circle) (w : circle) :
    (z / w) = z / w

    The elements of the circle embed into the units.

    Equations
    Instances For
      @[simp]
      theorem circle.toUnits_apply (z : circle) :
      circle.toUnits z = Units.mk0 z (_ : z 0)
      @[simp]
      theorem circle.ofConjDivSelf_coe (z : ) (hz : z 0) :
      def circle.ofConjDivSelf (z : ) (hz : z 0) :

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

      Equations
      Instances For

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

        Equations
        Instances For
          @[simp]
          @[simp]

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

          Equations
          Instances For
            @[simp]