Exact Lagrangian maps

Let σ be a nondegenerate two-form on M with a chosen primitive one-form θ, σ = -dθ, so that (M, σ, θ) is an exact symplectic manifold. A Lagrangian map f : N → M is exact, with primitive h : N → ℝ, when h is smooth and f^*θ = dh (TauCeti.SmoothTwoForm.IsNondegenerate.IsExactLagrangianMap). The primitive is part of the data: in Floer theory it is the function from which actions of intersection points are computed. The predicate applies to embedded and immersed Lagrangians alike, through any parametrization.

The main facts are:

• Exactness forces isotropy. If σ = -dθ and f^*θ = dh for a smooth f, then f^*σ = -d(dh) = 0, so f is isotropic. Hence a smooth map with injective differentials from a manifold of half the dimension is an exact Lagrangian map exactly when f^*θ is the differential of a smooth function (TauCeti.SmoothTwoForm.IsNondegenerate.isExactLagrangianMap_iff_of_finrank).
• Uniqueness of primitives. Two primitives of the same exact Lagrangian map differ by a locally constant function, and every such modification is again a primitive (IsExactLagrangianMap.isExactLagrangianMap_iff_isLocallyConstant_sub). On a preconnected source they differ by a constant.
• Change of primitive. Replacing θ by θ + dg keeps f exact, with primitive h + g ∘ f.
• Transport by exact symplectomorphisms. A diffeomorphism ψ : M → M₂ with ψ^*σ₂ = σ and ψ^*θ₂ = θ + dg carries exact Lagrangian maps f with primitive h to exact Lagrangian maps ψ ∘ f with primitive h + g ∘ f, and conversely.

The cotangent examples, the zero section and the graphs of exact one-forms, are in TauCeti.Geometry.Symplectic.Cotangent.Bundle.Graph.

Main declarations

• TauCeti.SmoothTwoForm.IsNondegenerate.IsExactLagrangianMap: exact Lagrangian maps with a specified primitive.
• TauCeti.SmoothTwoForm.IsNondegenerate.isIsotropicMap_of_mpullback_eq_mextDeriv: exactness forces isotropy.
• IsExactLagrangianMap.isExactLagrangianMap_iff_isLocallyConstant_sub, IsExactLagrangianMap.exists_eq_add_const: uniqueness of primitives, in the namespace TauCeti.SmoothTwoForm.IsNondegenerate.
• TauCeti.SmoothTwoForm.IsNondegenerate.isExactLagrangianMap_add_mextDeriv_iff: change of primitive one-form.
• Diffeomorph.isExactLagrangianMap_comp_iff: transport by exact symplectomorphisms.

References

• D. McDuff, D. Salamon, Introduction to Symplectic Topology, 3rd ed., Oxford, 2017, Sections 3.4 and 9.2.
• P. Seidel, Fukaya categories and Picard–Lefschetz theory, Zurich Lectures in Advanced Mathematics, EMS, 2008, Section 7a.

structure TauCeti.SmoothTwoForm.IsNondegenerate.IsExactLagrangianMap {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] {E' : Type u_4} {H' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] (J : ModelWithCorners ℝ E' H') {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {σ : SmoothTwoForm I M} (hσ : σ.IsNondegenerate) (θ : SmoothForm I M ℝ 1) (f : N → M) (h : N → ℝ) : Prop

A map f : N → M is an exact Lagrangian map for the nondegenerate two-form σ and the one-form θ, with primitive h : N → ℝ, when it is a Lagrangian map, h is smooth, and f pulls θ back to dh. It is meant for a primitive θ of σ, σ = -dθ; for such a θ the isotropy of f follows from f^*θ = dh (TauCeti.SmoothTwoForm.IsNondegenerate.isIsotropicMap_of_mpullback_eq_mextDeriv).

• isLagrangianMap : IsLagrangianMap J hσ f

  An exact Lagrangian map is a Lagrangian map.

• contMDiff_primitive : ContMDiff J (modelWithCornersSelf ℝ ℝ) (↑⊤) h

  The primitive of an exact Lagrangian map is smooth.

• mpullback_eq : mpullback J I f ↑θ = mextDeriv (RoughForm.ofFunction J h)

  An exact Lagrangian map pulls the one-form back to the differential of its primitive.

theorem TauCeti.SmoothTwoForm.IsNondegenerate.isExactLagrangianMap_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] {E' : Type u_4} {H' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {σ : SmoothTwoForm I M} {hσ : σ.IsNondegenerate} {θ : SmoothForm I M ℝ 1} {f : N → M} {h : N → ℝ} : IsExactLagrangianMap J hσ θ f h ↔ IsLagrangianMap J hσ f ∧ ContMDiff J (modelWithCornersSelf ℝ ℝ) (↑⊤) h ∧ mpullback J I f ↑θ = mextDeriv (RoughForm.ofFunction J h)

An exact Lagrangian map is a Lagrangian map with a smooth primitive h of the pulled-back one-form, f^*θ = dh.

Exactness forces isotropy

theorem TauCeti.SmoothTwoForm.IsNondegenerate.isIsotropicMap_of_mpullback_eq_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] {E' : Type u_4} {H' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {σ : SmoothTwoForm I M} {hσ : σ.IsNondegenerate} {θ : SmoothForm I M ℝ 1} {f : N → M} {h : N → ℝ} [IsManifold J (↑⊤) N] (hθ : σ = -(mextDerivₗ I 1) θ) (hf : ContMDiff J I (↑⊤) f) (hh : ContMDiff J (modelWithCornersSelf ℝ ℝ) 2 h) (hfh : mpullback J I f ↑θ = mextDeriv (RoughForm.ofFunction J h)) : IsIsotropicMap J hσ f

Exact maps are isotropic. If σ = -dθ and a smooth map f pulls θ back to the differential of a C² function h, then f^*σ = -d(dh) = 0, so f is isotropic for σ.

theorem TauCeti.SmoothTwoForm.IsNondegenerate.isExactLagrangianMap_iff_of_finrank {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] {E' : Type u_4} {H' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {σ : SmoothTwoForm I M} {hσ : σ.IsNondegenerate} {θ : SmoothForm I M ℝ 1} {f : N → M} {h : N → ℝ} [IsManifold J (↑⊤) N] [FiniteDimensional ℝ E] (hθ : σ = -(mextDerivₗ I 1) θ) (hf : ContMDiff J I (↑⊤) f) (hinj : ∀ (x : N), Function.Injective ⇑(mfderiv% f x)) (hdim : 2 * Module.finrank ℝ E' = Module.finrank ℝ E) : IsExactLagrangianMap J hσ θ f h ↔ ContMDiff J (modelWithCornersSelf ℝ ℝ) (↑⊤) h ∧ mpullback J I f ↑θ = mextDeriv (RoughForm.ofFunction J h)

Exact Lagrangian maps from half-dimensional manifolds. For a primitive θ of σ, a smooth map with injective differentials from a manifold of half the dimension is an exact Lagrangian map with primitive h exactly when h is smooth and f^*θ = dh.

Uniqueness of primitives

theorem TauCeti.SmoothTwoForm.IsNondegenerate.IsExactLagrangianMap.isExactLagrangianMap_iff_isLocallyConstant_sub {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] {E' : Type u_4} {H' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {σ : SmoothTwoForm I M} {hσ : σ.IsNondegenerate} {θ : SmoothForm I M ℝ 1} {f : N → M} {h h' : N → ℝ} [IsManifold J 1 N] (hL : IsExactLagrangianMap J hσ θ f h) : IsExactLagrangianMap J hσ θ f h' ↔ IsLocallyConstant (h' - h)

Primitives are unique up to locally constant functions. Given an exact Lagrangian map with primitive h, a function h' is another primitive exactly when h' - h is locally constant.

theorem TauCeti.SmoothTwoForm.IsNondegenerate.IsExactLagrangianMap.add_const {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] {E' : Type u_4} {H' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {σ : SmoothTwoForm I M} {hσ : σ.IsNondegenerate} {θ : SmoothForm I M ℝ 1} {f : N → M} {h : N → ℝ} (hL : IsExactLagrangianMap J hσ θ f h) (c : ℝ) : IsExactLagrangianMap J hσ θ f fun (x : N) => h x + c

Adding a constant to the primitive of an exact Lagrangian map gives another primitive.

theorem TauCeti.SmoothTwoForm.IsNondegenerate.IsExactLagrangianMap.exists_eq_add_const {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] {E' : Type u_4} {H' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {σ : SmoothTwoForm I M} {hσ : σ.IsNondegenerate} {θ : SmoothForm I M ℝ 1} {f : N → M} {h h' : N → ℝ} [IsManifold J 1 N] [PreconnectedSpace N] (hL : IsExactLagrangianMap J hσ θ f h) (hL' : IsExactLagrangianMap J hσ θ f h') : ∃ (c : ℝ), h' = fun (x : N) => h x + c

Primitives differ by a constant on a connected source. Two primitives of the same exact Lagrangian map from a preconnected manifold differ by a constant.

Change of primitive one-form

theorem TauCeti.SmoothTwoForm.IsNondegenerate.isExactLagrangianMap_add_mextDeriv_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] {E' : Type u_4} {H' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {σ : SmoothTwoForm I M} {hσ : σ.IsNondegenerate} {θ θ' : SmoothForm I M ℝ 1} {f : N → M} {h : N → ℝ} (hf : ContMDiff J I (↑⊤) f) {g : M → ℝ} (hg : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) g) (hθ' : ↑θ' = ↑θ + mextDeriv (RoughForm.ofFunction I g)) : IsExactLagrangianMap J hσ θ' f (h + g ∘ f) ↔ IsExactLagrangianMap J hσ θ f h

Changing the primitive one-form by an exact form. If θ' = θ + dg for a smooth function g on M, then a smooth map f is an exact Lagrangian map for θ' with primitive h + g ∘ f exactly when it is one for θ with primitive h.

Transport by exact symplectomorphisms

theorem Diffeomorph.isExactLagrangianMap_comp_iff_of_mpullback_eq {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] {E' : Type u_4} {H' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {σ : TauCeti.SmoothTwoForm I M} {hσ : σ.IsNondegenerate} {θ : TauCeti.SmoothForm I M ℝ 1} {f : N → M} {h : N → ℝ} {E₂ : Type u_7} {H₂ : Type u_8} [NormedAddCommGroup E₂] [NormedSpace ℝ E₂] [TopologicalSpace H₂] {I₂ : ModelWithCorners ℝ E₂ H₂} {M₂ : Type u_9} [TopologicalSpace M₂] [ChartedSpace H₂ M₂] [IsManifold I₂ (↑⊤) M₂] {σ₂ : TauCeti.SmoothTwoForm I₂ M₂} {hσ₂ : σ₂.IsNondegenerate} {θ₂ : TauCeti.SmoothForm I₂ M₂ ℝ 1} (ψ : Diffeomorph I I₂ M M₂ ↑⊤) (hψ : (TauCeti.SmoothForm.mpullback ⇑ψ ⋯) σ₂ = σ) (hψθ : (TauCeti.SmoothForm.mpullback ⇑ψ ⋯) θ₂ = θ) : TauCeti.SmoothTwoForm.IsNondegenerate.IsExactLagrangianMap J hσ₂ θ₂ (⇑ψ ∘ f) h ↔ TauCeti.SmoothTwoForm.IsNondegenerate.IsExactLagrangianMap J hσ θ f h

A symplectomorphism ψ with ψ^*σ₂ = σ carries exact Lagrangian maps for θ to exact Lagrangian maps for θ₂, with the same primitive, when it pulls θ₂ back to θ.

theorem Diffeomorph.isExactLagrangianMap_comp_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] {E' : Type u_4} {H' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {σ : TauCeti.SmoothTwoForm I M} {hσ : σ.IsNondegenerate} {θ : TauCeti.SmoothForm I M ℝ 1} {f : N → M} {h : N → ℝ} {E₂ : Type u_7} {H₂ : Type u_8} [NormedAddCommGroup E₂] [NormedSpace ℝ E₂] [TopologicalSpace H₂] {I₂ : ModelWithCorners ℝ E₂ H₂} {M₂ : Type u_9} [TopologicalSpace M₂] [ChartedSpace H₂ M₂] [IsManifold I₂ (↑⊤) M₂] {σ₂ : TauCeti.SmoothTwoForm I₂ M₂} {hσ₂ : σ₂.IsNondegenerate} {θ₂ : TauCeti.SmoothForm I₂ M₂ ℝ 1} (ψ : Diffeomorph I I₂ M M₂ ↑⊤) (hψ : (TauCeti.SmoothForm.mpullback ⇑ψ ⋯) σ₂ = σ) {g : M → ℝ} (hg : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) g) (hψθ : TauCeti.mpullback I I₂ ⇑ψ ↑θ₂ = ↑θ + TauCeti.mextDeriv (TauCeti.RoughForm.ofFunction I g)) (hf : ContMDiff J I (↑⊤) f) : TauCeti.SmoothTwoForm.IsNondegenerate.IsExactLagrangianMap J hσ₂ θ₂ (⇑ψ ∘ f) (h + g ∘ f) ↔ TauCeti.SmoothTwoForm.IsNondegenerate.IsExactLagrangianMap J hσ θ f h

Transport by exact symplectomorphisms. Let ψ : M → M₂ be a diffeomorphism with ψ^*σ₂ = σ and ψ^*θ₂ = θ + dg for a smooth function g on M. Then ψ ∘ f is an exact Lagrangian map for θ₂ with primitive h + g ∘ f exactly when f is an exact Lagrangian map for θ with primitive h.