The real projective line is homeomorphic to the circle #
For n = 1, real projective space RP¹ is homeomorphic to the complex unit circle Circle via
the map sending the antipodal class of a unit vector (x₀, x₁) ∈ S¹ ⊆ ℝ², identified with
z = x₀ + i x₁, to z² ∈ Circle. The map is well-defined because (-z)² = z², and is a
continuous bijection from a compact space to a Hausdorff space, hence a homeomorphism.
Main declarations #
TauCeti.RealProjectiveSpace.Line.toCircle: the squared complex coordinate onRP¹.TauCeti.RealProjectiveSpace.Line.toCircle_apply_mk: evaluation oftoCircleon a unit vector.TauCeti.RealProjectiveSpace.Line.homeomorphCircle: the homeomorphismRP¹ ≃ₜ Circle.TauCeti.RealProjectiveSpace.Line.homeomorphCircle_apply: forward evaluation ofhomeomorphCircle.TauCeti.RealProjectiveSpace.Line.homeomorphCircle_symm_apply: backward evaluation ofhomeomorphCircle.TauCeti.RealProjectiveSpace.Line.basepoint: the natural basepoint ofRP¹corresponding to1 : Circle.TauCeti.RealProjectiveSpace.Line.toCircle_basepoint:toCirclesendsbasepointto1.
References #
This supports the n = 1 case of π₁(RPⁿ) in TauCetiRoadmap/UniversalCovers/README.md, Stage 4,
item 13.
The map from RP¹ to the complex circle induced by squaring a unit-vector representative.
Squaring makes the value independent of the choice between the two antipodal representatives.
Equations
- One or more equations did not get rendered due to their size.
Instances For
On a unit-vector representative, toCircle is the square of its complex coordinate.
The real projective line is homeomorphic to the circle. The map sends the antipodal class
of a unit vector, viewed as a complex number z, to z².
Equations
Instances For
The homeomorphism RP¹ ≃ₜ Circle evaluates as the squared-coordinate map.
The inverse homeomorphism Circle ≃ₜ RP¹ evaluates on squares of unit vectors.
A natural basepoint of RP¹: the antipodal class of the Euclidean unit vector corresponding
to 1 : ℂ under sphereHomeomorphCircle.