The unit codisc and cosphere bundles of a Riemannian manifold

A Riemannian metric g on a manifold M measures covectors, and so singles out two subsets of the cotangent bundle T*M = TauCeti.CotangentBundle I M:

• the unit codisc bundle D*M = {z | ‖z.2‖ ≤ 1} (TauCeti.CotangentBundle.codiscBundle);
• the unit cosphere bundle S*M = {z | ‖z.2‖ = 1} (TauCeti.CotangentBundle.cosphereBundle).

Here ‖p‖ is the norm of a covector for g, the operator norm for the metric norm on the tangent space. With the canonical symplectic form of T*M and the Liouville form -λ, the codisc bundle of a compact manifold is the standard example of a Liouville domain, and these are the sets on which the symplectic capacities of cotangent bundles are computed. This file establishes their point-set and smooth structure.

Both sets are closed, and compact when M is compact (TauCeti.CotangentBundle.isCompact_codiscBundle) by IsCompact.norm_le_bundle_of_continuous: near each point the bundle coordinates of a covector are bounded by a multiple of its norm, since the inverse tangent trivialization is locally bounded.

Since every nonzero value is a regular value of the norm of covectors (TauCeti.CotangentBundle.isRegularValue_norm_snd), S*M is a regular level. For a smooth metric on a boundaryless manifold, it carries the atlas TauCeti.regularLevelChartedSpace of regular levels, for which it is a smooth manifold of dimension dim T*M - 1 (TauCeti.CotangentBundle.instIsManifoldCosphereBundle) and a smoothly embedded hypersurface of T*M (TauCeti.CotangentBundle.isSmoothEmbedding_coe_cosphereBundle) whose tangent spaces are the kernels of the differential of the norm (TauCeti.CotangentBundle.range_mfderiv_coe_cosphereBundle).

Main definitions

• TauCeti.CotangentBundle.codiscBundle: the unit codisc bundle D*M.
• TauCeti.CotangentBundle.cosphereBundle: the unit cosphere bundle S*M.

Main results

• TauCeti.CotangentBundle.isClosed_codiscBundle and TauCeti.CotangentBundle.isCompact_codiscBundle: D*M is closed, and compact over a compact manifold; similarly for S*M.
• TauCeti.CotangentBundle.instIsManifoldCosphereBundle: S*M is a smooth manifold.
• TauCeti.CotangentBundle.isSmoothEmbedding_coe_cosphereBundle: its inclusion into T*M is a smooth embedding.

References

• D. McDuff, D. Salamon, Introduction to Symplectic Topology, 3rd ed., Oxford, 2017, Section 3.2 and Chapter 12.
• J.-F. Barraud, M. Damian, V. Humilière, A. Oancea, Floer homology with DG coefficients. Applications to cotangent bundles, arXiv:2404.07953, §1.2.

def TauCeti.CotangentBundle.codiscBundle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] : Set (CotangentBundle I M)

The unit codisc bundle D*M of a Riemannian manifold: the covectors of norm at most one.

def TauCeti.CotangentBundle.cosphereBundle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] : Set (CotangentBundle I M)

The unit cosphere bundle S*M of a Riemannian manifold: the covectors of norm one. Its body is exposed because the manifold structure on S*M is that of the regular level {z // ‖z.2‖ = 1}, read through this definition.

@[simp]

theorem TauCeti.CotangentBundle.mem_codiscBundle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {z : CotangentBundle I M} : z ∈ codiscBundle I M ↔ ‖z.snd‖ ≤ 1

@[simp]

theorem TauCeti.CotangentBundle.mem_cosphereBundle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {z : CotangentBundle I M} : z ∈ cosphereBundle I M ↔ ‖z.snd‖ = 1

theorem TauCeti.CotangentBundle.cosphereBundle_subset_codiscBundle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] : cosphereBundle I M ⊆ codiscBundle I M

theorem TauCeti.CotangentBundle.snd_ne_zero_of_mem_cosphereBundle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {z : CotangentBundle I M} (hz : z ∈ cosphereBundle I M) : z.snd ≠ 0

A covector of the unit cosphere bundle is not zero.

theorem TauCeti.CotangentBundle.isClosed_codiscBundle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I 1 M] [IsContMDiffRiemannianBundle I 0 E fun (x : M) => TangentSpace I x] : IsClosed (codiscBundle I M)

theorem TauCeti.CotangentBundle.isClosed_cosphereBundle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I 1 M] [IsContMDiffRiemannianBundle I 0 E fun (x : M) => TangentSpace I x] : IsClosed (cosphereBundle I M)

theorem TauCeti.CotangentBundle.isCompact_codiscBundle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I 1 M] [IsContMDiffRiemannianBundle I 0 E fun (x : M) => TangentSpace I x] [CompactSpace M] : IsCompact (codiscBundle I M)

The unit codisc bundle of a compact Riemannian manifold is compact.

theorem TauCeti.CotangentBundle.isCompact_cosphereBundle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I 1 M] [IsContMDiffRiemannianBundle I 0 E fun (x : M) => TangentSpace I x] [CompactSpace M] : IsCompact (cosphereBundle I M)

The unit cosphere bundle of a compact Riemannian manifold is compact.

instance TauCeti.CotangentBundle.instCompactSpaceElemRealCosphereBundle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I 1 M] [IsContMDiffRiemannianBundle I 0 E fun (x : M) => TangentSpace I x] [CompactSpace M] : CompactSpace ↑(cosphereBundle I M)

theorem TauCeti.CotangentBundle.contMDiffAt_norm_snd_of_mem_cosphereBundle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I 1 M] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] (z : CotangentBundle I M) (hz : z ∈ cosphereBundle I M) : ContMDiffAt (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] ℝ))) (modelWithCornersSelf ℝ ℝ) (↑⊤) (fun (z : CotangentBundle I M) => ‖z.snd‖) z

The norm of covectors is smooth at the points of the unit cosphere bundle.

@[instance_reducible]

noncomputable instance TauCeti.CotangentBundle.instChartedSpaceForallFinHSubNatFinrankRealProdContinuousLinearMapIdOfNatElemCosphereBundle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I 1 M] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [I.Boundaryless] : ChartedSpace (Fin (Module.finrank ℝ (E × (E →L[ℝ] ℝ)) - 1) → ℝ) ↑(cosphereBundle I M)

The unit cosphere bundle of a smooth Riemannian manifold without boundary, with the atlas of the regular level ‖z.2‖ = 1 of the norm of covectors.

instance TauCeti.CotangentBundle.instIsManifoldCosphereBundle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I 1 M] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [I.Boundaryless] : IsManifold (modelWithCornersSelf ℝ (Fin (Module.finrank ℝ (E × (E →L[ℝ] ℝ)) - 1) → ℝ)) ↑⊤ ↑(cosphereBundle I M)

The unit cosphere bundle is a smooth manifold, of dimension dim T*M - 1.

theorem TauCeti.CotangentBundle.isSmoothEmbedding_coe_cosphereBundle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I 1 M] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [I.Boundaryless] : Manifold.IsSmoothEmbedding (modelWithCornersSelf ℝ (Fin (Module.finrank ℝ (E × (E →L[ℝ] ℝ)) - 1) → ℝ)) (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] ℝ))) (↑⊤) Subtype.val

The unit cosphere bundle is a smoothly embedded hypersurface of the cotangent bundle.

theorem TauCeti.CotangentBundle.range_mfderiv_coe_cosphereBundle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I 1 M] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [I.Boundaryless] (z : ↑(cosphereBundle I M)) : (↑(mfderiv% Subtype.val z)).range = (↑((mfderiv% fun (z : CotangentBundle I M) => ‖z.snd‖) ↑z)).ker

The tangent space of the unit cosphere bundle at a covector is the kernel of the differential of the norm of covectors there.