Lens spaces #
Let m be a positive integer and let ℓ₀, …, ℓₖ be residues modulo m that are units. The cyclic
group ℤ/m acts on the unit sphere S²ᵏ⁺¹ ⊆ ℂᵏ⁺¹ with a generator rotating the i-th
coordinate by the angle 2πℓᵢ/m:
(z₀, …, zₖ) ↦ (e^{2πiℓ₀/m} z₀, …, e^{2πiℓₖ/m} zₖ).
The action is free because each ℓᵢ is a unit modulo m, and its orbit space is the lens
space L(m; ℓ₀, …, ℓₖ). The three-dimensional lens space L(p, q) is
TauCeti.LensSpace p ![1, q].
The rotations are linear isometries of ℂᵏ⁺¹ viewed as a real inner product space, so the
acting group is realised as a subgroup TauCeti.lensGroup m ℓ of the linear isometry group,
which acts on the unit sphere through LinearIsometryEquiv.instMulActionUnitSphere. It is
the image of the homomorphism TauCeti.lensRotation m ℓ out of ℤ/m, written
multiplicatively, which is injective when there is at least one coordinate, as there is for
ℂᵏ⁺¹. A finite group acts properly discontinuously, so the projection from the sphere
is a quotient covering map. This file develops the topology of the quotient; its manifold
structure is in TauCeti.Geometry.Manifold.Instances.LensSpace, and its fundamental group in
TauCeti.AlgebraicTopology.UniversalCover.LensSpace.FundamentalGroup.
Requiring ℓᵢ to be a unit of ZMod m builds the coprimality condition into the type, and it
ensures that the prescribed action of ℤ/m is faithful and free. For m = 1 the acting group is
trivial and the lens space is a copy of the sphere.
Main definitions #
TauCeti.lensRotation: the representation ofℤ/monℂᵏby the weighted coordinate rotations.TauCeti.lensGroup: its image, a finite group of linear isometries acting freely on the unit sphere.TauCeti.LensSpace: the lens spaceL(m; ℓ₀, …, ℓₖ), the orbit space of the unit sphere ofℂᵏ⁺¹.TauCeti.LensSpace.mk: the projection from the sphere.TauCeti.LensSpace.inductionOn,TauCeti.LensSpace.lift, andTauCeti.LensSpace.lift_unique: elimination principles for the quotient.
Main results #
TauCeti.lensRotation_injective: the representation is faithful when there is at least one coordinate ([NeZero k]), soTauCeti.lensGroupEquividentifies the lens group withℤ/m.TauCeti.lensGroup_isCancelSMul: the lens group acts freely on the unit sphere.TauCeti.LensSpace.mk_eq_mk_iff: two unit vectors have the same image exactly when a rotation carries one to the other;TauCeti.LensSpace.mk_lensRotation_smulis the invariance of the projection under a rotation.TauCeti.LensSpace.isQuotientCoveringMap_mk: the projection from the sphere is a quotient covering map with group the lens group.- A lens space is compact, Hausdorff and path-connected.
References #
- A. Hatcher, Algebraic Topology, Cambridge University Press (2002), Example 2.43 (lens spaces as quotients of odd-dimensional spheres).
- D. Rolfsen, Knots and Links, Publish or Perish (1976), Chapter 9, §9G, Example 1: surgery on
the unknot with coefficient
b/agives the lens spaceL(b, a); the three-dimensional lens spaces are thus the manifolds obtained by Dehn surgery on the unknot. - The quotient API (
mk,mk_eq_mk_iff,isQuotientCoveringMap_mk, and the compactness and path-connectedness instances) is adapted from the real projective space formalization inTauCeti.AlgebraicTopology.UniversalCover.RealProjective.Basic.
The weighted rotation representation of ℤ/m on ℂᵏ, as real linear isometries: the residue
a rotates the i-th coordinate by the angle 2π ℓᵢ a / m.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The i-th coordinate of a rotated vector is the i-th coordinate of the vector multiplied
by the root of unity e^{2πi ℓᵢ a / m}.
A rotation fixes a nonzero coordinate only if it is the identity: the weight of the
coordinate is a unit modulo m, so the rotation angle 2π ℓᵢ a / m is a multiple of 2π only
for a = 0.
The weighted rotation representation of ℤ/m is faithful once there is a coordinate.
The lens group: the cyclic group of linear isometries of ℂᵏ generated by the rotation
(zᵢ) ↦ (e^{2πiℓᵢ/m} zᵢ), the image of TauCeti.lensRotation.
Equations
- TauCeti.lensGroup m ℓ = (TauCeti.lensRotation m ℓ).range
Instances For
The lens group acts on the unit sphere by isometries.
The lens group acts freely on the unit sphere: a nontrivial rotation moves every unit
vector, because each weight is a unit modulo m and a unit vector has a nonzero coordinate.
The lens space L(m; ℓ₀, …, ℓₖ): the orbit space of the unit sphere S²ᵏ⁺¹ ⊆ ℂᵏ⁺¹
under the free action of ℤ/m whose generator rotates the i-th coordinate by 2πℓᵢ/m. It is a
closed analytic manifold of dimension 2k + 1
(TauCeti.Geometry.Manifold.Instances.LensSpace). The three-dimensional lens space L(p, q) is
LensSpace p ![1, q].
Equations
- TauCeti.LensSpace m ℓ = MulAction.orbitRel.Quotient ↥(TauCeti.lensGroup m ℓ) ↑(Metric.sphere 0 1)
Instances For
The quotient topology on a lens space.
Equations
- TauCeti.LensSpace.instTopologicalSpace m ℓ = { IsOpen := TauCeti.LensSpace.instTopologicalSpace._aux_1 m ℓ, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }
The projection from the unit sphere of ℂᵏ⁺¹ to the lens space.
Equations
- TauCeti.LensSpace.mk m ℓ = Quotient.mk (MulAction.orbitRel ↥(TauCeti.lensGroup m ℓ) ↑(Metric.sphere 0 1))
Instances For
To prove a property of every point of a lens space, it suffices to prove it on the image of every unit vector.
Two unit vectors have the same image in the lens space exactly when a rotation by a residue
modulo m carries one to the other.
Rotating a unit vector does not change its image in the lens space.
A function on the unit sphere that is invariant under the rotations descends to the lens space.
Equations
- TauCeti.LensSpace.lift m ℓ f h = Quotient.lift f ⋯
Instances For
Lifting an invariant function and applying it to a representative recovers the original function.
A function out of a lens space agreeing with an invariant function on representatives is its lift.