Identification of the unit circle in two-dimensional Euclidean space with the complex circle

The unit sphere sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 is isometric to Mathlib's complex unit circle Circle = {z : ℂ | ‖z‖ = 1} via the standard orthonormal basis isometry Complex.orthonormalBasisOneI.

Main declarations

• TauCeti.EuclideanSpace.sphereIsometryEquivCircle: the isometry equivalence between the unit circle in two-dimensional Euclidean space and Circle.
• TauCeti.EuclideanSpace.sphereHomeomorphCircle: the homeomorphism between the unit circle in two-dimensional Euclidean space and Circle.
• TauCeti.EuclideanSpace.coe_sphereIsometryEquivCircle_apply: forward evaluation of the isometry equivalence on underlying points.
• TauCeti.EuclideanSpace.coe_sphereHomeomorphCircle_apply: forward evaluation of the homeomorphism on underlying points.
• TauCeti.EuclideanSpace.coe_sphereIsometryEquivCircle_symm_apply: backward evaluation of the isometry equivalence on underlying points.
• TauCeti.EuclideanSpace.coe_sphereHomeomorphCircle_symm_apply: backward evaluation of the homeomorphism on underlying points.
• TauCeti.EuclideanSpace.sphereIsometryEquivCircle_neg: the isometry equivalence negates under the antipodal map.
• TauCeti.EuclideanSpace.sphereHomeomorphCircle_neg: the homeomorphism negates under the antipodal map.

noncomputable def TauCeti.EuclideanSpace.sphereIsometryEquivCircle : ↑(Metric.sphere 0 1) ≃ᵢ Circle

The unit circle in two-dimensional real Euclidean space is isometric to Mathlib's complex unit circle Circle.

Note: Circle is by definition the unit sphere sphere (0 : ℂ) 1 in ℂ (via Submonoid.unitSphere ℂ), so the metric and topological instances agree definitionally with those on sphere (0 : ℂ) 1. The type ascription Circle is therefore definitionally equal to sphere (0 : ℂ) 1.

Equations

• TauCeti.EuclideanSpace.sphereIsometryEquivCircle = Complex.orthonormalBasisOneI.repr.symm.unitSphereIsometryEquiv

noncomputable def TauCeti.EuclideanSpace.sphereHomeomorphCircle : ↑(Metric.sphere 0 1) ≃ₜ Circle

The unit circle in two-dimensional real Euclidean space is homeomorphic to Mathlib's complex unit circle Circle.

Equations

• TauCeti.EuclideanSpace.sphereHomeomorphCircle = TauCeti.EuclideanSpace.sphereIsometryEquivCircle.toHomeomorph

@[simp]

theorem TauCeti.EuclideanSpace.coe_sphereIsometryEquivCircle_apply (x : ↑(Metric.sphere 0 1)) : ↑(sphereIsometryEquivCircle x) = Complex.orthonormalBasisOneI.repr.symm ↑x

The Euclidean-circle isometry is the standard orthonormal-coordinate isometry on underlying points.

@[simp]

theorem TauCeti.EuclideanSpace.coe_sphereHomeomorphCircle_apply (x : ↑(Metric.sphere 0 1)) : ↑(sphereHomeomorphCircle x) = Complex.orthonormalBasisOneI.repr.symm ↑x

The Euclidean-circle homeomorphism is the standard orthonormal-coordinate isometry on underlying points.

@[simp]

theorem TauCeti.EuclideanSpace.coe_sphereIsometryEquivCircle_symm_apply (z : Circle) : ↑(sphereIsometryEquivCircle.symm z) = Complex.orthonormalBasisOneI.repr ↑z

The inverse Euclidean-circle isometry is the standard coordinate representation on underlying points.

@[simp]

theorem TauCeti.EuclideanSpace.coe_sphereHomeomorphCircle_symm_apply (z : Circle) : ↑(sphereHomeomorphCircle.symm z) = Complex.orthonormalBasisOneI.repr ↑z

The inverse Euclidean-circle homeomorphism is the standard coordinate representation on underlying points.

@[simp]

theorem TauCeti.EuclideanSpace.sphereIsometryEquivCircle_neg (x : ↑(Metric.sphere 0 1)) : sphereIsometryEquivCircle (-x) = -sphereIsometryEquivCircle x

The Euclidean-circle isometry negates under the antipodal map.

@[simp]

theorem TauCeti.EuclideanSpace.sphereHomeomorphCircle_neg (x : ↑(Metric.sphere 0 1)) : sphereHomeomorphCircle (-x) = -sphereHomeomorphCircle x

The Euclidean-circle homeomorphism negates under the antipodal map.