Lens spaces are analytic manifolds

The lens space TauCeti.LensSpace m ℓ is the orbit space of the unit sphere S²ᵏ⁺¹ ⊆ ℂᵏ⁺¹ under the free action of the finite lens group TauCeti.lensGroup m ℓ (TauCeti.AlgebraicTopology.UniversalCover.LensSpace.Basic). The lens group consists of linear isometries, so it acts on the sphere by analytic diffeomorphisms, and the orbit space is an analytic manifold of dimension 2k + 1 by TauCeti.instIsManifoldQuotient. The projection from the sphere is an analytic local diffeomorphism.

As for Mathlib's spheres (EuclideanSpace.instChartedSpaceSphere), the manifold structure is stated for any n with Fact (finrank ℝ (EuclideanSpace ℂ (Fin (k + 1))) = n + 1), and the instance TauCeti.factFinrankEuclideanSpaceComplex (TauCeti.Analysis.InnerProductSpace.Euclidean.Space) supplies n = 2k + 1. This lets instance search find the structure for a concrete model such as 𝓡 3, where it could not solve 2 * k + 1 = 3 for k.

Main results

• TauCeti.LensSpace.instIsManifold: the lens space is an analytic manifold modelled on ℝ²ᵏ⁺¹.
• TauCeti.LensSpace.isLocalDiffeomorph_mk: the projection from the sphere is an analytic local diffeomorphism.

References

• A. Hatcher, Algebraic Topology, Cambridge University Press (2002), Example 2.43 (lens spaces as quotients of odd-dimensional spheres).

instance TauCeti.instContMDiffConstSMulRealEuclideanSpaceFinModelWithCornersSelfTopWithTopENatSubtypeLinearIsometryEquivIdComplexHAddNatOfNatMemSubgroupLensGroupElemSphere (m : ℕ) [NeZero m] {k : ℕ} (ℓ : Fin (k + 1) → (ZMod m)ˣ) {n : ℕ} [Fact (Module.finrank ℝ (EuclideanSpace ℂ (Fin (k + 1))) = n + 1)] : ContMDiffConstSMul (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ⊤ ↥(lensGroup m ℓ) ↑(Metric.sphere 0 1)

The lens group acts on the unit sphere of ℂᵏ⁺¹ by analytic diffeomorphisms.

@[instance_reducible]

noncomputable instance TauCeti.LensSpace.instChartedSpace (m : ℕ) [NeZero m] {k : ℕ} (ℓ : Fin (k + 1) → (ZMod m)ˣ) {n : ℕ} [Fact (Module.finrank ℝ (EuclideanSpace ℂ (Fin (k + 1))) = n + 1)] : ChartedSpace (EuclideanSpace ℝ (Fin n)) (LensSpace m ℓ)

The charts of a lens space, pushed forward from the sphere along the orbit projection.

Equations

• One or more equations did not get rendered due to their size.

instance TauCeti.LensSpace.instIsManifold (m : ℕ) [NeZero m] {k : ℕ} (ℓ : Fin (k + 1) → (ZMod m)ˣ) {n : ℕ} [Fact (Module.finrank ℝ (EuclideanSpace ℂ (Fin (k + 1))) = n + 1)] : IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ⊤ (LensSpace m ℓ)

A lens space is an analytic manifold of dimension 2k + 1.

theorem TauCeti.LensSpace.isLocalDiffeomorph_mk (m : ℕ) [NeZero m] {k : ℕ} (ℓ : Fin (k + 1) → (ZMod m)ˣ) {n : ℕ} [Fact (Module.finrank ℝ (EuclideanSpace ℂ (Fin (k + 1))) = n + 1)] : IsLocalDiffeomorph (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ⊤ (mk m ℓ)

The projection from the sphere to a lens space is an analytic local diffeomorphism.