The cotangent bundle of a manifold

The cotangent bundle T*M of a manifold M modelled on I : ModelWithCorners 𝕜 E H is the total space of the bundle of continuous linear functionals on the tangent spaces,

TauCeti.CotangentBundle I M = Bundle.TotalSpace (E →L[𝕜] 𝕜) (fun x ↦ TangentSpace I x →L[𝕜] 𝕜).

No new structure is chosen: its topology, fibre-bundle and vector-bundle structure, charts and manifold structure, modelled on I.prod 𝓘(𝕜, E →L[𝕜] 𝕜), are those of Mathlib's bundle of continuous linear maps from the tangent bundle to the trivial line bundle. In particular, the projection is a submersion by Bundle.isSubmersion_proj, the zero section is smooth by Bundle.contMDiff_zeroSection, and the fibrewise addition and scalar multiplication are the vector space structures of the fibres.

This file computes the charts in coordinates. The preferred chart at a covector over x₀ sends a covector p at x to (φ₀ x, p ∘ d(φ₀⁻¹)), where φ₀ is the extended chart of M at x₀ (TauCeti.CotangentBundle.extChartAt_apply, TauCeti.CotangentBundle.extChartAt_symm_apply). Consequently, a change of base chart φ = φ₁ ∘ φ₀⁻¹ acts on cotangent coordinates by

(q, p) ↦ (φ q, p ∘ (dφ_q)⁻¹),

the derivative of the inverse change of charts at φ q (TauCeti.CotangentBundle.extChartAt_extChartAt_symm). The new covector pairs with the pushed-forward tangent vector as the old covector pairs with the original one (TauCeti.CotangentBundle.extChartAt_extChartAt_symm_snd_apply_fderivWithin). This is the transformation law of covector components, dual to that of tangent vectors. A map into the single fibre over a fixed point q moves only the fibre coordinate in these charts, so its derivative is that of its covector part (TauCeti.CotangentBundle.hasMFDerivAt_mk).

Covectors pull back along the differential of a map f : M → N: a covector p at f x gives the covector p ∘ df_x at x. For a family of covectors over a parameter manifold this is smooth: TauCeti.CotangentBundle.contMDiffAt_mk_comp_mfderiv loses one degree of smoothness of f, as the differential does. It gives the smoothness of the cotangent lift of a diffeomorphism (Diffeomorph.cotangent). The map may also vary smoothly with the parameter (TauCeti.CotangentBundle.contMDiffAt_mk_comp_mfderiv_uncurry), as the slice inclusions of a product manifold do.

The construction follows the Zulip discussion Cotangent Bundle as a Manifold in the channel Is there code for X?, which observed that Mathlib's continuous-linear-map bundle operations already supply the cotangent total space with its manifold structure.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Graduate Texts in Mathematics 218, Springer, 2013, Chapter 11.

@[reducible, inline]

abbrev TauCeti.CotangentBundle {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u_4) [TopologicalSpace M] [ChartedSpace H M] : Type (max u_4 u_1 u_2)

The cotangent bundle of a manifold M modelled on I: the total space of the bundle whose fibre at x is the space of continuous linear functionals on TangentSpace I x. It is a manifold modelled on I.prod 𝓘(𝕜, E →L[𝕜] 𝕜).

theorem TauCeti.CotangentBundle.ext {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {z w : CotangentBundle I M} (hproj : z.proj = w.proj) (h : ∀ (v : TangentSpace I z.proj), z.snd v = w.snd v) : z = w

Two covectors are equal if they have the same base point and take the same values.

theorem TauCeti.CotangentBundle.extChartAt_apply {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (z₀ z : CotangentBundle I M) : ↑(extChartAt (I.prod (modelWithCornersSelf 𝕜 (E →L[𝕜] 𝕜))) z₀) z = (↑(extChartAt I z₀.proj) z.proj, z.snd ∘SL Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) z₀.proj) z.proj)

The preferred chart of the cotangent bundle at z₀ sends a covector z to the chart image of its base point and to the covector precomposed with the inverse of the tangent chart at z₀.

theorem TauCeti.CotangentBundle.extChartAt_symm_apply {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (z₀ : CotangentBundle I M) {q : E} (p : E →L[𝕜] 𝕜) (hq : q ∈ (extChartAt I z₀.proj).target) : ↑(extChartAt (I.prod (modelWithCornersSelf 𝕜 (E →L[𝕜] 𝕜))) z₀).symm (q, p) = ⟨↑(extChartAt I z₀.proj).symm q, p ∘SL Bundle.Trivialization.continuousLinearMapAt 𝕜 (trivializationAt E (TangentSpace I) z₀.proj) (↑(extChartAt I z₀.proj).symm q)⟩

The inverse of the preferred chart of the cotangent bundle at z₀ sends a point q of the base chart and a model covector p to the covector p composed with the tangent chart, at the point of M with coordinates q.

theorem TauCeti.CotangentBundle.extChartAt_extChartAt_symm {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (z₀ z₁ : CotangentBundle I M) {q : E} (p : E →L[𝕜] 𝕜) (hq : q ∈ (extChartAt I z₀.proj).target) (hq₁ : ↑(extChartAt I z₀.proj).symm q ∈ (extChartAt I z₁.proj).source) : ↑(extChartAt (I.prod (modelWithCornersSelf 𝕜 (E →L[𝕜] 𝕜))) z₁) (↑(extChartAt (I.prod (modelWithCornersSelf 𝕜 (E →L[𝕜] 𝕜))) z₀).symm (q, p)) = ((↑(extChartAt I z₁.proj) ∘ ↑(extChartAt I z₀.proj).symm) q, p ∘SL fderivWithin 𝕜 (↑(extChartAt I z₀.proj) ∘ ↑(extChartAt I z₁.proj).symm) (Set.range ↑I) ((↑(extChartAt I z₁.proj) ∘ ↑(extChartAt I z₀.proj).symm) q))

Transition maps of the cotangent bundle. Changing from the preferred chart at z₀ to the preferred chart at z₁ sends (q, p) to (φ q, p ∘ (dφ_q)⁻¹), where φ is the change of base charts; (dφ_q)⁻¹ is the derivative of the inverse change of charts at φ q.

theorem TauCeti.CotangentBundle.extChartAt_extChartAt_symm_snd_apply_fderivWithin {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (z₀ z₁ : CotangentBundle I M) {q : E} (p : E →L[𝕜] 𝕜) (hq : q ∈ (extChartAt I z₀.proj).target) (hq₁ : ↑(extChartAt I z₀.proj).symm q ∈ (extChartAt I z₁.proj).source) (v : E) : (↑(extChartAt (I.prod (modelWithCornersSelf 𝕜 (E →L[𝕜] 𝕜))) z₁) (↑(extChartAt (I.prod (modelWithCornersSelf 𝕜 (E →L[𝕜] 𝕜))) z₀).symm (q, p))).2 ((fderivWithin 𝕜 (↑(extChartAt I z₁.proj) ∘ ↑(extChartAt I z₀.proj).symm) (Set.range ↑I) q) v) = p v

A change of charts of the cotangent bundle preserves the pairing of covectors with tangent vectors: the new covector, evaluated on the image of v under the derivative of the change of base charts, is the old covector evaluated on v.

theorem TauCeti.CotangentBundle.contMDiffOn_mk_comp_continuousLinearMapAt {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n : WithTop ℕ∞} [IsManifold I (n + 1) M] (x : M) {U : Set M} (hU : U ⊆ (trivializationAt E (TangentSpace I) x).baseSet) {c : M → E →L[𝕜] 𝕜} (hc : ContMDiffOn I (modelWithCornersSelf 𝕜 (E →L[𝕜] 𝕜)) n c U) : ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 (E →L[𝕜] 𝕜))) n (fun (y : M) => ⟨y, c y ∘SL Bundle.Trivialization.continuousLinearMapAt 𝕜 (trivializationAt E (TangentSpace I) x) y⟩) U

Pulling a C^n family of model covectors back through tangent-bundle coordinates gives a C^n cotangent section wherever the coordinates are defined.

theorem TauCeti.CotangentBundle.hasMFDerivAt_mk {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {EX : Type u_5} {HX : Type u_6} {X : Type u_7} [NormedAddCommGroup EX] [NormedSpace 𝕜 EX] [TopologicalSpace HX] {IX : ModelWithCorners 𝕜 EX HX} [TopologicalSpace X] [ChartedSpace HX X] (q : M) {c : X → E →L[𝕜] 𝕜} {y : X} {c' : TangentSpace IX y →L[𝕜] E →L[𝕜] 𝕜} (hc : HasMFDerivAt% c y c') : HasMFDerivAt% (fun (y : X) => ⟨q, c y⟩) y (ContinuousLinearMap.inr 𝕜 E (E →L[𝕜] 𝕜) ∘SL c')

The derivative of a map into one fibre. If c : X → E →L[𝕜] 𝕜 has derivative c' at y, then y ↦ (q, c y), a map into the fibre of the cotangent bundle over the fixed point q, has derivative w ↦ (0, c' w) at y, read in the preferred chart at (q, c y): the base coordinate does not move, and over q the tangent trivialization at q is the identity.

theorem TauCeti.CotangentBundle.contMDiffAt_mk_comp_mfderiv {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {E' : Type u_5} {H' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold J 1 N] {EX : Type u_8} {HX : Type u_9} {X : Type u_10} [NormedAddCommGroup EX] [NormedSpace 𝕜 EX] [TopologicalSpace HX] {IX : ModelWithCorners 𝕜 EX HX} [TopologicalSpace X] [ChartedSpace HX X] {m n : WithTop ℕ∞} {Ψ : X → CotangentBundle J N} {g : X → M} {f : M → N} {z₀ : X} (hΨg : ∀ (z : X), (Ψ z).proj = f (g z)) (hΨ : ContMDiffAt IX (J.prod (modelWithCornersSelf 𝕜 (E' →L[𝕜] 𝕜))) m Ψ z₀) (hg : ContMDiffAt IX I m g z₀) (hf : ContMDiffAt I J n f (g z₀)) (hmn : m + 1 ≤ n) : ContMDiffAt IX (I.prod (modelWithCornersSelf 𝕜 (E →L[𝕜] 𝕜))) m (fun (z : X) => ⟨g z, (Ψ z).snd ∘SL mfderiv% f (g z)⟩) z₀

Pulling covectors back along a map is smooth. Let Ψ z be a covector at f (g z), depending on a parameter z. Its pullback along the differential of f at g z, Ψ z ∘ df_(g z), is a covector at g z. If Ψ and g are C^m at z₀ and f is C^n at g z₀ with m + 1 ≤ n, the family of pulled-back covectors is C^m at z₀.

theorem TauCeti.CotangentBundle.contMDiff_mk_comp_mfderiv {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {E' : Type u_5} {H' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold J 1 N] {EX : Type u_8} {HX : Type u_9} {X : Type u_10} [NormedAddCommGroup EX] [NormedSpace 𝕜 EX] [TopologicalSpace HX] {IX : ModelWithCorners 𝕜 EX HX} [TopologicalSpace X] [ChartedSpace HX X] {m n : WithTop ℕ∞} {Ψ : X → CotangentBundle J N} {g : X → M} {f : M → N} (hΨg : ∀ (z : X), (Ψ z).proj = f (g z)) (hΨ : ContMDiff IX (J.prod (modelWithCornersSelf 𝕜 (E' →L[𝕜] 𝕜))) m Ψ) (hg : ContMDiff IX I m g) (hf : ContMDiff I J n f) (hmn : m + 1 ≤ n) : ContMDiff IX (I.prod (modelWithCornersSelf 𝕜 (E →L[𝕜] 𝕜))) m fun (z : X) => ⟨g z, (Ψ z).snd ∘SL mfderiv% f (g z)⟩

Pulling covectors back along a map is smooth. The global version of TauCeti.CotangentBundle.contMDiffAt_mk_comp_mfderiv.

theorem TauCeti.CotangentBundle.contMDiffAt_mk_comp_mfderiv_uncurry {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {E' : Type u_5} {H' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold J 1 N] {EX : Type u_8} {HX : Type u_9} {X : Type u_10} [NormedAddCommGroup EX] [NormedSpace 𝕜 EX] [TopologicalSpace HX] {IX : ModelWithCorners 𝕜 EX HX} [TopologicalSpace X] [ChartedSpace HX X] {m n : WithTop ℕ∞} [IsManifold IX 1 X] {Ψ : X → CotangentBundle J N} {g : X → M} {f : X → M → N} {z₀ : X} (hΨg : ∀ (z : X), (Ψ z).proj = f z (g z)) (hΨ : ContMDiffAt IX (J.prod (modelWithCornersSelf 𝕜 (E' →L[𝕜] 𝕜))) m Ψ z₀) (hg : ContMDiffAt IX I m g z₀) (hf : ContMDiffAt (IX.prod I) J n (Function.uncurry f) (z₀, g z₀)) (hmn : m + 1 ≤ n) : ContMDiffAt IX (I.prod (modelWithCornersSelf 𝕜 (E →L[𝕜] 𝕜))) m (fun (z : X) => ⟨g z, (Ψ z).snd ∘SL mfderiv% (f z) (g z)⟩) z₀

Pulling covectors back along a family of maps is smooth. Let Ψ z be a covector at f z (g z), depending on a parameter z. Its pullback along the differential of f z at g z, Ψ z ∘ d(f z)_(g z), is a covector at g z. If Ψ and g are C^m at z₀ and (z, x) ↦ f z x is C^n at (z₀, g z₀) with m + 1 ≤ n, the family of pulled-back covectors is C^m at z₀. Unlike TauCeti.CotangentBundle.contMDiffAt_mk_comp_mfderiv, the map may vary with the parameter, which is then required to range over a C¹ manifold.