Graphs of one-forms in a cotangent bundle

A smooth one-form α on a manifold M is a smooth section s_α : x ↦ α_x of the cotangent bundle T*M = TauCeti.CotangentBundle I M; its image is the graph of α. Since the Liouville form λ is tautological, s_α^*λ = α (TauCeti.CotangentBundle.mpullback_liouvilleForm), and so the canonical symplectic form ω = -dλ pulls back to s_α^*ω = -dα (TauCeti.CotangentBundle.mpullback_symplecticForm).

The section s_α has injective differential, because the projection π : T*M → M is a left inverse of it (Bundle.mfderiv_injective_of_proj_comp_eq_id). Combining these facts with the tangent-image predicates of TauCeti.Geometry.Symplectic.Lagrangian.Manifold:

• s_α is an isotropic map exactly when α is closed (TauCeti.CotangentBundle.isIsotropicMap_section_iff);
• when M is finite-dimensional, T*M has twice the dimension of M, so s_α is a Lagrangian map exactly when α is closed (TauCeti.CotangentBundle.isLagrangianMap_section_iff).

In particular the zero section of T*M is a Lagrangian map (TauCeti.CotangentBundle.isLagrangianMap_zeroSection), and so is the graph of the differential df of a smooth function (TauCeti.CotangentBundle.isLagrangianMap_section_mextDerivₗ).

Since s_α^*λ = α, the graph of α is an exact Lagrangian map for the primitive λ of ω, with primitive h, exactly when α = dh (TauCeti.CotangentBundle.isExactLagrangianMap_section_iff). So the graph is exact Lagrangian for some primitive exactly when α is an exact form (TauCeti.CotangentBundle.exists_isExactLagrangianMap_section_iff); the zero section is exact Lagrangian with primitive 0 (TauCeti.CotangentBundle.isExactLagrangianMap_zeroSection).

Main declarations

• TauCeti.CotangentBundle.mpullback_symplecticForm: s_α^*ω = -dα.
• TauCeti.CotangentBundle.isIsotropicMap_section_iff: the graph of α is isotropic iff dα = 0.
• TauCeti.CotangentBundle.isLagrangianMap_section_iff: the graph of α is Lagrangian iff dα = 0.
• TauCeti.CotangentBundle.isLagrangianMap_zeroSection: the zero section is Lagrangian.
• TauCeti.CotangentBundle.isLagrangianMap_section_mextDerivₗ: the graph of df is Lagrangian.
• TauCeti.CotangentBundle.isExactLagrangianMap_section_iff: the graph of α is exact Lagrangian with primitive h iff α = dh.
• TauCeti.CotangentBundle.exists_isExactLagrangianMap_section_iff: the graph of α is exact Lagrangian iff α is exact.
• TauCeti.CotangentBundle.isExactLagrangianMap_zeroSection: the zero section is exact Lagrangian.

References

• A. Cannas da Silva, Lectures on Symplectic Geometry, Lecture Notes in Mathematics 1764, Springer, 2001, Section 3.
• D. McDuff, D. Salamon, Introduction to Symplectic Topology, 3rd ed., Oxford, 2017, Section 3.2.

theorem TauCeti.CotangentBundle.mpullback_symplecticForm {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (α : SmoothForm I M ℝ 1) : (SmoothForm.mpullback (fun (x : M) => ⟨x, (SmoothForm.degreeOneEquiv α) x⟩) ⋯) (symplecticForm I M) = -(mextDerivₗ I 1) α

The graph of a one-form pulls the symplectic form back to minus its derivative. The section of the cotangent bundle defined by a smooth one-form α pulls the canonical symplectic form ω = -dλ back to -dα.

theorem TauCeti.CotangentBundle.isIsotropicMap_section_iff {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (α : SmoothForm I M ℝ 1) : (SmoothTwoForm.IsNondegenerate.IsIsotropicMap I ⋯ fun (x : M) => ⟨x, (SmoothForm.degreeOneEquiv α) x⟩) ↔ α.IsClosed

The graph of a one-form is isotropic exactly when the form is closed. The section of the cotangent bundle defined by a smooth one-form α is an isotropic map for the canonical symplectic form if and only if dα = 0.

theorem TauCeti.CotangentBundle.isLagrangianMap_section_iff {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [FiniteDimensional ℝ E] (α : SmoothForm I M ℝ 1) : (SmoothTwoForm.IsNondegenerate.IsLagrangianMap I ⋯ fun (x : M) => ⟨x, (SmoothForm.degreeOneEquiv α) x⟩) ↔ α.IsClosed

The graph of a one-form is Lagrangian exactly when the form is closed. On a finite-dimensional manifold, the section of the cotangent bundle defined by a smooth one-form α is a Lagrangian map for the canonical symplectic form if and only if dα = 0.

theorem TauCeti.CotangentBundle.isLagrangianMap_zeroSection {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [FiniteDimensional ℝ E] : SmoothTwoForm.IsNondegenerate.IsLagrangianMap I ⋯ (Bundle.zeroSection (E →L[ℝ] ℝ) fun (x : M) => TangentSpace I x →L[ℝ] ℝ)

The zero section is Lagrangian. On a finite-dimensional manifold, the zero section of the cotangent bundle is a Lagrangian map for the canonical symplectic form.

theorem TauCeti.CotangentBundle.isLagrangianMap_section_mextDerivₗ {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [FiniteDimensional ℝ E] (f : SmoothForm I M ℝ 0) : SmoothTwoForm.IsNondegenerate.IsLagrangianMap I ⋯ fun (x : M) => ⟨x, (SmoothForm.degreeOneEquiv ((mextDerivₗ I 0) f)) x⟩

The graph of an exact one-form is Lagrangian. On a finite-dimensional manifold, the section of the cotangent bundle defined by the differential df of a smooth function f is a Lagrangian map for the canonical symplectic form.

Exact Lagrangian graphs

theorem TauCeti.CotangentBundle.isExactLagrangianMap_section_iff {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [FiniteDimensional ℝ E] (α : SmoothForm I M ℝ 1) {h : M → ℝ} : SmoothTwoForm.IsNondegenerate.IsExactLagrangianMap I ⋯ (liouvilleForm I M) (fun (x : M) => ⟨x, (SmoothForm.degreeOneEquiv α) x⟩) h ↔ ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) h ∧ ↑α = mextDeriv (RoughForm.ofFunction I h)

The graph of a one-form is exact Lagrangian exactly when the form is exact. On a finite-dimensional manifold, the section of the cotangent bundle defined by a smooth one-form α is an exact Lagrangian map for the primitive λ of ω = -dλ, with primitive h, if and only if h is smooth and α = dh.

theorem TauCeti.CotangentBundle.exists_isExactLagrangianMap_section_iff {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [FiniteDimensional ℝ E] (α : SmoothForm I M ℝ 1) : (∃ (h : M → ℝ), SmoothTwoForm.IsNondegenerate.IsExactLagrangianMap I ⋯ (liouvilleForm I M) (fun (x : M) => ⟨x, (SmoothForm.degreeOneEquiv α) x⟩) h) ↔ α ∈ exactForms I M 1

The graph of a one-form is exact Lagrangian for some primitive exactly when the form is exact. On a finite-dimensional manifold, the pulled-back Liouville form on the graph of a smooth one-form α has a smooth primitive making the graph an exact Lagrangian map if and only if α is an exact form.

theorem TauCeti.CotangentBundle.isExactLagrangianMap_zeroSection {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [FiniteDimensional ℝ E] : SmoothTwoForm.IsNondegenerate.IsExactLagrangianMap I ⋯ (liouvilleForm I M) (Bundle.zeroSection (E →L[ℝ] ℝ) fun (x : M) => TangentSpace I x →L[ℝ] ℝ) 0

The zero section is exact Lagrangian. On a finite-dimensional manifold, the zero section of the cotangent bundle is an exact Lagrangian map for the primitive λ of ω = -dλ, with primitive 0, since λ vanishes along it.